# Formal Modeling of IoT and Drone-Based Forest Fire Detection and Counteraction System
## 4 Specifying Model Formally Using VDM-SL
### Static Model
```
*ADMode =<IDDE>|<WORKINGS>; ADAction =<EXTINGUISH_FIRE>|<FIRE_EXTINGUISHED>| <FIRE NOTEXTINGUISH>; ADrone::adnode: NODE con_adds: set of NODE order: ControlRoom adnode: ADMode adaction: ADAction inv mk_Adrone(adnode, con_adds, order, admode, adaction) == adnode_Power =<High> andif order.aorder.order_recieved = true then admode = <WORKING> and adaction = <EXTINGUISH_FIRE> and adaction = <FIRE_EXTINGUISH> else admode = <IDDE> and adnode.connect = true \(\Leftrightarrow\) con_adds <> {} or adnode.connect = false <=> con_adds = (  
```
GTPopology:subnects:setofSNet croom:setofControlRoom gtocron:Links mdrones:setofMDrone adrones:setofADrone motmodcon:Links crtondecon:Links adtoadcon:Links crtodacon:Links crtodacon:Links invmk_GTopology(subnects,croom,gtocron,mdrones,adrones,mdtomdcon,artomdcon,artomdcon,artoadcon)==forallsbnintestubnets& exlistscrinsetcroom& existscrconinsetgocron& exron=mk_(sbnt.gateways.gwnode.ndid,cr.cronde.ndidid)andforallmintestmdrones& existsconninsetmatomdcon& comn=mk_(mdl.mndoed.ndidid) md2.mndoed.ndidid) forallconninsetmatomdcon& existsmdl,mdl2 insetmdrones& comn=mk_(mdl.mndoed.ndidid,mdl2.mndoed.ndidid)and existscrinsetcroom& existscrooninsetcroom& extscroon=mk_(cr.cronde.ndidid,mdl.mndoed.ndidid) andforallsandiinsetadrones& existsadminsetadrones& existsconninsetadrones& conn=mk_(adl.adnode.ndidid,ad2. It is being confirmed in the **pre-condition** that the fire is detected, and the **post-condition** shows that the fire information will be transmitted if and only if gateways receive that information from sensors. ```
InfoTransmission(detected:bool)transmitted:boolextrdsensors:setofSensorrdgateways:setofGateWaypredetected=trueposttransmitted<=forallsennistsensors&existsownistgateways&sen.animalsensor.asnode.fireinfo=<INFORRANSMIT>=>gw.gwnnode.fireinfo=<INFORRECEVED>orsen.tempsensor.tsnode.fireinfo=<INFORRECEVED>orsen.flinefors=<INFORRECEVED>orsen.flinefors=<INFORRECEVED>orsem.smokesensor.snsnode.fireinfo=<INFORRECEVED>orgw.gwnnode.fireinfo=<INFORRECEVED>;
```
After the information has been sent, the gateways will report it to the control room and the process transmitted is taken as input. The set of gateways is read in the external clause and written on the set of control rooms. The transmission of information is confirmed in the **pre-condition**, the connections of the gateways and control room are shown in the **post-condition**, and the gateway sends a signal that is received by the control room. ```
ReportToControlRoom(transmitted:bool)extrdgateways:setofGateWaywrroom:setofControlRoompretransmitted=truepostforallwinsetgateways&existscrinsetroom&gw.gwnnode.signal=<SIGNALSENDTOCR>andcr.c.ernode.signal=<SIGNALRECEVED>;
```
When the control room receives signals from gateways, it issues an order to monitor drones, which is defined here in this operation. It reads a set of control rooms and writes on the mdrone in the external clause. **Pre-condition** is true, and in the **post-condition**, the process monorder returns true if and only if the monitoring order is received from the control room. The connection between the monitoring drone and the control room is shown, and when the order is received, the drone will start visualizing the area to confirm the fire. ```
TestMonorder()monorder:boolextrdcro:setofControlRoomwrmdrones:setofMDronepretruepostmonorder<=>existscrinsetroom&existsmdinsetmdrones&md.mdnodeinsetcr.con.cernbroksandcr.aorder.order.recieved=true=>md.mdronemode=<WORKING>andmd.mdroneaction=<REATIMEvisualIZATION>;
```
After visualizing the area, the drone will report back to the control room that the fire information is correct or not. The monorder process, node, and set of monitoring drones are taken as input. In the **pre-condition**, the process monorder returns true as the visualization is done and in the **post-condition** drone provides the information that the fire is confirmed or there is no fire and goes back to its position.