# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
## 3 Methodology
### Unicast Routing Module for V2V Communication
In known destination topologies, the vehicle direction operation is used to change the vehicle's position in the header. Vehicle Direction operation is used to find the exact as well as current location in V2V communication. operations VehicleDirection(Veh : MobileVehicle, netw : VANET, middle : Middle_Point) Path : Lane pre true post (Veh in set netw. KnownDestination. L_link union netw. KnownDestination. R_link and exists Veh in set netw. KnownDestination. L_link & Veh.Pos in set middle and Path = mk_(1,0)) or (Veh in set netw. KnownDestination. Vehicle and exists Veh in set netw. KnownDestination. L_link & Veh.Pos not in set middle and Path = mk_(0,1)) or (Veh in set netw. KnownDestination. Vehicle and exists Veh in set netw. KnownDestination. R_link & Veh.Pos in set middle and Path = mk_(1,0)) or (Veh in set netw. KnownDestination. Vehicle and exists Veh in set netw. KnownDestination. R_link & Veh.Pos not in set middle and Path = mk_(0,1));
```
The 'Neighbor Search' operation is utilized to search for a source as well as a destination in which the source and destination are scanned to see whether they are in the same subnet or not. When the start node and target node both are in the same subnet (it may be right subnet or left subnet), then the algorithm will return true; otherwise, it will return false. ```
NeighborSrch (str : MobileVehicle, dest : MobileVehicle, netw : KnownDestination) output : bool pre true post output <=> (str in set netw. L_link and dest in set netw. L_link) or (str in set netw. R_link and dest in set netw. R_link);
```
The function NetRange determines which of the input node's neighbors are within its coverage. ```
NetRange(V : MobileVehicle, netw : VANET) Y : set of MobileVehicle pre true postforally in set netw. KnownDestination.Vehicle & y.Pos in set V.limit and Y = {y};
```
The protocol for creating a zone is defined in this algorithm. For this routing method, a two-hop scope creation is proposed. The method returns a scope, which is a collection of connections connecting a vehicle to all of its neighbours within its two-hop radius. ```
ZoneNetCreation(Veh : MobileVehicle, netw : VANET, nearer : set of MobileVehicle, nonarer : set of MobileVehicle) scope : Net_Conn pre true post nearer = NetRange(Veh, netw) and foall y in set nearer & exists conn1 in set elem netw.Mobile_conn & conn1 = mk_( Veh, y) and Veh.Vehicle_IP_Add <> y.Vehicle_IP_Add and foall y in set nearer & nonarer = NetRange(y,netw) and foall y in set nonarer & exists conn2 in set elem netw.Mobile_conn & conn2 = mk_(y,y) and y.Vehicle_IP_Add <> y.Vehicle_IP_Add and scope = [conn1, conn2];
```
When the destination vehicle exists in the scope, then the below Zone Destination Search function returns true; otherwise, it returns false. ```
ZoneDestinationSrch(dest : MobileVehicle, Zon : Net_Conn) Output: bool pre true post Output <=> exists mk_(Veh1,Veh2) in set elems Zon & (Veh1= dest) or (Veh2=dest);
```  
A scope/zone is passed as an input to the peripheral selection function, which returns a vehicle at the scope's limit as an output. The peripheral node is a node at the zone's edge that creates a two-hop scope around the destination node if it is not included in the scope. This vehicle must have a link to the source or be inside the domain, according to the method's first point. Then, because it will be in that scope for a longer period of time, the slowest car will be chosen as a peripheral. _ChoosePeriVehZone_(_dest : MobileVehicle_, _Zon : Net_Com,netw : VANET,middle : Middle_Point_) _peri : MobileVehicle_ _pre true_ _post_ _forall mk_(Veh1, Veh2) in set elems Zon & Veh1.Vehicle_Type =<SOURCEVEHICLE>_ and Veh2.Vehicle_Type = <RELAYED>_ and forall mk_(Veh2,pv) in set elems Zon & Veh2.Vehicle_Type_ =<RELAYED>_ and pv.Vehicle_Type <> <DESTINATIONVEHICLE>_ and pv.V_Speed = <MINIMIMM>_ and VehicleDirection (pv,netw,middle) = VehicleDirection(dest, netw, middle) and peri = pv;_  
When the start node and target vehicle are not in the single subnet, the head vehicle selection function is employed.