# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
## 2 Related Work
### Literature Review of Formal Methods  
The formal methods are implemented in different areas of life to measure the model accuracy as well as increase the efficiency of the model. In life-critical tasks, formal methods provide the errors free model before the implementation of the system model in a real-time environment. Formal methods utilized in every life-critical task such as border protection system [38] in which the authors proposed wireless sensors and actor networks (WSANs)-utilizing formal methods, railway interlocking system [39], in which formal analysis of safety properties are presents about moving block interlocking, the authors proposed smart healthcare system utilizing formal methods [40], and guidance system with intelligent traffic monitoring system [41] also utilized formal methods. In Refs. [42; 43], the authors proposed MAHSNs that used VDM-SL to show the working of the system as well as verify the accuracy of the model. In Ref. [35], the authors suggested a smart algorithm for an efficient, structured unicast routing protocol. The authors only focused on V2V communication, not on V2I communication. In Ref. [44], the authors used VDM-SL \begin{table}
\begin{tabular}{c c c c c c} \hline \hline
**Reference** & **Year** & **Tools/Approaches** &
\begin{tabular}{c} **Advantages of** \\ **Methods** \\ \end{tabular} & **Description** & **Disadvantages and Limitations** \\ \hline
[29] & 2015 & NS-2 & \begin{tabular}{c} • Results can be \\ quickly obtained more \\ ideas can be tested easily \\ in shortest time \\ \end{tabular} & \
\begin{tabular}{c} • In VANET cluster \\ delivered the emergency \\ alert message in shortest \\ time. \\ \end{tabular} &
\begin{tabular}{c} • No Formal verification and \\ validation \\ \(\bullet\) Bugs are unreliable and to \\ model real system is complicated \\ \end{tabular} \\ \hline
[30] & 2015 & \begin{tabular}{c} • Centralized \\ management for \\ network \\ \end{tabular} & \
\begin{tabular}{c} • Create a framework \\ for VANETs which is \\ beneficial for both \\ fog-computing and SDN \\ \end{tabular} &
\begin{tabular}{c} • Formal verification and \\ validation is not provided \\ • Significant amount of latency \\ and lake in maintenance \\ \end{tabular} \\ \hline
[31] & 2015 & \begin{tabular}{c} SUMO NS-2 \\ MOVE \\ \end{tabular} & \begin{tabular}{c} • Not required costly \\ equipments and easily \\ tested in short time \\ \end{tabular} & \
\begin{tabular}{c} • Reached emergency \\ vehicle at shortest time \\ • Delivered message \\ from emergency vehicle \\ to traffic signal \\ \end{tabular} &
\begin{tabular}{c} • No comparative performance \\ • Simulation based and not find \\ the correctness of the system \\ model \\ Complicated structure, lightly \\ maintained and not seen \\ significant development \\ \end{tabular} \\ \hline
[32] & 2019 & \begin{tabular}{c} NS-2, \\ VanetMobiSim \\ \end{tabular} & \begin{tabular}{c} • Support multiple \\ protocols and many \\ algorithms support in \\ routing and queuing \\ \end{tabular} & \
\begin{tabular}{c} • Multi-hop-clustering \\ approach is proposed by \\ using BFS algorithm \\ • Improve the \\ VANET’s performance \\ Minimize the rate of \\ message control \\ \end{tabular} &
\begin{tabular}{c} • Simulation based \\ • Not calculate the accuracy of \\ the model utilizing formal \\ methods \\ • Complicated structure and \\ unreliable bugs \\ \end{tabular} \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Cont. to model and monitor the AODV traffic-based flooding mechanism for mobile ad hoc networks systems. In the field of software engineering, system validation is a major problem. There is a danger of loss of life if there is an error in the safety and security crucial system's specification. In most earlier studies, costly computer-based simulation approaches were utilized to assess models. Simulation approaches fall short of establishing a model's total accuracy because the number of test cases necessary to achieve the appropriate degree of confidence grows exponentially.