# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
## 3 Methodology
### Unicast Routing Module for V2V Communication
Acknowledged(Path)
25. EXIT
26. elseif Scope-Destination-Srch (Dest, Scope) == FALSE
27. Choose-Peri-Veh(Scope)
28. Loop from step 21 to step 26
29. elseif Str in set R_S
30. 2H_Zone_Creation (hr, L,S)
31. if Scope-Destination-Srch (Dest, Scope) == TRUE
32. Save-Path (Dest, Str, Scope)
33. Acknowledged(Path)
34. EXIT
35. elseif Scope-Destination-Srch (Dest, Scope) == FALSE
36. Choose_Peri_Veh(Scope)
37. Loop from step 31 to step 35 Graph Theory Model of Unicast Module in V2V Communication

The complete network is represented using graph theory, as well as to create structural models. It depicted the whole network of unicast routing modules (nodes) and the connection of things (edges) to build a network. Figure 4 shows how graph-based topology improves the speed efficiency of vehicles between source and destination junctions, allowing each vehicle to reach its destination without wasting time, delays, or fuel. This model shows the two scenarios of V2V communication (scenario 'a' and scenario 'b'). In first scenario both source and destination in a single subnet. They can communicate easily without involving any head node. However, in the other scenario of the unicast module, both source and destination vehicles at the different subnet via a head node. We will show you how to choose a head vehicle. In scenario two, the head node creates several zones to pick a peripheral and found target vehicle. VDM-SL may also be used to turn a graph-based model into a formal model. ### Emergency Service Module

The warning alert is broadcast to the closest fog-based RSU as well as the vehicle in the situation of any emergency occurrence. Fog-based RSU sent an emergency alert to the hospital, along with path and location information. The hospital then double-checks its services before sending a rescue call to the emergency vehicle. The ambulance vehicle examines the direction as well as the destination ID and route information for the crash. Figure 5 depicts the fog-based RSU's message distribution. The fog-based RSU has sent out

Figure 4: Graph-based Model of Unicast Topology of Two Cases (**a**) and (**b**). an alert message to other fog-based RSUs and the vehicles, instructing them to change their routes so that the path could be safe for the arriving emergency car to arrive on time at the crash scene and rescue the victims. This further decreases the possibility of future mishaps. When an emergency/accident happens, Algorithm 2 sends out an emergency response and checks the message from it. If the message is classified as an emergency, the fog-based RSU sends a message to the other fog-based RSUs. Other drivers can quickly change lanes as a result of this, and it also unicasts a warning to the registered ambulance and then alerts the emergency vehicle to save the patients. After the rescue procedure, the fog-based RSU received a message from the hospital. Then the fog-based RSU shows the normal flow of traffic by removing all entities. The formal method in terms of the VDM-SL is utilized to define the system formally, and the VDM-SL toolbox will be used to describe validation and analysis of the proposed model in given sections. ### UML Based Model of Emergency Service Module

The Unified Modeling Language (UML) is widely used, and it contains a semi-formal style that may be used to depict system requirements in detail. At the beginning of the development process, the UML is the recommended modeling language for system portrayal. It is possible to achieve first stage model functional performance evaluation using UML and formal models by combining formal techniques and formal models with UML. If the erroneous system performance is not handled quickly, it can lead to a slew of additional issues that obstruct system function and, as a consequence, the system ends up costing a lot of money. Figure 5: Emergency Case scenario. Using the UML, a use case diagram may describe the specifics of the system's users and their interactions with it.