Formal Analysis of Traffic Conflicts Severity using KeYmaera

Evaluating traffic safety based on extracted crash data is deemed unreliable. 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, the correctness of the property is guaranteed thanks to the mathematical basis and rigorous analysis nature of formal methods. This research project aims to complement conventional data-oriented methods for traffic safety assessment with the formalization of TCTs and formal verification of safety properties using the KeYmaera theorem prover based on differential Dynamic Logic (dDL). Our main focus is to guarantee the safety of road users through the evaluation of traffic situations and providing safer traffic interactions between vehicles. In order to analyse different traffic situations and conduct a speed-adaptation feedback loop to update vehicles' speeds, we use the SUMO (Simulation of Urban MObility) traffic simulator, which we feed with the verified property by establishing a data exchange via Mathematica.

Publications

Thesis

Oumaima Barhoumi, "Formal Analysis of Traffic Conflicts Severity using KeYmaera", MASc Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, August 2024.

Conference Papers

[1] Barhoumi, Oumaima, Mohamed H. Zaki, and Sofiène Tahar. Formal Analysis of Vehicular Crash Severity Using KeYmaera X. Symbolic Computation in Software Science, LNCS 14991, Tokyo, Japan, August 2024 (To Appear).

Journal Papers

[1] Barhoumi, Oumaima, Mohamed H. Zaki, and Sofiène Tahar. A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques. IEEE Open Journal of Vehicular Technology, Vol. 5, April 2024, pp. 606-619.