Login | Register

Formal Analysis Of Traffic Conflicts Severity Using Keymaera


Formal Analysis Of Traffic Conflicts Severity Using Keymaera

barhoumi, oumaima (2022) Formal Analysis Of Traffic Conflicts Severity Using Keymaera. Masters thesis, Concordia University.

[thumbnail of Barhoumi_MASc_S2022 (PDF-A).pdf]
Text (application/pdf)
Barhoumi_MASc_S2022 (PDF-A).pdf - Accepted Version
Available under License Spectrum Terms of Access.


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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:barhoumi, oumaima
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:10 August 2022
Thesis Supervisor(s):Tahar, Sofiene
ID Code:990832
Deposited By: Oumaima Barhoumi
Deposited On:27 Oct 2022 14:21
Last Modified:27 Oct 2022 14:21
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top