2021/10/12 by Mariam Nour, Nour, Mariam, Mohamed H. Zaki +1
Computer Science · Engineering · #Computer science #Computers and Society (cs.CY) #Engineering #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Methods in Verification #Formal methods #Headway #Intelligent transportation system #Programming language #Real-time computing #Simulation #Software engineering #Specification language #Systems and Control (eess.SY) #Temporal logic #Traffic control and management #Transport engineering #Vehicular Ad Hoc Networks (VANETs) #cs.CY #cs.SY #eess.SY #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.2110.06208
published in arXiv (Cornell University) (Cornell University)
arxiv created 2021/10/12 · openalex publication_date 2021/10/12 · arxiv updated 2021/10/13 · openalex created_date 2021/10/25 · openalex updated_date 2026/07/28
Smart cities are revolutionizing the transportation infrastructure by the integration of technology. However, ensuring that various transportation system components are operating as expected and in a safe manner is a great challenge. In this work, we propose the use of formal methods as a means to specify and reason about the traffic network's complex properties. Formal methods provide a flexible tool to define the safe operation of the traffic network by capturing non-conforming behavior, exploring various possible states of the traffic scene, and detecting any inconsistencies within it. Hence, we develop specification-based monitoring for the analysis of traffic networks using the formal language, Signal Temporal Logic. We develop monitors that identify safety-related behavior such as conforming to speed limits and maintaining appropriate headway. The framework is tested using a calibrated micro-simulated highway scenario and offline specification-based monitoring is applied to individual vehicle trajectories to understand whether they violate or satisfy the defined safety specifications. Statistical analysis of the outputs show that our approach can differentiate violating from conforming vehicle trajectories based on the defined specifications. This work can be utilized by traffic management centers to study the traffic stream properties, identify possible hazards, and provide valuable feedback for automating the traffic monitoring systems.