Formal Modeling of Responsive Traffic Signaling System Using Graph Theory and VDM-SL

Internet of things (IoT) is playing a major role in smart cities to make a digital environment. Traffic congestion is a serious road issue because of an increasing number of vehicles in urban areas. Some crucial traffic problems include accidents and traffic jams that cause waste of fuel, health dis...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Afifa Nawaz, Nazir Ahmad Zafar, Eman H. Alkhammash
Formato: article
Lenguaje:EN
Publicado: MDPI AG 2021
Materias:
Acceso en línea:https://doaj.org/article/0b6593ca30d14346a59566ca2b96aac4
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
Descripción
Sumario:Internet of things (IoT) is playing a major role in smart cities to make a digital environment. Traffic congestion is a serious road issue because of an increasing number of vehicles in urban areas. Some crucial traffic problems include accidents and traffic jams that cause waste of fuel, health diseases, and a waste of time. Present traffic signaling systems are not efficient in resolving congestion problems because of the lack of traffic signals. Nowadays, traffic signaling systems are modeled with fixed time intervals in which no proper mechanism for emergency vehicles is available. Such traffic mechanisms failed to deal with traffic problems effectively. The major objective is to establish a robust traffic monitoring and signaling system that improves signal efficiency by providing a responsive scheme; appropriate routes; a mechanism for emergency vehicles and pedestrians in real-time using Vienna Development Method Specification Language (VDM-SL) formal method and graph theory. A formal model is constructed by considering objects, such as wireless sensors and cameras that are used for collecting information. Graph theory is used to represent the network and find appropriate routes. Unified Modeling Language is used to design the system requirements. The graph-based framework is converted into a formal model by using VDM-SL. The model has been validated and analyzed using many facilities available in the VDM-SL toolbox.