# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
## 6 Conclusions  
The internet of things (IoT) is an application of smart nodes in a network that detects, interprets, processes as well as reacts to data within the time needed. In vehicular ad hoc networks, the suggested approach takes into consideration human and automobile activity. It also ensures a constant flow of traffic, which not only decreases fuel use but also improves living standards. The bulk of current research on algorithm performance analysis depends on testing and simulation-based techniques, which may not guarantee correctness. This study's formal approaches are more effective in confirming the model's correctness. The VDM-SL is used to improve the specification's accuracy and to do a thorough analytical assessment [48]. VSM-SL also has an important interaction with graph theory and UML diagrams. This is due to the fact that graph-based and UML models were simple to convert into formal models. The unicast procedure also described in which  
\begin{table}
\begin{tabular}{c c c c c} \hline \hline
**Composite** & **Operations and** & **Syntax Check** & **Type Check** & **Pretty Print** \\ \hline \multirow{3}{*}{MobileVehicle} & VehicleDirection & ✓ & ✓ & ✓ \\  & NeighborSrch & ✓ & ✓ & ✓ \\  & NetRange & ✓ & ✓ & ✓ \\ \hline \multirow{3}{*}{KnownDestination} & ZoneNetCreation & ✓ & ✓ & ✓ \\  & ZoneDestinationSrch & ✓ & ✓ & ✓ \\  & ChoosePeriVehZone & ✓ & ✓ & ✓ \\ \hline \multirow{3}{*}{VANET} & ChooseHeadVehicle & ✓ & ✓ & ✓ \\  & Save Path & ✓ & ✓ & ✓ \\ \hline \multirow{2}{*}{Time} & Acknowledged & ✓ & ✓ & ✓ \\  & KnownDestinationV2V & ✓ & ✓ & ✓ \\ \hline \hline \end{tabular}
\end{table}
Table 2: Results of Unicast Module.  
\begin{table}
\begin{tabular}{c c c c} \hline \hline
**Composite Objects** & **Operations and Functions** & **Syntax Check** & **Type Check** & **Pretty Print** \\ \hline Emergency & HospitalRegistration & ✓ & ✓ & ✓ \\ Hospital & RemovedRegisteredHospital & ✓ & ✓ & ✓ \\ Sensors & VehicleRegistration & ✓ & ✓ & ✓ \\ FogBasedRSU & RemovedRegisteredVehicle & ✓ & ✓ & ✓ \\ Message & isHospitalRegistered & ✓ & ✓ & ✓ \\ Time & isVehicleRegistered & ✓ & ✓ & ✓ \\ Vehicle & getNoOrRegisteredEnterVehicle & ✓ & ✓ & ✓ \\ FogCloud & getNoOrRegisteredVehicle & ✓ & ✓ & ✓ \\ TrustedAuthority & SetSensorsOnRSU & ✓ & ✓ & ✓ \\  & EmergencyAlertMsg & ✓ & ✓ & ✓ \\  & SendTrafficData & ✓ & ✓ & ✓ \\  & TimeAlert & ✓ & ✓ & ✓ \\  & GetInfoForRescueVictim & ✓ & ✓ & ✓ \\  & NewEmergencyDet & ✓ & ✓ & ✓ \\  & getEmergency & ✓ & ✓ & ✓ \\  & ViewCloudDataByTA & ✓ & ✓ & ✓ \\  & BroadcastEmergencyMsg & ✓ & ✓ & ✓ \\ \hline \hline \end{tabular}
\end{table}
Table 3: Results of Emergency Service Module.  
vehicle-to-vehicle communication was discussed formally. We have utilized the formal techniques VDM-SL approach to ensure the system's correctness. It has been observed that formal techniques are a more dependable and tangible approach to system development than other approaches because formal methods allow for the investigation of problems at an early stage in the system's development. It raises and improves the system's quality and bridges the semantic gap between system design and implementation.