# Efficient IoT-Based Formal Model for Vehicle-Life Interaction in VANETs Using VDM-SL
## 3 Methodology
### Emergency Service Module's Specifications  
VDM-SL is used to formalize the functionality as well as the specification of emergency messages broadcast by fog-RSU. VDM-SL, a well-known modeling and specification language, is used to specify its properties. The Emergency_type and Sensor_info_anyMiscellaneous are declared as enumeration types. Name, emergency location, isemergency and location declared as token and Id as a string. The hospital is a composite object with four fields: hospital id, name, location, and message alert. ```
types Name=token; String = seq of char; Id= String; Loc = token; Emergency_Loc = token; isAny_Emergency = token; Emergency_type = <FIRE> | <MEDICAL> | <OTHER>; Sensor_info_anyMiscellaneous= <EMEGENCYLOCATION>| <EMEGENCYTYPE>; Hospital := Hos_id : Id Has_name : Name : Name  Hos_loc : Loc  Msgalert : map Id to FogBasedRSUI inv mk_Hospital(i, -, -, -)= len i <= 8;
```  
The emergency object is a composite object with three fields, namely, emergency recorded, emergency location, and type. The invariant was also used, which defined the number of emergencies if they occurred. When an emergency occurs, it must check the location and type of emergency. **Emergency: Emergency_recorded:ld**  
_E_location: set of Emergency_Loc_  
_E_type: set of Emergency_type_  
_inv mk_Emergency(-,Le,Lt)== (card(Le) = card(Lt)) and ((!<MEDICAL>] subset Lt \ |<FIRE>) \ {<OTHER>} or [<FIRE>] subset Lt \ |<MEDICAL>| {<OTHER>} or [<OTHER>] subset Lt \ |<MEDICAL>| {<FIRE>} and [<MEDICAL>,<FIRE>,<OTHER> ] inter Lt < |);_  
Sensors, FogBasedRSU, Message and Time also defined as composite objects which have different number of fields. _Sensor :: S.Id: Id S_monitoring: set of Vehicle; Msg_sent=<SENT_MSG_RSU>|<SENT_MSG_VEHICLE>|<SENT_MSG_HOSPITAL>|<SENT_MSG_EMERGENCYVEHICLE>; FogBasedRSU:: rsu_ld: Id sensors: Sensors broadcastMsg: MSg_sent Msgalert: map Id to FogBasedRSU Time_altr: map Id to FogBasedRSU; Message: RSU_id: FogBasedRSU_Msg_type: Emergency; Hours= nat: Mint= nat; Sec= nat; Time:: hours: Hours emit: Mint sec: Sec;_  
Enumeration types are specified for Vehicle_Type. The vehicle object is defined as a composite object with three fields: vehicle id, vehicle type, and message alert. _Vehicle_Type= <EMERGENCYVEHICLE>|<VEHICLE>; Vehicle :: T_Id: Id Velt_Type: Vehicle_Type Msgalert: map Id to FogBasedRSU Time_altr: map Id to FogBasedRSU inv mk_Vehicle (i, -, -, -)== len i <= 8;_  
The fog cloud is also defined as a composite object that has twelve different fields with different data types. This composite object is used to store the data from fog-based RSUs. _FogCloud:_ _Rould : Id vehicled : map Id to Vehicle sensorId : Id TA_id: Id Time_altr: map Id to FogBasedRSU Video_Traffic: map Id to Camera rsu: map Id to FogBasedRSU R_sensors: map Id to Sensors hospital : map Id to Hospital Msgalert: map Id to FogBasedRSU currentlocation: set of Loc get_info_anyMiscellaneous: map Sensors to Sensor_info_anyMiscellaneous any_emergency : set of isEmergency emergency_list: map Id to Emergency; Road : Rd_Id: Id Rd_rsu1: FogBasedRSU;The Trusted Authority object is a six-field composite object that includes the trusted authority identity, view vehicle, view traffic video, view location, view RSUs sensors, and view hospital. The trusted authority can view the mentioned information using an identifier from the fog cloud. _TrustedAuthority : TA_id: Id View_vehicle: map Id to Vehicle View_traffic_video: map Id to Camera View_location: set of Loc View_Rsusensor : map Id to Sensors View_hospital : map Id to Hospital;_  
State, actions, and reusable functions make up the dynamic portion. The properties established above in the form of composite objects are included in the formal definition of the proposed module's state. As demonstrated below, the function init is also used to initialise the composite objects.