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. One of the proposed solutions is traffic monitoring systems which collect and analyze traffic data for the safe operation and management of the overall system. Even though traffic safety analysis has been tied to crash data, surrogate safety measures (SSM) have recently emerged as a replacement. SSM can provide a convenient alternative for understanding the impact of conflicts on overall road safety. Traditionally, conflicts were studied through manual methods that are time-consuming and prone to biases. With the onset of new technologies such as automated video techniques, micro-simulation and Vehicular ad-hoc Networks researchers are adopting statistical and machine learning methods for developing reliable indicators for possible traffic crashes. However, these technologies don't provide high-level reasoning about the overall state of the traffic. 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 system 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, maintaining appropriate headway, and performing safe lane-change maneuvers. The framework is tested using a calibrated micro-simulated highway scenario and offline monitoring is applied to individual vehicle trajectories to check 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.


If this is your thesis or dissertation, and want to learn how to access it or for more information about readership statistics, contact us at STARS@ucf.edu.

Graduation Date





Zaki Hussein, Mohamed


Master of Science (M.S.)


College of Engineering and Computer Science


Civil, Environmental, and Construction Engineering

Degree Program

Civil Engineering; Smart Cities







Release Date

May 2021

Length of Campus-only Access


Access Status

Masters Thesis (Open Access)