# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
## 3 Methodology
### Emergency Service Module's Specifications
_state EmergencyMsg_RescueVictim of vehicle: map Id to Vehicle traffic_video: map Id to Camera rsin: map Id to FogBasedRSU location: map Sensors to Loc trusted_authority: map Id to TrustedAuthority Rsusensor : map Id to FogBasedRSU hospital : map Id to Hospital fogcloud: map Id to FogCloud sensors : set of Sensor currentlocation: set of Loc get_info_anyMiscellaneous: map Sensors to Sensor_info_anyMiscellaneous any_emergency: set of isAny_Emergency emergency_list: map Id to Emergency init EM=EM=mk_EmergencyMsg_RescueVictim({!->},{!->},{! The formal specification of the 'Vehicle Registration' operation consists of two parameters vehicle id and vehicle type. Pre_condition: we have used the dom operator to check that the vehicle Id, which we take as an input, is not in the domain of the vehicle map. Post_condition: use the union operator to add the pair of vehicle id and type in the map. _VehicleRegistration(inputId: Id, typeh: Vehicle_Type) ext wr vehicle: map Id to Vehicle pre inputId not in set dom vehicle post vehicle = vehicle \(\sim\) municipal inputId!\(\sim\) mk_Vehicle(inputId, typeh, {!->},{[1!->})]);_  
The formal specification of the 'Remove Registered Vehicle' operation consists of one parameter, which is vehicle id. Pre_condition: used the dom operator to check that the vehicle Id which we take as input has to be in the domain of the vehicle map. Post_condition: we have used the domain deletion operator. _RemoveRegisteredVehicle(inputId: Id) ext wr vehicle: map Id to Vehicle pre inputId in set dom vehicle post vehicle =[ inputId]!\(<\)-: vehicle \(\sim\);_  
The 'isHospital Registered' operation checks whether or not the hospital is registered. _isHospitalRegistered(idInt: Id) Result : bool ext rd hospital : map Id to Hospital pre true post Result \(<=>\) hosln in set dom hospital;_  
The 'isVehicle Registered' operation checks whether or not the vehicle is registered. _isVehicleRegistered(idInt: Id) Result : bool ext rd vehicle: map Id to Vehicle pre true post Result \(<=>\) idln in set dom vehicle;_  
This operation gave us the exact number of emergency vehicles that are registered. _getNoOfRegisteredCenter_Vehicle() Result: nat ext rd vehicle: map Id to Vehicle pre true post Result = card (ev 1 ev in set mg vehicle & ev.Veh_Type =\(<\)EMERGENCYVEHICLE\(>\));_  
This operation is also available to check the connected vehicles that are registered. _getNoOfRegisteredVehicle() Result: nat ext rd vehicle: map Id to Vehicle pre true post Result = card (tv 1 v in set mg vehicle & ev.Veh_Type =\(<\)VEHICLE\(>\));_  
'Set Sensors On RSU' operation is used to monitor the vehicles. This operation takes a sensor as well as a location as an input where we have to set the sensor on RSU. Pre_condition: used to check the sensor, which we take as an input, is not in the domain of the location map. Post_condition: when the pre-condition is true, then the sensor place in the mapping by using set notation. ```
SetSensorsOnRSU(inputS:Sensors, locIn: Loc) ext wr location: map Sensors to Loc wr sensors : set of Sensor pre inputS not in set dom location post location= location municipal inputS |-> locIn };
```  
The 'Emergency AlertMsg' operation is used to sense the emergency conditions from VANETs, and the emergency alert message is sent to the other RSUs and vehicles. ```
EmergencyAlertMsg() ext wr vehicle: map Id to Vehicle rd Rsusensor: map Id to FogBasedRSU wr rsu: map Id to FogBasedRSU wr hospital: map Id to Hospital wr fogcloud: map Id to FogCloud pre true post exists msg in set dom fogcloud & fogcloud (msg).Msgalert = Rsusensor and vehicle (msg).Msgalert = Rsusensor and rsu (msg).Msgalert = Rsusensor;
```  
The 'Send Traffic Data' operation is used to send the video of the traffic as well as emergency conditions to the cloud for further use. ```
SendTrafficData() ext rd traffic_video: map Id to Camera wr fogcloud: map Id to FogCloud pre true post exists rd in set dom fogcloud & fogcloud (vd).