# Formal Modeling of IoT and Drone-Based Forest Fire Detection and Counteraction System
## 4 Specifying Model Formally Using VDM-SL
```
Nonreport(monorder:bool,node:NODE,mdrone:setofMDrone)premonorder=truepostforallmintendrone&md.mdroneaction=<FIRE_CONFIG>ormd.mdroneaction=<NOFIRE_EQUND>andmd.mdnode.pos=node.pos;
```
After confirmation of fire, the control room issues orders to the actor drone to combat the fire. It takes the _monreport_ process as input to check whether the fire info is true or false. In the external clause, the set of control room and _mdrone_ are being read and written in the set of _adrone_. **Pre-condition** indicates that the fire has been confirmed and the method actionorder returns true in the **post-condition** if and only if the order is sent from the control room. ```
NFDR(NT)  
Network is deployed in the subnet mechanism which are connected to Control room nominated as CR\({}_{i}\)  
1. For each subnet \(SBN_{i}\) gateways are described as \(GW_{i}\) where i = 1, 2,..., k
2. There exists \(i,j=1,\ 2,\ \ldots,\) k \((i\
eq j)\)
3. If PathGWCR \((\ (GW_{i})(CR_{i}),\ NT)\) = True, Then
4. Subnets are connected to Control Room Else disconnected
5. Forall subnet \(SBN_{i}\), where i = 1, 2,..., k
6. If PathSS \((\ S_{i}[GW_{i}],\ NT)\) and PathSA \((S_{i}A_{i}[GW_{i}],\ NT)\) = True, then
7. Nodes are connected in Subnets Else disconnected
8. Forall Nodes N in subnet \(SBN_{i}\)
9. Crucial(N)= False
10. If subnet is distributed without any N, then
11. Crucial(N)= True
12. Endlf
13. If (sensor S fails) Then
14. \(S^{\prime}\) Replaced(S)
15. Else If (Alarm A fails) Then
16. \(A^{\prime}\) Replaced(A)
17. Else If (Gateway GW fails) Then
18. \(GW^{\prime}\) Replaced (GW)
19. Endlf
20. Forall Drones \(D_{i}\) where i = 1, 2,..., k
21. If PathDD \((D_{i},D_{i},\ NT)\) and PathDCR \((D_{i}[CR_{i}],\ NT)\) = True, then
22. Drones are connected to control room Else not connected
23. Forall drones D
24. Crucial(D)= False
25. If network is distributed without D, then
26. Crucial(D)= True
27. Endlf
28. If (Drone D fails) = true, then
29. \(D^{\prime}\) Replaced(D)
30. Endlf
```
**Algorithm 1**Failure detection and recovery

## 6 Formal Modeling of Failure Detection Algorithm

VDM-SL is used to define the formal specification of the presented algorithm. It should be remembered that the mathematical constructs of VDM-SL can be used to model any component of a network. The proposed model is divided into two parts: static and dynamic. ### Static Model

In the network, there are several nodes, which are the sensor, alarm, gateways, and drones. All these nodes have similar attributes, so the composite object named Node has several fields, which are described here. The status indicates whether the failure is detected or not. The info is used to record the information of failure. The situation variable shows whether the node is crucial, and connection is used to record the connectivity between the nodes. Sensors:Send:Node

nbr:sset of Node

inv mk Sensor(senid,nbrs)==

senid.pwr = <Low> and senid.status = <FAILURE_DETECTED> <=> senid.situation = <CRCIAL> and senid.info <> [] and

senid.status = <FAILURE_NOT_DETECTED> <=> senid.situation = <NOT_CRCIAL> and senid.info = {} and senid.connection = true <=> nbrs <> (| and senid.connection = false <=> nbrs = {};

The object sensor is specified here with two fields, _senid_ and _nbrs_, and the **Invariant** indicates that the power of the sensor node is low, and the status is becoming _FAILURE_DETECTED_ if and only if the situation of the sensor is crucial and any info is received; otherwise, no failure is detected. If there is a neighbor's set linked with the sensor, then it is connected; otherwise, it is disconnected.