# Formal Modeling of IoT and Drone-Based Forest Fire Detection and Counteraction System
## 4 Specifying Model Formally Using VDM-SL
### Static Model
```
1 harm:=allid:Node
2 nbrs:set of Node
3 nbrs:=landland.pwr = <Low> and
4 lid.status = <FAILURE_DETECTED> <=> allid.situation = <CRCIAL> and
5 lid.info <> {} andalid.status = <FAILURE_ NOT DETECTED> <=> allid.situation = <NOT_CRCIAL> and
6 nbrs <> {} andalid.connection = false <=> nbrs = {};  
The Alarm is described with two fields, and its **Invariant** is described as the alarm node's power is low, and the status changes to FAILURE_DETECTED if and only if the alarm's situation is crucial and any information is received; otherwise, no failure is detected. If a neighbor's set is attached to the alarm, then it is connected; otherwise, it is disconnected. ``` Gateway:gwid:Node
1 nbrs:set of Node
2 inv mk Gateway(gwid,nbrs)== gwid.status = <FAILURE_DETECTED> <=> gwid.situation = <CRCIAL> and
3 gwid.info <> {} and gwid.status = <FAILURE_NOT_DETECTED> <=> gwid.situation
4 <NOT_CRCIAL> and gwid.info = {} and gwid.connection = true <=> nbrs <=>
5 nbrs <> {} and gwid.connection = false <=> nbrs = {}; ```
The most critical node gateway is identified as _GateWay_, which has fields _gwid_ and _nbrs_. **Invariant** described as the gateway status is detected as failed if and only if its situation is crucial and the info of the event is also received. If the gateway node has a neighbor's set, then the _connection_ returns true; otherwise, it returns false. ```
1 Drone:=idid:Node
2 nbrs:set of Node
3 inv mk_Drone(did,nbrs)== did.pwr = <High> and did.situation = <CRCIAL>
4 <> card nbrs < 2 and did.situation = <NOT_CRCIAL> <=> card nbrs >= 2 and did.status = <FAILURE_DETECTED> <=> did.info <> {} and
5 lid.status = <FAILURE_NOT_DETECTED> <=> did.info <={} and
6 lid.connection = true <=> nbrs <> {} and
7 lid.connection = false <=> nbrs = {}; ```
The drone is described here as an object _Drone_ having these following fields: did and nbrs. **Invariant** specified as: the power of the drone is high as compared to the alarm and sensor. A drone is considered crucial if there are less than two nodes in the neighbors; otherwise, it is considered not crucial. The drone is connected if and only if the neighbor's set is not empty. ``` ControlRoom:<crid:Node
8 nbrs:set of Node
9 grcconns:Conns
10 for(nbrs:set of Node
11 inv mk_ControlRoom(grid,_,_,_)== crid.pwr = <High>; ```
The control room is important in the network topology because all the objects are connected with it. So, it is specified here as _ControlRoom_, having four fields. **Invariant**: The power of the control room will always be high as compared to all other nodes. ### Dynamic Model

The dynamic model's formal specification is defined further below, where the state, functions, and operations are included. There are topology, sensors, alarms, drones, gways, and conn are utilized in the state which are already defined above. ``` state_IOUN of  intopology: [NTopology]  sensors: set of Sensor  alarms: set of Alarm  drones: set of Drone  gways: set of GateWays  conn: Conns  inv mk_IOTN(ntopology, -, -, -, -, -)== card ntopology.subnets >= 1 and  exists_sbmt in set ntopology.subnets &  exists controlroom in settopology.crooms & exists node in set sbnt.nodes & PathSS([node], sbnt)= true and PathSAL([node], sbnt)= true and  PathSGW([node], sbnt)= true and  PathOKR([node], controlroom)=true and  PathDCR([node]  
```
operationsFailureOfSensor(sen:Sensor)failed:bool extrdntopology:[NTtopology] preforallshntinsettopology.snets& existssnodeinsetshnt.nodes&snode.sensors=sen postfailed<>sen.senid.connection=falseandsen.nbrs={} andforallshntinsettopology.snets& existsnodeinsetshnt.nodes&PathSS([node],shnt)=falseorPathSAL([node],shnt)=falseandPathSSW([node],shnt)=false)
```  
In the **pre-condition**, the existence of an input sensor in the subnet is verified. The **post-condition** is described as failure detected only when the connectivity of the sensor with neighbor nodes is disconnected. The paths of communication between sensor-to-sensor, sensor-to-alarm, and sensor-to-gateway might be broken.