# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
## 3 Methodology
### Unicast Routing Module for V2V Communication  
A data packet that can be easily transmitted from only one source to a single target in a network is known as unicast communication. With known destination topology, the developed protocol handles unicast mode, which means that the destination's position is known and determined using partitioning. In the case of V2V communication, there are several options for a destination spot. The choices for V2V communication utilizing unicast protocol are as follows: (1) In source vehicle as well as a destination vehicle in the single subnet either left subnet or in the right subnet. (2) If the source and destination cars are on different subnets, the destination vehicle must be in the right subnet if the source is in the left, and vice versa. Figure 3 shows the above-mentioned scenarios. In case 1 scenario 'a', relay node establishes wireless connections between the source and destination nodes by carrying packets from the source and passing them on to the destination. Since the destination node's location is identified, only certain nodes with the same lane flags as the destination vehicle are involved. In Figure 3 case 2 scenario 'b', depicts V2V communication between the source node as well as the target node in the two halves of the network via a head node. We will show you how to choose a head vehicle. In scenario two, the head node creates several zones to pick a peripheral and found target vehicle. Figure 3: V2V Communication, Unicast Scenarios of (**a**) and (**b**) Cases. Figure 2: The Flow of System Methodology. The given Algorithm 1 demonstrates a procedure about how to communicate a vehicle with another vehicle in a network called VANETs. The unicast procedure's algorithm is seen below. The algorithm's first step is to set up the proposed topology for the vertically partitioned network. The addresses of the vehicles engaged in the correspondence are then updated in the'str' and 'dest' variables. \"Vehicle-Direction\" would be labeled for both the source and destination vehicles to determine their location. The source vehicle will use \"Neighbour-Search\" to decide if the source and destination vehicles are in the single subnet. If the \"Neighbour-Search\" function returns TRUE, a 2-hop scope is established, then the destination is searched within the scope, and if the destination vehicle is located in the scope, the path from source to destination is registered, as well as an acknowledged message is sent to the root vehicle that is the start point. If the destination vehicle is not identified in the scopes, a peripheral vehicle is selected at the edge of the previous scope and makes a loop on the procedure mentioned in the seventh point until the destination is not found. If the algorithm \"Neighbour-Search\" returns FALSE, the head is a car that is heading into the middle. If the target vehicle is in the left subnet, a scope is generated for that subnet, and if the destination is located within that scope, the route is registered, and an acknowledged message is received. If the destination cannot be found within that scope, step 17 will be repeated before the destination can no longer be found. ```
1. Procedure Unicast
2. Input: V2V Comm (Communication)
3. if Vchl Comm Vkh2 then
4. Str \(\leftarrow\) Vchl & Dest \(\leftarrow\) Vkh2
5. Vehicle-Direction (KDT, Str, VB, Middle) & Vehicle-Direction (KDT, Dest, VL, Middle)
6. Neighbour-Search (Str, Dest, L, S, R_S)
7. if Neighbour-Search (Str, Dest, L, S, R_S) == TRUE
8. 2H- Zone-Creation (Str, Subnet)
9. Scope-Destination-Srch(Dest, Scope)
10. if Scope-Destination-Srch (Dest, Scope) == TRUE
11. Save-Path (Dest, Str, Scope)
12. Acknowledged(Path)
13. EXIT
14. elseif Scope-Destination-Srch (Dest, Scope) == FALSE
15. Choose-Peri-Veh (Scope)
16. Loop from step 8 to step 9
17. if Neighbour-Search (Str, Dest, L, S, R_S) == FALSE
18. Choose-Head (Str, Middle)
19. Move hto to Middle
20. ifStr in set L_S
21. 2H_Zone-Creation (hr, R_S)
22. if Scope-Destination-Srch (Dest, Scope) == TRUE
23. Save-Path (Dest, Str, Scope)
24.