Abstract

Evaluating traffic safety based on crash data is deemed unreliable due to the scarcity of the reported crashes. Furthermore, the process of accumulating a dependable database can take years to be achieved. As an alternative, surrogate safety measures such as Traffic Conflict Techniques (TCTs) are emerging to address many shortcomings of the crash data analysis. However, using data-centric approaches such as simulation to identify traffic conflicts events leading to crashes limits the confidence in road safety assessment. With formal verification, improving traffic safety by accurately analysing traffic conflicts is guaranteed thanks to the mathematical basis and rigorous analysis nature of formal methods.

This thesis aims to complement conventional data-oriented methods for traffic safety assessment with the formal verification of safety properties using the KeYmaera theorem prover based on differential Dynamic Logic (dL). Our main focus is to guarantee the safety of road users through the evaluation of traffic conflicts and providing safer traffic interactions between vehicles. Towards achieving this goal, we propose a set of traffic safety properties based on the combination of different TCTs, i.e., time-to-collision (TTC), space headway (SHW), shockwave speed (SWV), extended delta-V ($\Delta$V) and deceleration rate, along with evasive actions indicators, i.e., jerk profile and yaw rate. The aim of these properties is to formally analyse traffic conflicts in order to determine their severity as well as set accurate traffic conditions to ensure the traffic safety.

In another effort to validate the property linking TTC, SHW and SWV, we use SUMO (Simulation of Urban MObility) on a real-life dataset. Thanks to this traffic simulator, the vehicles dynamics are extracted and a list of TCTs is also provided for every time step. In order to realize a traffic management process, Mathematica is used to interface with SUMO, identify vehicles violating the stated safety property and conduct a speed-adaptation control process to update vehicles’ speeds.