The Responsive Traffic Signaling System Using Graph Theory and Vienna Development Method Specification Language (VDM-SL) is 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 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.
Traffic congestion has become a serious issue in large cities in terms of social, economic and environmental impact. Smart cities aim to continuously improve the lives of citizens in different aspects: transportation, health, education, energy, etc. As cities now become larger, congestion is increased due to rapid urbanization. The smart city is a combination of multiple components of a specific area that is automated to make a digital environment and all smart devices and tools related to a network. Traffic congestion has become a major problem because of the increasing population in huge cities around the world 
. Some crucial traffic problems include accidents and traffic jams that cause a waste of fuel, motor power, property damage, environmental pollution, health diseases, and a waste of time. Every day almost 3700 people are injured due to traffic signal-related accidents, and 1.35 million people die every year because of traffic rule violations, careless driving, and technical faults 
Existing traffic signalized intersections exhibit several problems, mostly due to fixed signal time intervals. No proper framework for emergency vehicles, such as pedestrians, car drivers, police, accidents, fire brigade, and rescue services, is currently available 
. Thus, these existing traffic signal systems failed to address traffic congestion problems efficiently. Due to the fixed clock cycle of red, green, and amber lights, vehicles need to wait at each traffic lane until the cycle is completed. In some cases, some vehicles must wait unnecessarily for the signal time of other lanes even if no traffic is occurring at the signals 
. Most vehicle drivers are aware of the traffic rules, but the system does not provide any support for a safe crossing signal, thereby resulting in road accidents.
Traffic signaling systems are one of the most important components of our daily routine.
There are severe problems with traffic congestion in urban areas due to lack of less efficient traffic signaling mechanisms. There is little work around traffic signaling systems in Formal methods and VDM-SL. Most traffic signaling systems are modeled with fixed time intervals in which no proper mechanism of emergency vehicles and safe crossing of pedestrians is provided at the signals.
Several possible solutions have been developed for traffic controls. However, improvements are still needed to overcome the issues in achieving efficiency at signals addressing responsive traffic monitoring and signaling system. In 
, public transport system estimation was presented based on license plate recognition (LPR) and cellphone location (CL) data. The use of several data sources, such as LPR and CL data, completely keeps the advantage of extreme level reporting and accuracy. Some disadvantages of CL data include the difficulty in estimating traffic flows. CL data keep focusing only on traffic state analysis, demand forecasting, and traffic zone. In 
, extraordinary resolution driving performance was utilized, and data are obtained through sensors from 303 drivers to monitor a driver’s performance at the path section at joint level.
2. Formal Modeling of Responsive Traffic Signaling System Using Graph Theory and VDM-SL
Herein modeled a Responsive Traffic monitoring and Signaling system using Unified Modeling Language (UML), Graph theory, WSAN, and VDM-SL formal method. Traffic communication and information collection play vital roles in transportation infrastructure. Unfortunately, most of the systems can only detect vehicle positions in a fixed manner, and their information collection task is only performed by communication and power supply cables, thereby leading to high construction costs. In another way, information collection and vehicle detection can be easily performed using WSAN because it provides the advantages of wireless distribution, flexibility without cables, and low energy consumption. The use of a wireless sensors network can solve many difficulties in traffic information collection systems 
. Traffic signal strategies are classified as fixed cycle and traffic responsive. For the responsive scheme, the traffic signaling systems can be improved to set the dynamic time interval of red, green, and amber lights according to the amount of waiting vehicles and pedestrians at the signalized intersection to improve efficiency. A traffic signal is assumed to depend on the next signal at an intersection to reduce time and fuel. When an emergency vehicle is detected, the controller will alert each lane to stop the flow of vehicles and display the red signals on all lanes to continue the flow of the emergency vehicle. The traffic flow at a signal is measured to set a responsive traffic signaling scheme by analyzing the intersection. When a controller detects any unintended pedestrian near zebra crossing, all the signals will be turned to red to inform the vehicles to stop so that pedestrians can cross the road safely.
A VDM-SL formal model is developed by integrating approaches for a responsive traffic monitoring and signaling system that enhances the efficiency of vehicles and increases safety at the traffic signals. This model will help make schedules between the occurrences of traffic signals in the targeted areas to provide a successful flow of vehicles across all traffic signal intersections. Our graph-based model is converted into a formal model through the VDM-SL. The proof of validation is provided by various facilities that are available in the VDM-SL toolbox 
. The formal specification is checked by type and syntax checkers, pretty printer, and integrity for validation of the system.
Figure 1 describes an abstract representation of a traffic signaling intersection. It displays different signalized intersections, cameras, traffic signals, emergency vehicles, primary vehicles, and other objects. The proposed specification is based on finding different locations of places, determining the shortest path toward the destination path in terms of distance and time, and identifying less traffic on the signalized intersection. For traffic jam or rush, dynamic information is provided to update the controller using signal intersection video cameras that take real-time video streaming and images of the traffic situation to find the shortest routes. The shortest route is estimated depending on two factors, namely, distance and time. For a real model, the shortest route has equal importance in terms of distance and time. The distance-dependent or time-dependent shortest route may be selected as required.
Abstract representation of Traffic Signalized Intersection.
3. System Architecture
System architectures refer to different design decisions nature-wise; these designs are mostly commercial and nontechnical decisions. In any system, designing the model through UML diagrams is important to meet the functional and nonfunctional requirements of the system.
Herein constructs an efficient traffic signaling and monitoring system with the integration of different approaches, including UML, graph theory, and VDM-SL formal methods, to improve the efficiency among signal intersections. Flow chart of the proposed techniques is presented as in Figure 2:
Figure 2. Flow chart of the proposed techniques.
3.1. UML Based Models
By using UML, herein will define how the signals will periodically update according to the real-time conditions of the roads and how the signals depend on each other at the intersection. We modeled our system using various diagrams, such as use case and Sequences.
Different types of diagrams are designed, and the details are given below:
Use cases are a set of different types of scenarios that define the interaction between a system and a user. The two major components of a use case include actors and use cases.
Sequence diagrams model the behavior of systems by defining the way in which multiple objects interact with each other to achieve the goals. The sequence diagrams are read in ascending and descending order. In a traffic system, all the modules are required to work online. As such, any system can send requests at any time. An information system always has a strong behavior. Therefore, some behavior of this work is complete in the sequence direction. Thus, this kind of diagram is known as the sequence diagram.
Figure 3 displays the extended use case diagram and defines all the details of this system, which includes five actors. They are all detectors that are detecting the current situation on the traffic signals. Traffic controllers are continuously monitoring and taking decisions based on the current traffic flow. Traffic detectors detect all situations on the road and pass information to the controller. Storehouse stores the details about the detectors, vehicles, pedestrians, and emergency vehicles. Pedestrians and primary vehicle drivers will know the real-time road condition of signals and then decide whether to pass over the lane and/or wait for the other signals.
Extended use case.
Figure 4 shows an object of primary vehicles that crosses the detector. The detector will detect all vehicles and count the vehicles at every lane. Subsequently, the detector sends the current traffic situation to the traffic controller for future actions. Sensors are sending and receiving information at the parallel time. In this way, it identifies the current flow of traffic with the help of detector sensors.
Sequence Diagram for Primary Vehicles.
The traffic controller collects all the information, analyzes this received information, and sends the traffic flow to the traffic optimizer. After completing all processes, the traffic controller sets the signal and responsive time at numerous vehicles’ lane. Primary vehicles check the signal and follow the time to cross the road. According to dynamic time, two lanes can possibly have different times to cross the vehicles by counting the vehicles at every lane, and the remaining lane must be stopped.
Figure 5 shows when objects of primary and emergency vehicles cross the detector. The detector detects the emergency vehicle lane at this time and will send data to the controller for further actions. The controller collects all information from detectors and passes current traffic information to the optimizer, which optimizes and sends the received data back to the controller. The traffic controller sets the responsive time on the signalized intersection at a specific lane. Priority is awarded to emergency vehicles, such as fire brigades, police, and ambulance, by turning signals in nearly all vehicle lanes, except lanes where emergency vehicles are crossing, into red. Other primary vehicles must stop because the emergency vehicle may pass in any lanes.
Sequence Diagram for Emergency Vehicle.
Figure 6 shows when the pedestrians will reach the footpath; detectors will act as cameras and sensors that detect the pedestrians, send information to the traffic controller, detect all pedestrians, and count the pedestrians at every lane. Next, the detectors send the current traffic situation to the traffic optimizer for future actions.
Sequence Diagram for Pedestrians.