Formal Analysis of Vehicular Crash Severity Using KeYmaera X

In this paper, we integrate formal methods with traffic conflict techniques such as Time-To-Collision and Deceleration Rate, and evasive action indicators, like Jerk Profile and Yaw Rate in order to introduce a practical traffic safety rule. We propose the use of formal methods to prove the correctness of this traffic safety rule and verify road users’ compliance with it. To this end, we utilize differential dynamic logic and the KeYmaera X theorem prover for the formalization and verification of this rule. Furthermore, we conduct a formal analysis of crash severity applied to different traffic collision scenarios to determine the optimal evasive actions to be taken during a traffic conflict, along with their appropriate intensity. Using KeYmaera X, we are able to automatically verify the proposed traffic safety rule in three traffic collision scenarios, namely rear-end and head-on and left-side collisions.