# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
### Contribution  
In this paper, we will propose an IoT-based formal model for vehicle-life interaction in VANETs using VDM-SL, which provide emergency services by the arrival of an emergency vehicle at accident locations. Wireless sensors will be used to monitor the real-time situation, and actors will be used to perform actions as required, minimizing the average waiting time, reducing the traffic congestion issues and making communication effective by usingIoT. Further, a unicast routing protocol is utilized to convey messages from the source to destination vehicles. The proposed system is utilized different approaches such as; IoT, Graph theory, Unified Modeling Language (UML), and formal methods with the proof of concept. UML diagram is utilized to portray the system's requirements comprehensively. The developed graph-based model was utilized to present the network as well as the appropriate route. The formal methods are mathematical techniques supported by many tools that offer effective ways to model, design, and analyze the system. The formal methods in terms of VDM-SL (Vienna Development Method-Specification Language) are used to define the formal modeling of the system in a systematic way, and the VDM-SL toolbox is utilized to provide the validation as well as verification of the model [10].  
An abstract representation of the system is described in Figure 1. It displays different techniques such as VANETs, IoT, UML diagrams, graph-based models and formal methods that we have used in our system. It shows the emergency services by the arrival of an emergency vehicle at accident locations. Moreover, our fog-based strategy encompasses objects such as emergency vehicles, hospitals, RSUs, automobiles, and others who are directly or indirectly related to fog-enabled RSUs in order to give improved comfort, safety, and smooth driving. Our fog-based RSU provides emergency services like mobile RSU. It will be covered most road sections as much as possible in cities and on highways between cities. IoT will be adopted in which sensors will be used to monitor the real-time environment, and actors will be used to take action in case of any emergency. This work is displayed in Figure 1 by utilizing the emergency service module diagram as well as the UML diagram. It also represents the unicast scenarios for simple V2V communication, there are several options for a destination spot, but two of them are utilized in our system. Further, this work represents a unicast routing module diagram and graph-based model, which describe the behavior of the module. After this, these models easily translated into a formal model using VDM-SL. The VDM-SL toolbox will be used to convert the formal model into a validated model.  
Figure 1: Abstract Representation of the System.  
The following are the key contributions of this paper:  
1. We adopt a fog-based protocol and specify this protocol in a formal method approach, which provides emergency services with the arrival of an emergency vehicle at accident locations. II. We also adopt a unicast routing protocol to send a message from one vehicle to another, which is focused on V2V communication. III. The network of V2V communication will be represented using graph theory. IV. Unified Modeling Language (UML) is utilized to model and capture different components of a system. V. The formal language VDM-SL is utilized to provide the specification of the system, and a VDM-SL toolbox is used to check the validation of the proposed model.  
The rest of this paper is organized as follows. In Section 2, we present the related work. We proposed system methodology and algorithms in Section 3. Section 4 presents the formal methods and formal specifications of the system. The model analysis is provided in Section 5. The conclusion of this paper is presented in Section 6. Some future challenges are present in Section 7.