A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques
Traffic conflict techniques enable a comprehensive assessment of traffic safety analysis. Formal methods allow the identification of factors that contribute to traffic safety issues and provide evidence of potential safety degradation. As such, formal methods provide a novel way to model traffic rul...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2024-01-01
|
| Series: | IEEE Open Journal of Vehicular Technology |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/10496854/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832582338367717376 |
|---|---|
| author | Oumaima Barhoumi Mohamed H. Zaki Sofiene Tahar |
| author_facet | Oumaima Barhoumi Mohamed H. Zaki Sofiene Tahar |
| author_sort | Oumaima Barhoumi |
| collection | DOAJ |
| description | Traffic conflict techniques enable a comprehensive assessment of traffic safety analysis. Formal methods allow the identification of factors that contribute to traffic safety issues and provide evidence of potential safety degradation. As such, formal methods provide a novel way to model traffic rules and verify road users' compliance. The paper proposes formalizing a traffic safety rule in differential dynamic logic and using KeYmaera theorem prover for verification. This rule considers time-to-collision (TTC), space headway (SHW), and shockwave speed (SWV). To validate the effectiveness of this rule in realistic traffic scenarios, we conducted a study using calibrated microsimulation data from the SR528 highway in Orlando, Florida. Our analysis examined the TTC, SHW, and SWV values for vehicle platoons on the highway and demonstrated how smaller TTC and SHW values indicate shockwaves and subsequent conflicts. Furthermore, we observed that shockwave speed could contribute to traffic conflicts by enabling evasive actions such as sudden braking or lane changes as the risk of collisions increases. By highlighting these findings, we aim to provide valuable insights into the real-world applicability of formal methods for traffic safety and their potential in promoting safer driving practices that can help create reliable autonomous vehicle control systems. |
| format | Article |
| id | doaj-art-d2d554db9cbd4fe3a01f512f86a9ee6c |
| institution | Kabale University |
| issn | 2644-1330 |
| language | English |
| publishDate | 2024-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Open Journal of Vehicular Technology |
| spelling | doaj-art-d2d554db9cbd4fe3a01f512f86a9ee6c2025-01-30T00:04:27ZengIEEEIEEE Open Journal of Vehicular Technology2644-13302024-01-01560661910.1109/OJVT.2024.338741410496854A Formal Approach to Road Safety Assessment Using Traffic Conflict TechniquesOumaima Barhoumi0https://orcid.org/0009-0009-1843-7925Mohamed H. Zaki1https://orcid.org/0000-0002-2970-2423Sofiene Tahar2https://orcid.org/0000-0002-5537-104XDepartment of Electrical and Computer Engineering, Concordia University, Montreal, QC, CanadaDepartment of Civil and Environmental Engineering, Western University, London, ON, CanadaDepartment of Electrical and Computer Engineering, Concordia University, Montreal, QC, CanadaTraffic conflict techniques enable a comprehensive assessment of traffic safety analysis. Formal methods allow the identification of factors that contribute to traffic safety issues and provide evidence of potential safety degradation. As such, formal methods provide a novel way to model traffic rules and verify road users' compliance. The paper proposes formalizing a traffic safety rule in differential dynamic logic and using KeYmaera theorem prover for verification. This rule considers time-to-collision (TTC), space headway (SHW), and shockwave speed (SWV). To validate the effectiveness of this rule in realistic traffic scenarios, we conducted a study using calibrated microsimulation data from the SR528 highway in Orlando, Florida. Our analysis examined the TTC, SHW, and SWV values for vehicle platoons on the highway and demonstrated how smaller TTC and SHW values indicate shockwaves and subsequent conflicts. Furthermore, we observed that shockwave speed could contribute to traffic conflicts by enabling evasive actions such as sudden braking or lane changes as the risk of collisions increases. By highlighting these findings, we aim to provide valuable insights into the real-world applicability of formal methods for traffic safety and their potential in promoting safer driving practices that can help create reliable autonomous vehicle control systems.https://ieeexplore.ieee.org/document/10496854/Transportation safetytime-to-collisionspace headwayshockwavesformal verification |
| spellingShingle | Oumaima Barhoumi Mohamed H. Zaki Sofiene Tahar A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques IEEE Open Journal of Vehicular Technology Transportation safety time-to-collision space headway shockwaves formal verification |
| title | A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques |
| title_full | A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques |
| title_fullStr | A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques |
| title_full_unstemmed | A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques |
| title_short | A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques |
| title_sort | formal approach to road safety assessment using traffic conflict techniques |
| topic | Transportation safety time-to-collision space headway shockwaves formal verification |
| url | https://ieeexplore.ieee.org/document/10496854/ |
| work_keys_str_mv | AT oumaimabarhoumi aformalapproachtoroadsafetyassessmentusingtrafficconflicttechniques AT mohamedhzaki aformalapproachtoroadsafetyassessmentusingtrafficconflicttechniques AT sofienetahar aformalapproachtoroadsafetyassessmentusingtrafficconflicttechniques AT oumaimabarhoumi formalapproachtoroadsafetyassessmentusingtrafficconflicttechniques AT mohamedhzaki formalapproachtoroadsafetyassessmentusingtrafficconflicttechniques AT sofienetahar formalapproachtoroadsafetyassessmentusingtrafficconflicttechniques |