# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
## 3 Methodology
### Unicast Routing Module for V2V Communication
The four primary components of the use case diagram are the system boundary, the actor, the association, and the use case; also, the use case diagram depicts the link between actors and use cases. Figure 6 shows a use case diagram that demonstrates the system's capabilities. The RSU, TA, hospital, vehicles, and emergency vehicles are the characters. RSUs are used to find emergency services if an emergency service is used to find emergency services. ## 6 Conclusion

In this paper, we have proposed a novel approach to the user's users and their interactions with the user's users. The user's users are able to find emergency services that are not only used in the user's users. The user's users are able to find emergency services that are not used in the user's users. The user's users are able to find



occurs, broadcast emergency messages, send a time alert message as well as remove all the entities after the rescue procedure is completed. Trusted authority (TA) is used to check the authorized entity in the system, including vehicles and hospitals. The hospital received an emergency occurrence message from RSU and then sent a rescue message to the emergency vehicle. After the rescue procedure is complete, it informs the RSU. The emergency vehicle is used to rescue the victims from the emergency occurrence location and then inform the hospital. ## 4 Formal Methods and Formal Specifications

The VDM-SL specification of the proposed Algorithm given below, in which different objects, operations, and functions described. ### Unicast Routing Module's Specifications for V2V Communication

The Vehicle_type, Veh_Speed, and Data_Packet are declared as enumeration types. The position declared as Point up and down declared as Bit and Id as a token. A composite object is MobileVehicle that has eight fields, i.e., Vehicle_IP, limit, R_Id, V_speed, Vehicle_type, Dist, packet, and Pos. Figure 6: Use case Diagram of Emergency Service Module. _types Bit = a intv BT == BT = 0 or BT = 1; a = int; b = int; Point = a*b; Road= real; Up=Bit; Pos = Point; Down = Bit; Lane = Up*Down; Ad _hoc_Net = Mobile_Vehicle*Mobile_Vehicle; Rdd= map Road to Lane; Net_Comm = seq of Ad_hoc_Net; Vehicle_type = <SOURCEVEHICLE>!! _<DESTINATIONVEHICLE>!! <RELAYED>; Data_Packet= <SENT>!! <REESND>!! <SEND>!! <DROPED>!! <RECEIVED>; Veh_Speed = <NORMAL>! <MAXIMUM>! <MINIMUM>; MobileVehicle :: Vehicle_IP_Add : seq of Bit limit : set of Point R_Id : seq of Bit V_Speed : Veh_Speed Vehicle_Type : Vehicle_type Dist : real packet : Data_Packet Pos : Point; ^Known Destination' has four fields i.e., Vehicle, L_link, Mobile_conn, and R_link which is a composite object. _KnownDestination :: Vehicle : set of Mobile_Vehicle L_link : set of Mobile_Vehicle Mobile_conn : seq of Ad_hoc_Net Mobile_conn : seq of Ad_hoc_Net R_link : set of Mobile_Vehicle;

VANET has three fields i.e., Vehicle, Mobile_conn, and Known_dest, which is a composite object, and the middle point is declared as a set of points. _VANET:: Vehicle : set of Mobile_Vehicle Mobile_conn : seq of Ad_hoc_Net Known_dest : Known_Destination inv mk_VANET(Vehicle, Mobile_conn,-) == forall Va, Vb in set Vehicle & exists Mnet in set elems Mobile_conn & Mnet = mk_( Va, Vb) and forall Mnet in set elems Mobile_conn & exists Va, Vb in set Vehicle & Mnet = mk_( Va, Vb); Middle_Point = set of Point inv _x =_forall mk_(a, b) in set x & mk_(a,b)_ = mk_(0,b) and exists mk_(a1,b1) in set x & mk_(a1,b1) = mk_(0,0);_

The formal specification of the system's state is shown below. The state incorporates all of the system's necessary attributes that will be used in the unicast process, and the state's invariant will be used to communicate. _state V2V_Unicast of netv : VANET scope : Net_Comm res : Data_Packet middle : Middle_Point nearer : set of MobileVehicle subnetbase : VANET nonearer: set of MobileVehicle pathreh : Net_Comm inv mk_V2V_Unicast(-,-,-,-,-,-) == KnownDestinationV2V () end_

There are various operations used in the unicast routing protocol.