# Formal Modeling of IoT and Drone-Based Forest Fire Detection and Counteraction System
## 4 Specifying Model Formally Using VDM-SL
### Static Model  
The system consists of different nodes having similar attributes and is defined in _Node_ as a composite object consisting of six variables, and the description is given. Ndid shows that each node has a unique identity. Pos shows that each node is notified of its position. The Power node has the power low or high. Status is used to check whether the sensor is active or sleeping. FireInfo records that the information of fire is transmitted or received. Signal is used for sending signals from the gateway to the control room. The connect variable is used to check the connection of nodes. ```
typesN0 ID=token;Pos::xcor:intYor::printPower=<HiH>|<LOW>;Status=<ACTIVE>|<SLEEP>; FireInfo=<INFORTRANSMIT>|<INFORECIEVED>|<INFO_NOTRECIEVED>; Signal=<SIGNAL_SENDTO_CR>|<SIGNAL_RECIEVED>; NODE:nidid:N0 IDpos:PosPower:Power status:Status fireinfo:FireInfo signal:Signal connection:bool; Links=setofLink invlinks=forallmk_(nidl,nidl2)insetlinks&mk_(nidl2,nidl1)insetlinks&mk_(nidl2,nidl1)inlink=*idlD*NidlD;
```  
The _Link_ represents the connection between two nodes, and the connectivity of the network is represented by the _Links_ relationship. In the network, every two nodes are identical, which means that both can communicate with each other. A node is not connected to itself, which indicates that the network does not have a loop. **Composite objects of alarm and sensors**  
```
1 LarmMode=<ON>|<OPE>;1 Larm::anhode:NODEmode:AlarmMode;
```  
The alarm is also a node and defined as a composite object having two fields. The _anode_ accesses the attributes of the object NODE, and other shows that either alarm's mode will be on or off. ```
Animal=token;AnimalBehavior=<NORMAL>|<PANIC>|<WORK>|<RUNMAWY>;Temp::bodytemp:realnndbodytemp:real;AnimalSensor::sanode:NODE animals:setofAnimal temp:Temp  animalbehavior:AnimalBehavior:AnimalBehavior=forallanimimxmlesensor(sanode,animals,temp,animalbehavior)==forallanimsetanimals&an=sanode.ndiadifftemp.bodytemp<temp.nndbodytemp>temp.nndbodytemp>temp.nndbodytempandanimalbehavior=<PANIC>oranimalbehavior=<WORK>oranimalbehavior=<RUNMAWY>then assode.status=<ACTIVE>elseanimalbehavior=<NORMAL>and assode.status=<SLEEP>;
```  
The formal definition of the sensor attached to the animal's body is defined as _AnimalSensor_ in the composite object with four fields and a description. The asnode is used to access the attributes of the earlier specified object NODE. The animals variable is used to show the attachment of certain sensors to a collection of animals. The temp is used to monitor the body temperature of the animal, and animal behavior defines the behavior of the animals. The _invariant_ for this sensor is defined as the uniquely identified sensors are connected to limited animals. If the temperature of the animal's body changes from normal and the behavior is panicked, worried, or the animal runs away from their place, then the sensor's status becomes active otherwise it stays asleep. ```
Tree=token;Ground=token;Location::tloc:Treegloc:Ground;Temperature:currenttemp:realnattemp:real;TemSensor::tsnode:NODE tsdeployed:mapsetofNID toLocation connds:setofNODE temperature:TemperatureinvmkTempensor(tsnode,tsdeployed,connds,temperature)==forallsnodeinsetdomtsdeployed&snode=(tsnode.ndiad)and iftemperature.currenttemp>temperature.nattemp then tsnode.status=<ACTIVE>andtsnode.firesoftstoechotesetasnode.status=<SLEEP>andtsnode.connect=true<=>connds<>()andtsnode.connect=false<=>connds=();
```  
The composite object _TempSensor_ is described here as displaying five fields for detecting temperature in the forest, and the description is given. The tsnode accesses attributes of the object NODE. The tsdeployed indicates that a set of sensors is deployed at a specific location. The connds displays the connection of nodes that are connected, and the temperature field records the current and natural temperature. The _invariant_ is defined as: the set of sensors deployed on the trees and ground to check the temperature of the forest.