# Formal Modeling of IoT-Based Drone Network for Combating COVID-19 Pandemic

Authors: Moeeza Iqbal; Nazir Ahmad Zafar; Eman H. Alkhammash; Myriam Hadjouni
Journal: Journal of Sensors
 (2022)

---

## Abstract

Coronavirus biologically named COVID-19 is a disease that is circulating throughout the world due to its viral nature. The interaction of people is a source of spreading of coronavirus. Millions of people have been affected by this virus, and most of them have lost their lives. At present, this viral disease has grown into a worldwide pandemic which is a troubling spot for the whole world. Few technologies are supporting to manage and solve the COVID-19 crisis. In this paper, unified modeling language (UML) will be used to describe requirements and behavior of the proposed system. Unmanned aerial vehicle (UAV) drones are flying mechanical devices without any human pilot that is efficient to reduce the spreading rate of COVID-19. In the proposed IoT-based model, a cluster-based drones’ network will be used to monitor and perform required actions to tackle the violations of standard operating procedures (SOPs). The drones will gather all data through embedded cameras and sensors and will communicate with the control room to operate the actions as required. In this model, a well-maintained and collision-free network of drones will be designed using graph theory. Drones’ network will observe the violation of SOPs in the targeted area and make decisions such as produce alarm sound to alert persons and through communications by sending people warning messages on their smartphones. Further, the persons having COVID symptoms such as high temperature and unbalance respiratory rates will be identified using wearable sensors that are deployed to the targeted area and will send information to the control room to perform required actions. Drones will be able to provide medical kits to the patients’ residences that are identified using wearable sensors to reduce interaction of people. The model will be specified using Vienna Development Method-Specification language (VDM-SL) and validated through the VDM-SL toolbox.


---

## Body

## 1. Background

The IoT is a network of linked, Internet-interconnected gadgets that can transmit and receive data over a wireless link with no human participation. COVID-19 is a viral illness that can be transferred from one person to another by the close interaction of people in less than 6 feet of distance. The earliest-time coronavirus was discovered in December 2019 in Wuhan located in China; in the past, no one knew about it, but in a short time, this virus has grown into a worldwide pandemic [1]. Unmanned aerial vehicle (UAV) drones play an essential part in dealing with the COVID-19 outbreak although they are flying robots with no human interference, which would help to minimize virus transmission.


## 2. Introduction

Corresponding to the latest statistics worldwide, 45.8 million people have been affected with COVID-19 and 1.19 million people could not stay alive. In Pakistan, 334K COVID-19 cases are reported and 6,823 people have lost their lives [2]. COVID-19 symptoms include dry cough, headache, and tiredness, but certain patients might experience throat pressure, nasal congestion, and sore throat. The World Health Organization (WHO) has declared standard operating procedures (SOPs) to reduce transmission of coronavirus. SOPs include keeping a social distance of 6 feet, using a mask, and using sanitizer. To reduce the spread of virus, it is important to maintain SOPs and minimize the interaction among the people.In this paper, the proposed model includes three modules that are monitoring SOPs, identification of COVID patients, providing them medical services, and the maintenance of drones’ network in case of any failure. The proposed model is cluster-based which includes sensor drones, actor drones, cluster heads, and a control room. By integrating the Internet of Things (IoT), drones can detect SOP violations in the targeted area using embedded sensors and cameras. Our major goal is to keep monitoring of SOP breaches in targeted area and take action while reducing human interaction in order to keep the spread under control. Unified modeling language (UML) is used to develop a model that described the behavior of the system [3]. To make the system understandable, the proposed system is modelled and the functionalities are explained using UML. Graph theory is a data structure that is used to effectively store information [3] which is used to represent the connections and communication between the nodes [4]. In targeted areas, the drones will be able to monitor the violations of SOPs and communicate with the control room in order to perform runtime actions. It is assumed that the control room have details of every person so they can communicate with people when it will be required. In the targeted area, wearable sensors are already implemented to identify persons having symptoms of COVID-19 and inform control room to perform an action. The control room will be able to communicate with drones and people as well, and each drone will be able to communicate with every other drone. It is assumed that every person has done and medical insurance where the drones will deliver medicine and test kits.Figure1 illustrates, that when a drone detects a violation of social distancing or missing mask, the drone will perform some actions such as produce alarm sound and spray sanitizer then provides information to the control room, which then takes action by sending an alarm message to the individual.Figure 1
Monitoring SOPs.For any model, maintenance is an essential part that in case of any failure there should be a recovery method for the maintenance of the model. The drones are restricted to their defined zones to avoid the collision. In case if a drone fails due to any technical reason, then for placing new drone, the existing drones will be shifted and cover the place of failed drone and then the new drone will be placed in the space. This procedure will help to avoid the collision of drones during the placement of new drones as shown in Figure2. The control room is responsible for the charging of drones; it allows drones to charge from time to time and the neediest drones have priority to be charged first.Figure 2
Drones’ maintenance.Wearable sensors are used to identify COVID patients. Wearable sensors are already implemented in the targeted region. Figure3 illustrates that individual having symptoms of coronavirus (high temperature and unbalance respiratory rates) can be identified and sent a signal to control room. A control room refers a message to persons and also sends a signal to actor drone to provide medical services to the residence of that patient.Figure 3
Identifying infected person.The model is specified utilizing formal methods in Vienna Development Method-Specification language (VDM-SL). The formal methods are a software engineering framework that employs mathematical methodology in the development of complex software systems [5]. To describe each process attribute, the method employs a formal specification code. The VDM-SL uses a distinct syntax composed of objects, relations, and laws. Model validation is done by the VDM-SL toolbox to check the correctness by utilizing facilities available in the VDM-SL toolbox. COVID-19 has become a globally big challenge because people are not taking precautions. We are addressing this issue by making a formal model of a well-maintained drone-based network system that will reduce the interaction of people by providing medical services and network of drones will restrict persons to follow SOPs in targeted area by alerting them. The model is validated and verified by using features of the VDM-SL toolbox. There exists a little research work on COVID-19 and drone system, but there is no work done on drones’ network using formal methods and there exists no complete model that provides SOP alerts and maintenance of drones and medical delivery in a single system.


## 3. Related Work

In [1], the authors proposed a drone-based architecture to handle the pandemic issues by monitoring people following social distancing. Furthermore, this study was to collect the medical data by using wearable sensors in crowded areas; by processing collected data, the drones become able to take some real-time decisions. In this research, they also restricted drones to their zones to avoid the collision. In [2], the study explores, during the COVID-19 pandemic, drones would improve medicine delivery efficiency. Drones will also contribute to delivering a COVID test kit to the patient’s house and carrying the specimen to a laboratory in this study. The lesser the chance of viral transmission, the less you contact with patients. In [6], the delivery through drones has been discussed in this research; the authors proposed a model in which the drones can deliver multiple packages to the customer as well as the energy drains. The result of the experiments concludes that the number of drones and the speed of drones have an impact value on the objective. In [7], an architecture of a design of a network of drones has been discussed. It consists of coordination and communication with each other by using embedded sensors. They also implemented a multidrone system that can assist in disaster situations such as search, rescue, and monitoring. In [8], the authors present a brief review about cooperative tasks performed by multi-unmanned aerial vehicles. Furthermore, in this research, they have analyzed the importance as well as difficulties of UAV mutual tasks under some complex environment. In [9], the researchers highlighted many technologies which are helping in the fight against coronavirus. They also have discussed the difficulties of using the given algorithms. A model has been presented to recognize the symptoms of the virus which needs some extra accuracy. They determined that many technologies need more development for an efficient model. In [10], a method has been introduced to estimate the location of a drone. For the estimation, they used double sensors. With the connection of these sensor, they can find the nearest drone and its locus will make a cone which will help to estimate the location of the drone. In [11], the authors discussed about monitoring visitor’s behavior by analyzing zenith images captured by the drones. They also discussed this method of analyzing behavior is way better than the GPS and many more techniques. Furthermore, in this paper, a real-time scenario was discussed to get feedback about crowded place. In [12], an efficient city-based method is introduced which will help to reduce the spread of coronavirus among the medical staff of the hospitals. All the patients will be isolated at their homes. The doctors will deliver the medications with the help of drones. Only those patients who are more critical will be admitted to hospitals. This method will reduce the interaction of patients with the doctors.In [13], the innovative fight of Ghana in Africa during coronavirus has been discussed. Africa is deficient in technology as compared to all other regions, but in this breakout, an innovative idea utilizing drones to deliver test supplies is introduced, test samples, medications, and many more effective activities. In [14], this study has proposed an improved multidrone method to handle attacks more effectively. Furthermore, in this study, they have proposed communication between every drone to take a decision against the attack. The results show that this method is more useful than the regular one. In [15], a survey about UAV technology has been taken. They have discussed about the many existing parameters of UAVs like the network and communication. They also highlighted applications as well as the challenges of the technique. In [16], the authors give a review of the existing UAV communication protocols, network architecture. They also discussed some techniques like machine learning, encryption to enhance security and long-lasting communications. Furthermore, in this study, some applications are also discussed. In [17], the authors reviewed the recent issues of the deployment of drones. They highlighted that the drones could inflict many other air objects. So, there is a need of having some more policies to overcome this issue. Furthermore, in this paper, they have discussed about air management. In [18], the authors proposed a framework for some dynamic weather. The candidate drones work for delivery service. The proposed framework allows the drones to make some runtime changes according to the delivery expectations. The results show the efficiency of the framework. In [19], the authors proposed an approach to solving the charging issue of the drones in the network. They proposed a scheduling algorithm that schedules drones with preference like the most needed drone will get the charging slot first. Furthermore, if a drone needs charging, it can request from the station. Game theory approach has been used in it which results in an efficient system of charging. In [20], the authors proposed a trajectory model in order to minimize the disturbance between normal aircraft and drones. In this model, the positions of drones will be covered like the initial position, updated position, and different collision zones have been analyzed, and the results show the proposed model can be deployed to evaluate the probability of collision. In [21], the authors proposed a machine learning-based model to predict the threat of coronavirus in the whole world. Cloud computing platform has been used in this model to enhance the accuracy of the prediction. Further, they have provided some useful future directions. In [22], the authors review the role of IoT in combating COVID-19 pandemic as the linked devices and applications which are IoT-based are very useful to handle this pandemic. Further, they have discussed that monitoring of patients and early diagnosis can reduce the spread of coronavirus. In [23], the authors have discussed all the possibilities of the spreading of coronavirus. They have said some disinfection like sodium hypochlorite, chlorine, and bleach solution can be helpful for lower growth of coronavirus. Further, they have assessed the implementation of drones spraying these disinfection chemicals.In [24], two concepts have been proposed by the authors for swarm drones which include a structural model to avoid the autonomous directions to overcome the GPS-denied environment and to build a collision-free system. Further, they have simulated the system under some GPS-denied scenario. In [25], a system has been proposed to detect coronavirus automatically by using thermal images by using IoT-based drones. Further, the system can use virtual reality for real-time scanning and monitoring. In [26], the authors propose a study to show the importance of artificial intelligence in the fight against the coronavirus as the AI can be useful in treatment testing and preventing the spread of this virus. In [27], the authors have proposed a system to avoid collision of multidrones by making a less complex framework in order to rout the drones with some time plans; further, some scenario has been discussed to show the efficiency of system framework of scheduling. In [28], the authors have reviewed all points which are related to COVID-19 pandemic as well as the impact of this outbreak on the economy. In [29], the authors proposed a study of smart city technologies such as drones, smart healthcare, and medicine delivery in order to minimize the spread of COVID-19; these technologies will reduce the interaction of people. Further, they have discussed groceries’ delivery essential things and many more important items without any human interaction. In [30], the authors have reviewed the role of many information technologies in the fight against COVID-19 pandemic and the study has concluded that IT such as video calls, drones’ big data, and many more tools have played a role in the prevention and treatment. In [31], the authors give an overview of some solutions that already exist for contact tracing. Further, they have discussed principles that can affect the efficiency of the wearable tackling. In [32], the authors proposed a review of the use of unmanned aviation systems (UAS) to handle the COVID-19 issues; further, the authors discussed the innovations in the technologies used during the pandemic. In [33], the authors have reviewed big data, IoT, and AI that play an important role in diagnoses and treatment of COVID-19. In [34], the authors propose a study that includes the deep learning edge computing and their role and the challenges of these technologies in the COVID-19 pandemic. Further, they have proposed a system with its issues and scope. In [35], the authors have proposed a study on the integration of technology and the challenges on the integration also have been discussed. Further, they have given a future direction to improve the efficiency of the technologies.In [36], the researchers identify emerging technology in order to analyze COVID-19 handling. The proposed model could aid in the reduction of coronavirus dissemination. It will also improve healthcare team safety and minimize worker workload. The importance of these technologies in limiting the crisis is also discussed in this study. In [37], the scholars look at several technologies that might benefit in the struggle during COVID-19. The effect of certain technologies is discussed. AI stands for artificial intelligence. The most influenced innovations explored in this paper are machine learning and supply chain. In [38], during the COVID-19 pandemic, the researchers explored the use of drones for food delivery. They have two theories for gathering samples, one before and one after the introduction of this technology. The findings reflect a clear improvement in the regulation of virus transmission. In [31], during COVID-19, the researchers explored the use of wearable monitoring systems. They also explained the concepts of using this tracing and the problems that can arise as a result of using this technology, as well as its reliability. In [39], the scholars provided an analysis of several agricultural technologies such as AI, IoT, robots, and drones. Those would be the agricultural mechanization developments after COVID-19. In [40], the scholars suggested a robotic Internet to support in the struggle next to COVID-19 by capturing medical methods and saving the data on a cloud server where doctors may access it and bring medical instructions via the Internet. In [41], food system of time has contested. Although these herbaceous plants are favorable to the immune system, they are included together with numerous other meals that may be helpful in battling the virus. The report goes through this food chain in detail. In [42], the consideration of AI, which can be helpful in coping with the COVID-19 crisis, has been explored. They also addressed how AI can be educated so that it can spot infected people, which might save lives. In [43], the authors talk about smartphone apps that might aid in the fight against COVID-19. Data may be monitored in real time via apps or smartphone dashboards, and in China, there are apps for individuals that are in close contact with a confirmed or accused person. In [44], the authors provide the information about the role of drones in case of any disease crisis breaks like COVID-19. They also said that the drones are used for monitoring the spread of virus, for cargo, or any delivery system during pandemic. In [45], the authors have discussed that the role of drone technology can be very helpful in any crisis like the current COVID-19 pandemic. In the US, there are some programs that have shown drones feasible for these kinds of tasks. In [46], the authors have presented about the role of robotics in handling infectious disease. The robotics include cameras and sensors for monitoring in public areas as well as the temperature and medical conditions can be monitored which can be very helpful for combating virus. In [47], the authors have described the role of information technology application for the management of COVID-19 crisis. The information technologies are categorized into four topics in this paper, the diagnosis of disease and prediction about it and protection. The main motive is to describe the use of technologies to reduce the spread of virus.In [48], the authors describe the conditions of lockdown due to COVID-19 like restrictions of our home activities and other changes about the society have been discussed and some future issues are also discussed. In [49], the authors have provided their opinions about the challenge’s opportunities and solutions about the post-COVID-19 and also about the agriculture food supply chain. They said in future the new agricultural herbs could be helpful in COVID-19 handling. In [50], the authors have discussed the deep learning applications to healthcare and the importance of deep learning in healthcare. They also discussed use cases of three different countries, and the challenges and issues of deep learning have been discussed. In [51], the authors provide the relation of effective pandemic handling with artificial intelligence. The diagnosis and therapy relationship has been discussed. The future deployment of AI in any pandemic is also discussed. In [52], the researchers have discussed the changes that occurred in our food system due to the COVID-19 pandemic. They also discussed the perspectives from CO+RE.


## 4. System Model

At present, the rapid spreading of coronavirus has become a global major problem. COVID-19 can be transmitted from one person to another person by human close interaction. When a COVID patient coughs, sneezes, or talks, virus can transmit by their respiratory droplets. In addition, people may become affected by contacting any infected substance and then touching their eyes, mouth, or nose. On a daily basis, millions of people are dying from this virus due to no cure. The vaccination process has started; until process is not done, it is important to minimize the interaction of people. The WHO includes social distancing, wearing mask, and sanitization.In this paper, a model is presented which uses a cluster-based drone network to monitor the violations of SOPs. This model is designed by unified modeling language and graph theory. The drones will monitor people wearing a mask or maintaining social distancing in the targeted area and send violation information to the control room for performing actions as required.


### 4.1. Internet of Things

The Internet of Things (IoT) describes the idea of connecting any gadget to the Internet and other devices. It is a vast network of interconnected items and people; all of which store and communicate information about how they are utilized and the environment around them. Devices with embedded sensors are connected to an Internet of Things infrastructure, which gathers data from a variety of sources and utilizes algorithms to transfer the most significant information to apps tailored to specific needs. It is an emerging technology; in the future, everything will be connected with the Internet of Things. IoT has made so many tasks easier and saves human time and effort. In our model, we have used drones with embedded sensors and cameras to monitor violations of SOPs and send signals to the control room for performing actions as required.


#### 4.1.1. UML Diagram

The UML is a structured modeling language made up of a collection of standard diagrams that let system and software engineers describe, visualize, plan, and analyze software system elements, as well as advanced analytics and other nonsoftware components. In the proposed model, the UML is used in terms of sequence diagrams. Sequence diagrams are relationship diagrams that show how processes are performed. They track the interaction among objects in the form of coordinated work. Sequence diagrams are time-oriented, and they physically represent the structure of the process by diagram to describe time what messages are received and when.Figure4 illustrates the process of monitoring SOP’s violation in the form of a sequence diagram. The sequence diagram included six objects: sensor drone, actor drone, produce alarm, cluster head, control room, and persons.Figure 4
Monitoring sequence diagram.The process of monitoring SOP’s violation is described in the form of sequence diagram. The sequence diagram shows the sequence of all the communication between objects. Firstly, the sensor drone senses violation and sends signal to the actor drone; a return message is sent to sensor drone.After receiving signal from sensor drone, a return message is sent to actor drone. The actor drone will spray sanitizer and produce an alarm sound and then sends message to cluster head. Cluster head will send signal to control room for performing actions such as the control room sending an alarm message to the person who have violated SOPs; a return message is sent to the control room.Figure5 illustrates sequence diagram that describes the process of maintenance of network of drones. This diagram includes three objects: control room, drones, and new drones, and the sequence of communication between these objects is illustrated using diagram.Figure 5
Maintenance sequence diagram.In case of any failure, the control room will find a failed drone; a return message action performed is sent to the control room. Then, the nearest drone will be shifted to the place of failed drone; the shifting process will continue until there exists a place where a new drone will be placed. The control room sends signal to the new drone as placed new drone, and a return message is sent to the control room.The shifting of drones will be collision-free as the drones have allotted their zones. Each drone has its zone, and when a new drone will be placed, the nearest drone will shift to the place of failed drone and new drone will be placed to the empty space.In Figure6, the sequence of communication of medical delivery service process is described in a sequence.Figure 6
Identification sequence diagram.This diagram includes seven objects that are wearable sensors, sensor drones, actor drones, cluster head, control room, persons, and medicine drone. The sequence of communication between these objects is illustrated using this sequence diagram. Firstly, the wearable sensors will sense symptoms of COVID-19 and send a signal to sensor drone; the sensor drone will send a signal to the actor drone; the actor drone will spray sanitizer and produce an alarm sound to alert the person and then sends a signal to the cluster head. The cluster head will send a signal to the control room for further actions. The control room refers alert to people and gives an order to the medicine drone to provide medical services to the patients’ homes.


### 4.2. Graph Theory

Graph theory is a combination of nodes and connections, and the communication between them can be represented. In our model, the graph theory is used to represent the whole proposed system by nodes and connections and communication between them.In Figure7, the monitoring process of the cluster-based proposed system is described in the form of graphs. Graph theory consists of nodes and edges. Wearable sensor node is connected to sensor drone nodes, and sensor drone nodes are connected to actor drone. Actor drones are connected to cluster heads.Figure 7
Graph of monitoring.Cluster head is connected to the other cluster heads, and every cluster head is connected to control room. These connections of nodes represent communication between nodes and edges during monitoring violations of SOPs.In Figure8, the network maintenance of the proposed system is described in graph theory which is composed of nodes and edges. Sensor drone nodes are connected to every other sensor drone node and also connected to actor drone nodes. The actor drone is connected to cluster head to send a signal to the other cluster head, and every cluster head is connected to the control room. Cluster heads can communicate with each other. In case of any drone failure, the failed drones will be detected; then, the nearest drone will shift to place of a failed drone, and then, the new drone will be placed in empty space. This shifting process is collision-free.Figure 8
Graph theory of maintenance.


### 4.3. Formal Method

Formal methods are procedures for describing complex systems mathematically. By creating a mathematically robust model of a complex system, programmers can not only validate the system’s features more thoroughly but also use mathematical evidence as an addition to system testing to ensure accurate behavior. We utilized formal method for specification in the VDM-SL language. To ensure the system’s accuracy, the validation was carried out utilizing the resources offered in the VDM-SL toolbox.Code 1.
typesID = token;Droneid = token;Statuss = <ACTIVE>|<SLEEP>;Embeddedsensor = token;Camera = token;Enrgy = <HIGH>|<LOW>;Alarm = <on>|<off>;Violation = <SOCIAL_DISTANCING>|<MISSING_MASK>;ViolationDetection = <VDETECTED>|<VNOTDETECTED>;CRAction = <WARNING_MESSAGE_TO_PERSONS>;SdroneMode = <IDLE>|<WORKING>;SDroneAction = <SENSE_VIOLATION>|<INFO_TO_ACTORDRONE>;AdroneMode = <IDLE>|<WORKING>;ADroneAction = <INFO_TO_CLUSTERHEAD>|<SANITIZATION>|<PRODUCE_ALARM>;ClusterHeadMode = <IDLE>|<WORKING>;ClusterHeadAction = <INFO_SENDTO_CR>;valuesSdinfeet: nat =6;In given specification, the types of the system are defined; first field is ID with type token. Second field is Droneid defined as a token type; third field is statuss which is defined as enumeration type which have 2 states active or sleep. Embeddedsensors and Camera are defined as token type. Enrgy is defined as it can be either high or low. The next two fields Alarm and Violation are also defined as enumeration types; both have two states. Every drone (sensor, actor, and cluster head) mode is defined as either IDLE or WORKING. In values, social distancing mearing in feet is valued as Sdinfeet.Code 2.
Sgnl :: received:boolnot_recieved:bool;Infor :: received:boolnot_recieved:bool;Database :: ID : tokenPid : IDperson : tokenpersonDetails : token;Drones :: Sensordrone: set of SDroneactordrones : set of ADroneembeddedsensor: Embeddedsensorcamera: Cameraviolationdetection:ViolationDetection;In above specifications, some composite objects are defined such as Sgnl and Info is defined as bool type which means it will be true or false. Database consists of four fields; ID defined as token, Pid as ID type, person, and presonDetails is defined as token. In the next line, Drones is a composite object which have five fields; first is Sensordrone defined as a set of SDrone and actordrones defined as a set of ADrone; next is embeddedsensor defined as Embeddedsensor type, camera is defined as Camera, and violationdetection is defined as ViolationDetection.Code 3.
Nde::Ndeid:IDenrgy:Enrgystatuss:Statusssgnl:Sgnlinfor : Infor;Edgeesss = set of Edgeeinv edg == forall mk_(Ndeid1,Ndeid2)in set edg &mk_(Ndeid2,Ndeid1) in set edg;Edgee = ID∗IDinv eg == let mk_(Ndeid1,Ndeid2) =eg in Ndeid1<>Ndeid2;In the given specification, the invariant of node describes that every node has a connection with every other node but a node is not connected to itself which means no loop exists.Code 4.
Controlroom ::cr: IDdb : map ID to Databasedrones : set of Dronesinfo : Inforcraction : CRActioninv mk_Controlroom( -,db,-,-,-)== forall person in set dom db & person = db(person).personDetails;In given specifications, Controlroom has five fields and the invariant of control room described that the control room has information of every person in the target area.Code 5.
SDrone::sdNde: NdesdNdemode: SdroneModesdNdeaction: SDroneActionviolation: Violationinv mk_SDrone(sdNde, sdNdemode, sdNdeaction, violation) == sdNde.enrgy = <HIGH>and sdNdemode = <WORKING> <=> sdNdeaction = <SENSE_VIOLATION>and if Sdinfeet < 6 or violation = <MISSING_MASK> thensdNdeaction = <INFO_TO_ACTORDRONE> else sdNdemode = <IDLE>;SDrone is defined as a composite object, and the invariant of SDrone describes that energy of sensor drone is high and mode of sensor drone will be working if and only if sensor drone will sense violation like missing mask or social distancing less than 6 feet, and then, sensor drone will send signal to actor drone or no violation found.Code 6.
ADrone::actordrone: Ndeactordronemode: AdroneModeactordroneaction: ADroneActioninv mk_ADrone(actordrone,actordronemode, actordroneaction) == actordrone.enrgy = <LOW> and actordronemode = <IDLE>and actordronemode = <WORKING> <=> actordrone.sgnl.received = true=> actordroneaction = <SANITIZATION> and actordroneaction = <INFO_TO_CLUSTERHEAD>;ADrone is identified as a composite object. The invariant indicates that the mode of actor drone is idle at first, and it goes in working mode if actor drone receives a signal from sensor drone. If actor drone receives a signal from sensor drone, actor drone will begin sanitization and send information to the cluster head.Code 7.
ClusterHead :: chNde : Ndesendssgnl : set of Dronesactdrone : set of ADronechmode: ClusterHeadModechaction: ClusterHeadActioninv mk_ClusterHead(chNde, -, -, chmode, chaction) == chNde.enrgy = <HIGH> and if chNde.sgnl.received = true then chmode = <WORKING> and chaction = <INFO_SENDTO_CR> else chmode = <IDLE>;Clusterhead is specified as a composite object which includes five fields, and the invariant describes that the energy of cluster head is high, and mode of cluster head will become working if and only if the cluster head receives signal from actor drone, and then, cluster head will send info to control room for further operations, or the mode will remain idle.Code 8.
ClusterHead :: chNde : Ndesendssgnl : set of Dronesactdrone : set of ADronechmode: ClusterHeadModechaction: ClusterHeadActioninv mk_ClusterHead(chNde, -, -, chmode, chaction) == chNde.enrgy = <HIGH> and if chNde.sgnl.received = true then chmode = <WORKING> and chaction = <INFO_SENDTO_CR> else chmode = <IDLE>;In the above specification, Cluster is defined as a composite object which includes four fields which are clusterhead, sensordrones, actordrones, and egd. The invariant of cluster describes that every node has a connection, sensor drone has a connection with other sensor drones, and sensor drone has a connection with actor drone. Actor drones have a connection with other actor drones, and every actor drone has a connection with cluster head.Code 9.
Topology :: clushead : set of ClusterHeadcrm : set of Controlroomclusterr : set of Clusteredgs : Edgeesssinv mk_Topology(clushead, crm, clusterr, edgs) ==forall ch in set clushead &exists crr in set crm &exists cc in set edgs &mk_(ch.chNde.Ndeid, crr.cr) = cc andforall cc in set edgs &exists cl1,cl2 in set clusterr &mk_(cl1.clusterhead.chNde.Ndeid,cl2.clusterhead.chNde.Ndeid) = cc andforall cl1, cl2 in set clusterr &exists cc in set edgs &mk_(cl1.clusterhead.chNde.Ndeid,cl2.clusterhead.chNde.Ndeid) = cc;In the above specifications, the graph theory-based topology of monitoring is described that includes clusters. Every cluster has a cluster head, and each cluster head has a connection with every other cluster heads, and every cluster head has a connection with control room.Code 10.
state SopsMonitoring oftopo : [Topology]sdrones : set of SDroneadrone : set of ADroneclusters : set of Clusterch : set of ClusterHeadcrom : set of Controlroomedg : Edgeesssinit sm == sm = mk_SopsMonitoring(nil, {},{}, {}, {}, {},{})endThe state of the monitoring system is defined which includes seven fields, and these will be used in the dynamic part of specification.Code 11.
operationsSOPsViolationDetection(cluster : Cluster) detected : boolext rd topo : [Topology]rd sdrones : set of SDronepreexists sd in set sdrones & sd in set cluster.sensordronespost detected <=> forall sd in set sdrones &sd.sdNdemode = <WORKING> andSdinfeet < 6 and sd.violation = <MISSING_MASK> and sd.sdNdeaction = <INFO_TO_ACTORDRONE>;In above specifications, the dynamic part of the system is defined. The pre/postcondition describes that the violations of SOPs are detected if and only if the mode of sensor drone is working and social distancing is less than 6 feet and mask is missing, and sensor drone sends info to actor drone.Code 12.
Adperformingactions(detected : bool) action : boolext rd topo : [Topology]rd adrone : set of ADronepre detected = truepost action <=> forall ad in set adrone &ad.actordrone.sgnl.received = true andad.actordronemode = <WORKING> and ad.actordroneaction = <PRODUCE_ALARM> and ad.actordroneaction = <SANITIZATION> and ad.actordroneaction = <INFO_TO_CLUSTERHEAD>;Adperformingactions describes the actions of actor drones. The pre/postcondition describes that actor drone mode will be working and will produce alarm sound and do sanitization and then sends violation information to the cluster head.Code 13.
InfoTransmitingtoControlroom(action : bool) transmited : boolext rd topo : [Topology]rd ch : set of ClusterHeadrd crom : set of Controlroompre action = truepost transmited <=> forall cluh in set ch &cluh.chNde.infor.received = true and cluh.chaction = <INFO_SENDTO_CR>;In the above operation, information is now transmitting to control room for further actions. The postcondition describes that when cluster head receives information from actor drone, it will send violation information to the control room.Code 14.
ControlroomActions(transmited : bool)ext rd topo : [Topology]rd crom : set of Controlroompre transmited = truepost exists cr in set crom &http://cr.info/.received = true => cr.craction = <WARNING_MESSAGE_TO_PERSONS>;The above operation describes the actions of the control room. The postcondition describes that when control room will receive information from cluster head, then control room sends warning message to the person.Another module of the proposed system is identifying corona patients by using wearable sensors. Formal model of this module is given below.Code 15.
typesID = token;Energy = <HIGH>|<LOW>;InfectInformation = <INFORMATION_SENT_to_SDRONE>|<INFORMATION_RECIEVED>|<NO_INFORMATION>;PeopleCondition = <NATURAL>|<FATIGUE>|<COUGH>;SdroneMode = <IDLE>|<WORK>;Statuss = <ACTIVE>|<SLEEP>;SDroneAction = <SGNL_TO_ACTORDRONE>;ActorDroneMode = <IDLE>|<WORK>;ActorDroneAction= <PRODUCE_ALARM>|<SANITIZATION>|<INFORMATION_TO_CLUSTERHEAD>;ClusterHeadMode = <IDLE>|<WORK>;ClusterHeadAction = <INFORMATION_SENDTO_CR>;MedDroneMode = <IDLE>|<WORK>;MedDroneAction= <DELIVER_KIT>;Ctrlaction = <ORDER_TO_MEDDRONE>|<MESSAGE_TO_PEOPLE>;In the above specifications, all the types are defined that will be used in the next specifications. First is ID defined as token; next all fields are defined as enumeration types that have different states, some have two and some have more than two. Every type of drone has two modes idle or working, and they have different actions. Sdrone has an action of signal to actor drone, and actor drone has actions which are produced alarm and sanitization and sends information to the cluster head. Cluster head action is sending info to the control room, and medicine drone action is to deliver medicine, and control room actions are issuing an order to medicine drone and send warning message to people.Code 16.
Sgnl :: sgnl_recieved:bool;Information :: Information_recieved:bool;Database :: peopleid : IDpeopleInformation : token;BodyBodyTemperature ::bodybodyBodyTemperature:real natbodybodyBodyTemperature:real;Rsystem:: bodyrsystem:real natrsystem:real;In above specifications, some composite objects are defined Sgnl and Information is defined as Boolean type. The database is defined as a composite object with a peopleid and peopleInformation of token type. Some COVID-19 indicators, such as fatigue and coughing, as well as body temperature, are considered to diagnose the patient.Code 17.
Nde::ndeid:IDenergy:Energystatuss:Statusssgnl:SgnlInformation:Information;EDGSSs = set of EDGSSinv EDGss == forall mk_(ndeid1,ndeid2)in set EDGss &mk_(ndeid2,ndeid1) in set EDGss;EDGSS = ID∗IDinv eg == let mk_(ndeid1,ndeid2) =eg in ndeid1<>ndeid2;The invariant describes that any node is connected to every other node; for example, if ndid1 is connected to ndid2, therefore ndid2 is connected to ndid1 and one node is not connected to itself.Code 18.
WESensor::wnde:Ndepeople:map ID to DatabasebodyBodyTemperature:BodyBodyTemperaturersystem:Rsystempcond:PeopleConditionInformation:InfectInformationinv mk_WESensor(wnde, people, bodyBodyTemperature, rsystem, pcond, Information)==forall ps in set dom people & ps = wnde.ndeid and if bodyBodyTemperature.bodybodyBodyTemperature > bodyBodyTemperature.natbodybodyBodyTemperature andrsystem.bodyrsystem < rsystem.natrsystem or rsystem.bodyrsystem > rsystem.natrsystem andpcond = <FATIGUE> or pcond = <COUGH> thenwnde.statuss = <ACTIVE> and Information = <INFORMATION_SENT_to_SDRONE> else wnde.statuss = <SLEEP>;WESensor are listed as composite object and of node type. It has five fields: the first is people, which maps id to database, the second is bodyBodytemperature, which identifies temperature, and the third is rsystem, which identifies respiratory system. The fourth field is pcond and the last is information. The invariant demonstrates the conditions for identifying infected people using WESensor by comparing people body temperature and respiratory rates with natural temperatures and respiratory rates. If the body temperature is higher than natural, the respiratory rate is higher or lower than natural, and the person condition is fatigued or coughing, then sensor’s status will change to active; otherwise, the sensor’s status will remain sleep.Code 19.
SDrone::sdnde: Ndesdndemode: SdroneModesdndeaction: SDroneActionInformation: Informationinv mk_SDrone(sdnde, sdndemode, sdndeaction, -) == sdnde.energy = <HIGH>and sdndemode = <WORK> <=> sdnde.Information.Information_recieved = true =>sdndeaction = <SGNL_TO_ACTORDRONE>;Sdrone have four fields, and the invariant shows that the energy of sensor drone is high and mode is working if the sensor drone has received information; then, action will be sending signal to the actor drone.Code 20.
ActorDrone::adnde:NdeActorDronemode:ActorDroneModeActorDroneaction:ActorDroneActioninv mk_ActorDrone(adnde, ActorDronemode, ActorDroneaction)== adnde.energy = <LOW> and ActorDronemode = <IDLE>and ActorDronemode = <WORK> <=> adnde.Information.Information_recieved = true => ActorDroneaction = <SANITIZATION> andActorDroneaction = <PRODUCE_ALARM> andActorDroneaction = <INFORMATION_TO_CLUSTERHEAD>;The invariant of actor drone shows that mode of actor drone is working if actor drone receives a signal from sensor drone; then, action of actor drone will be to produce alarm and do sanitization and sends Information to cluster head.Code 21.
ClusterHead :: chnde : NdeActorDrone : set of ActorDronechmode: ClusterHeadModechaction: ClusterHeadActioninv mk_ClusterHead(chnde, -, chmode, chaction) == chnde.energy = <HIGH> and if chnde.Information.Information_recieved = true then chmode = <WORK> and chaction = <INFORMATION_SENDTO_CR> else chmode = <IDLE>;The invariant shows that the energy of cluster head is high, and if cluster head received information from actor drone, then cluster head mode will be working and action will be information sends to control room else mode will remain idle.Code 22.
CtrlR::cnode:IDctrlaction : Ctrlactiondb : map ID to DatabaseWESensors: set of WESensorsgnl:SgnlInformation:Informationinv mk_CtrlR( -,-,db,-,-,-)== forall people in set dom db & people = db(people).peopleInformation;The CtrlR is defined as a composite entity with four fields that involve database control room function as ctrlction wearable sensors as a collection of WESensor and sgnl. The invariant demonstrates that any user is in a certain domain of the database and has personal information of people.Code 23.
MedDrone::mdnde:Ndemdronemode:MedDroneModemdroneaction: MedDroneActioninv mk_MedDrone(mdnde, mdronemode, mdroneaction)== mdnde.energy = <LOW> and mdronemode = <IDLE>and mdronemode = <WORK> <=> mdnde.sgnl.sgnl_recieved = true => mdroneaction = <DELIVER_KIT>or mdronemode = <IDLE>;Medicine drones include two modes: idle and working, and actions include delivering medicines, and not delivering kits. MedDrone is described as a composite object that is used as a Nde type and has the following fields: drone mode and behavior as stated above. The invariants indicate that the mode is idle at first, and it will only work if and only if the medicine drone receives a signal from the control room, at which point the ctrlaction will deliver medication or not.Code 24.
Cluster :: clusterhead : ClusterHeadsensordrones : set of SDroneactordrones : set of ActorDroneWESensors: set of WESensorEDGss : EDGSSsinv mk_Cluster(clusterhead, sensordrones, actordrones, WESensors, EDGss) ==forall ws in set WESensors & exists c in set EDGss &forall sd in set sensordrones &mk_(ws.wnde.ndeid, sd.sdnde.ndeid) = c andforall sd1,sd2 in set sensordrones &exists c in set EDGss &mk_(sd1.sdnde.ndeid, sd2.sdnde.ndeid) = c andforall ad1, ad2 in set actordrones &exists c in set EDGss &mk_(ad1.adnde.ndeid, ad2.adnde.ndeid) = c andmk_(sd1.sdnde.ndeid, ad1.adnde.ndeid) = c andmk_(sd1.sdnde.ndeid, clusterhead.chnde.ndeid) = c andmk_(ad1.adnde.ndeid, clusterhead.chnde.ndeid) = c;Cluster is defined as a composite object which has six fields, and the invariant of cluster defines that every node has a connection; firstly, wearable sensor has a connection with sensor drone and sensor drone has a connection with actor drone and actor drones have connection with other actor drones and with cluster head.Code 25.
Topology :: clushead : set of ClusterHeadcrm : set of CtrlRmdrone : set of MedDroneclusterr : set of ClusterEDGsss : EDGSSsinv mk_Topology(clushead, crm, mdrone, clusterr, EDGsss) ==forall ch in set clushead &exists crr in set crm &exists cc in set EDGsss &mk_(ch.chnde.ndeid, crr.cnode) = cc andforall cc in set EDGsss &exists cl1,cl2 in set clusterr &mk_( cl1.clusterhead.chnde.ndeid,cl2.clusterhead.chnde.ndeid) = cc andforall cl1, cl2 in set clusterr &exists cc in set EDGsss &mk_(cl1.clusterhead.chnde.ndeid,cl2.clusterhead.chnde.ndeid) = cc andforall md in set mdrone &exists crr in set crm &exists cc in set EDGsss &mk_(crr.cnode, md.mdnde.ndeid) = cc;In above specifications, graph theory-based topology is defined which describe the connection of cluster with control room. Every cluster has a cluster head; therefore, one cluster head has a connection with other cluster head and also a connection with control room. The control room has a connection with medicine drone.Code 26.
state MedService oftopo : [Topology]sdrones : set of SDroneActDrone : set of ActorDronemeddrone : set of MedDroneclusters : set of Clusterch : set of ClusterHeadcrom : set of CtrlREDGss : EDGSSsinit ms == ms = mk_MedService(nil, {}, {}, {}, {}, {}, {},{})endThe attributes are initialized in the init function, and the system is defined as medical services in state.Code 27.
operationsIdentifyInfected(WESensors: WESensor) Identified : boolext rd topo : [Topology]rd sdrones : set of SDronepre truepost Identified <=> exists sd in set sdrones & WESensors.wnde.statuss = <ACTIVE> and WESensors.Information = <INFORMATION_SENT_to_SDRONE> => sd.sdndemode = <WORK> and sd.sdndeaction = <SGNL_TO_ACTORDRONE>;IdentifyInfected is an operation that takes wearable sensors as input and returns output in Identified such as True or false is determined. Pre/postcondition: the operation’s precondition is true. The postcondition indicates that the patient will be detected if and only if the wearable sensor status is activated and wearable sensors will send signal to sensor drone, and then, mode of sensor drone becomes active and action of sensor drone is send information to actor drone.Code 28.
ActorDroneActions(Identified:bool) action : boolext rd topo : [Topology]rd ActDrone : set of ActorDronepre Identified = truepost action <=> forall ad in set ActDrone &ad.adnde.sgnl.sgnl_recieved = true andad.ActorDronemode = <WORK> and ad.ActorDroneaction = <PRODUCE_ALARM> and ad.ActorDroneaction = <SANITIZATION> and ad.ActorDroneaction = <INFORMATION_TO_CLUSTERHEAD>;In the above operations, actions of actor drone is described which takes input identified and output action; in postcondition, it shows that action is true if actor drone receives a signal from actor drone and mode of actor drone will become working; then, action of actor drone will produce alarm and sanitization and send info to cluster head.Code 29.
IdentificationRepoted(action:bool) reported:boolext rd ch: set of ClusterHeadpre action = truepost reported <=> exists clush in set ch & clush.chnde.Information.Information_recieved = true and clush.chaction = <INFORMATION_SENDTO_CR>;IdentificationRepoted is an operation that takes a bool type input. Cr is described as a group of control rooms in the external clause. Pre/postcondition: the precondition specifies that the defined operation must be valid. The postcondition indicates that the identification is reported if and only if cr is in the control room collection and the control room has received the signal.Code 30.
MedicalDelivery(Identified: bool)ext rd meddrone: set of MedDronerd crom: set of CtrlRpre Identified = truepost forall md in set meddrone & exists ctrl in set crom & if ctrl.Information.Information_recieved = truethen ctrl.ctrlaction = <ORDER_TO_MEDDRONE> andctrl.ctrlaction = <MESSAGE_TO_PEOPLE> =>md.mdronemode = <WORK> else md.mdronemode = <IDLE>;Pre/postcondition: the precondition is stated as true and in postcondition if the control room receives the info, and then, control room will give an order to the MedDrone for the medical services and sends warning message to the person; otherwise, the mode of MedDrone will remain idle.Another module of the proposed model is maintenance of drones’ network such as in case of a drone failure new placement drone will be collision-free. Drones will be charged from time to time, and the neediest drone will charge first.Code 31.
typesID = token;BatteryStatus = <DOWN>|<LOWEST>;Voltage = <HIGH>|<LOW>;Info = <COMMUNICATING>|<NOT_COMMUNICATING>;Status = <FAILED_DRONE_DETECTED>|<NOT_DETECTED>;Link = <LINKED>|<NOT_LINKED>;Condition = <FAULTED>|<NOT_FAULTED>;Shift = <NEAREST_DRONE>;Empty_Space_Drone = <REPLACE_NEW_DRONE>;Charging = <CHARGE_FIRST>|<CHARGE>;In the above specification, different types of system maintenance are specified and their types are defined.Code 32.
Nde::ndeid:IDvoltage : Voltagestatus: Statuscondition: Conditionlink : Linkinfo : Info;Edgeesss = set of Edgeeinv edg == forall mk_(ndeid1,ndeid2)in set edg &mk_(ndeid2,ndeid1) in set edg;Edgee = ID∗IDinv eg == let mk_(ndeid1,ndeid2) =eg in ndeid1<>ndeid2;The invariant shows that each node is unique such as id of one node is not equal to id of other node that means any node is not connected to itself.Code 33.
Zones = <A>|<B>;Drones::dnde:Ndezones : Zonesbattry : BatteryStatusinv mk_Drones(dnde,-, -)== dnde.voltage = <LOW> anddnde.status = <FAILED_DRONE_DETECTED> <=>dnde.link = <LINKED> and dnde.condition = <FAULTED> or dnde.status = <NOT_DETECTED> <=>dnde.link = <NOT_LINKED> and dnde.condition = <NOT_FAULTED>;Controlroom ::cr: Ndecharging : Chargingshift : Shiftshifted : Empty_Space_Drone;The described specification states two composite objects Drones and Controlroom. Drones include three fields: dnode, zones, and battry. The invariant shows that a drone will be detected as failed if and only if a drone is not linked and condition of drone is faulted; otherwise, failure is not detected. Control room includes four fields: cr, charging, shift, and shifted.Code 34.
ClusterHead :: chnde : Ndeinv mk_ClusterHead(chnde)== chnde.voltage = <LOW> andchnde.status = <FAILED_DRONE_DETECTED> <=>chnde.link = <LINKED> and chnde.condition = <FAULTED> or chnde.status = <NOT_DETECTED> <=>chnde.link = <NOT_LINKED> and chnde.condition = <NOT_FAULTED>;Clusterhead composite object includes one field chnode, and invariant describes that cluster head will be detected as failed if and only if it is linked and condition is faulted; otherwise, cluster head is not failure detected.Code 35.
Cluster :: clusterhead : ClusterHeaddrones : set of Dronesedg : Edgeesssinv mk_Cluster(clusterhead, drones, edg) ==forall d1,d2 in set drones &exists c in set edg &mk_(d1.dnde.ndeid, d2.dnde.ndeid) = c andforall d1 in set drones &exists c in set edg &mk_(d1.dnde.ndeid, clusterhead.chnde.ndeid) = c;Cluster includes three fields and that the cluster is composed of drones and cluster head. The invariant describes that every drone has a connection with every other drone and drones have a connection with cluster head.Code 36.
Topology :: clushead : set of ClusterHeadcrm : set of Controlroomclusterr : set of Clusteredgs : Edgeesssinv mk_Topology(clushead, crm, clusterr, edgs) ==forall ch in set clushead &exists crr in set crm &exists cc in set edgs &mk_(ch.chnde.ndeid, crr.cr.ndeid) = cc andforall cc in set edgs &exists cl1,cl2 in set clusterr &mk_(cl1.clusterhead.chnde.ndeid,cl2.clusterhead.chnde.ndeid) = cc andforall cl1, cl2 in set clusterr &exists cc in set edgs &mk_(cl1.clusterhead.chnde.ndeid,cl2.clusterhead.chnde.ndeid) = cc;Above specifications are graph-based topology which shows the connection between clusters and control room. Every cluster head is connected to other cluster head, and every cluster head is connected to control room. The connection is showed in form of nodes and edges.Code 37.
state Maintenance oftopo : [Topology]drones : set of Dronesclusters : set of Clusterch : set of ClusterHeadcrom : set of Controlroomedg : Edgeesssinit MN == MN = mk_Maintenance(nil, {}, {}, {}, {}, {})endThe State has defined all fields and their types which will be used in the dynamic model of the maintenance.Code 38.
operationsAlotingDroneZone() aloted : boolext rd topo : [Topology]rd drones : set of Dronespre truepost aloted = true <=> exists d1,d2 in set drones & d1 <> d2 andd1.zones = <A> and d2.zones = <B>;Operations are defined in the given specification; first operation is AlotingDroneZone(). Every drone has allotted its zone for designing a collision-free network.Code 39.
FailureDetection(drones : set of Drones) detected : boolext rd topo : [Topology]pre truepost exists d in set drones & detected = true <=>d.dnde.status = <FAILED_DRONE_DETECTED> andd.dnde.link = <NOT_LINKED> and d.dnde.condition = <FAULTED>;In postcondition of this operation, it is indicated that a drone is detected by stating that the drone is not linked and the condition of a drone is faulted; otherwise, failure not detected.Code 40.
ShiftingDrone(detected : bool) shifted : boolext rd topo : [Topology]rd crom : set of Controlroompre detected = truepost exists cr in set crom &shifted = true <=> cr.shift = <NEAREST_DRONE> andcr.shifted = <REPLACE_NEW_DRONE>;ChargingDrones()ext rd topo : [Topology]rd drones : set of Dronesrd crom : set of Controlroompre truepost exists d in set drones & exists cr in set crom &if d.battry = <LOWEST> thencr.charging = <CHARGE_FIRST> elsecr.charging = <CHARGE>;In ShiftingDrone, the postcondition describes that in case of any drone failure, the nearest drone is shifted to the place of failed drone and a new drone is placed at the empty place of that shifted drone. In ChargingDrones postcondition describes that drones are charging from time to time, but the neediest drone which has the lowest battery will charge first.


## 4.1. Internet of Things

The Internet of Things (IoT) describes the idea of connecting any gadget to the Internet and other devices. It is a vast network of interconnected items and people; all of which store and communicate information about how they are utilized and the environment around them. Devices with embedded sensors are connected to an Internet of Things infrastructure, which gathers data from a variety of sources and utilizes algorithms to transfer the most significant information to apps tailored to specific needs. It is an emerging technology; in the future, everything will be connected with the Internet of Things. IoT has made so many tasks easier and saves human time and effort. In our model, we have used drones with embedded sensors and cameras to monitor violations of SOPs and send signals to the control room for performing actions as required.


### 4.1.1. UML Diagram

The UML is a structured modeling language made up of a collection of standard diagrams that let system and software engineers describe, visualize, plan, and analyze software system elements, as well as advanced analytics and other nonsoftware components. In the proposed model, the UML is used in terms of sequence diagrams. Sequence diagrams are relationship diagrams that show how processes are performed. They track the interaction among objects in the form of coordinated work. Sequence diagrams are time-oriented, and they physically represent the structure of the process by diagram to describe time what messages are received and when.Figure4 illustrates the process of monitoring SOP’s violation in the form of a sequence diagram. The sequence diagram included six objects: sensor drone, actor drone, produce alarm, cluster head, control room, and persons.Figure 4
Monitoring sequence diagram.The process of monitoring SOP’s violation is described in the form of sequence diagram. The sequence diagram shows the sequence of all the communication between objects. Firstly, the sensor drone senses violation and sends signal to the actor drone; a return message is sent to sensor drone.After receiving signal from sensor drone, a return message is sent to actor drone. The actor drone will spray sanitizer and produce an alarm sound and then sends message to cluster head. Cluster head will send signal to control room for performing actions such as the control room sending an alarm message to the person who have violated SOPs; a return message is sent to the control room.Figure5 illustrates sequence diagram that describes the process of maintenance of network of drones. This diagram includes three objects: control room, drones, and new drones, and the sequence of communication between these objects is illustrated using diagram.Figure 5
Maintenance sequence diagram.In case of any failure, the control room will find a failed drone; a return message action performed is sent to the control room. Then, the nearest drone will be shifted to the place of failed drone; the shifting process will continue until there exists a place where a new drone will be placed. The control room sends signal to the new drone as placed new drone, and a return message is sent to the control room.The shifting of drones will be collision-free as the drones have allotted their zones. Each drone has its zone, and when a new drone will be placed, the nearest drone will shift to the place of failed drone and new drone will be placed to the empty space.In Figure6, the sequence of communication of medical delivery service process is described in a sequence.Figure 6
Identification sequence diagram.This diagram includes seven objects that are wearable sensors, sensor drones, actor drones, cluster head, control room, persons, and medicine drone. The sequence of communication between these objects is illustrated using this sequence diagram. Firstly, the wearable sensors will sense symptoms of COVID-19 and send a signal to sensor drone; the sensor drone will send a signal to the actor drone; the actor drone will spray sanitizer and produce an alarm sound to alert the person and then sends a signal to the cluster head. The cluster head will send a signal to the control room for further actions. The control room refers alert to people and gives an order to the medicine drone to provide medical services to the patients’ homes.


## 4.1.1. UML Diagram

The UML is a structured modeling language made up of a collection of standard diagrams that let system and software engineers describe, visualize, plan, and analyze software system elements, as well as advanced analytics and other nonsoftware components. In the proposed model, the UML is used in terms of sequence diagrams. Sequence diagrams are relationship diagrams that show how processes are performed. They track the interaction among objects in the form of coordinated work. Sequence diagrams are time-oriented, and they physically represent the structure of the process by diagram to describe time what messages are received and when.Figure4 illustrates the process of monitoring SOP’s violation in the form of a sequence diagram. The sequence diagram included six objects: sensor drone, actor drone, produce alarm, cluster head, control room, and persons.Figure 4
Monitoring sequence diagram.The process of monitoring SOP’s violation is described in the form of sequence diagram. The sequence diagram shows the sequence of all the communication between objects. Firstly, the sensor drone senses violation and sends signal to the actor drone; a return message is sent to sensor drone.After receiving signal from sensor drone, a return message is sent to actor drone. The actor drone will spray sanitizer and produce an alarm sound and then sends message to cluster head. Cluster head will send signal to control room for performing actions such as the control room sending an alarm message to the person who have violated SOPs; a return message is sent to the control room.Figure5 illustrates sequence diagram that describes the process of maintenance of network of drones. This diagram includes three objects: control room, drones, and new drones, and the sequence of communication between these objects is illustrated using diagram.Figure 5
Maintenance sequence diagram.In case of any failure, the control room will find a failed drone; a return message action performed is sent to the control room. Then, the nearest drone will be shifted to the place of failed drone; the shifting process will continue until there exists a place where a new drone will be placed. The control room sends signal to the new drone as placed new drone, and a return message is sent to the control room.The shifting of drones will be collision-free as the drones have allotted their zones. Each drone has its zone, and when a new drone will be placed, the nearest drone will shift to the place of failed drone and new drone will be placed to the empty space.In Figure6, the sequence of communication of medical delivery service process is described in a sequence.Figure 6
Identification sequence diagram.This diagram includes seven objects that are wearable sensors, sensor drones, actor drones, cluster head, control room, persons, and medicine drone. The sequence of communication between these objects is illustrated using this sequence diagram. Firstly, the wearable sensors will sense symptoms of COVID-19 and send a signal to sensor drone; the sensor drone will send a signal to the actor drone; the actor drone will spray sanitizer and produce an alarm sound to alert the person and then sends a signal to the cluster head. The cluster head will send a signal to the control room for further actions. The control room refers alert to people and gives an order to the medicine drone to provide medical services to the patients’ homes.


## 4.2. Graph Theory

Graph theory is a combination of nodes and connections, and the communication between them can be represented. In our model, the graph theory is used to represent the whole proposed system by nodes and connections and communication between them.In Figure7, the monitoring process of the cluster-based proposed system is described in the form of graphs. Graph theory consists of nodes and edges. Wearable sensor node is connected to sensor drone nodes, and sensor drone nodes are connected to actor drone. Actor drones are connected to cluster heads.Figure 7
Graph of monitoring.Cluster head is connected to the other cluster heads, and every cluster head is connected to control room. These connections of nodes represent communication between nodes and edges during monitoring violations of SOPs.In Figure8, the network maintenance of the proposed system is described in graph theory which is composed of nodes and edges. Sensor drone nodes are connected to every other sensor drone node and also connected to actor drone nodes. The actor drone is connected to cluster head to send a signal to the other cluster head, and every cluster head is connected to the control room. Cluster heads can communicate with each other. In case of any drone failure, the failed drones will be detected; then, the nearest drone will shift to place of a failed drone, and then, the new drone will be placed in empty space. This shifting process is collision-free.Figure 8
Graph theory of maintenance.


## 4.3. Formal Method

Formal methods are procedures for describing complex systems mathematically. By creating a mathematically robust model of a complex system, programmers can not only validate the system’s features more thoroughly but also use mathematical evidence as an addition to system testing to ensure accurate behavior. We utilized formal method for specification in the VDM-SL language. To ensure the system’s accuracy, the validation was carried out utilizing the resources offered in the VDM-SL toolbox.Code 1.
typesID = token;Droneid = token;Statuss = <ACTIVE>|<SLEEP>;Embeddedsensor = token;Camera = token;Enrgy = <HIGH>|<LOW>;Alarm = <on>|<off>;Violation = <SOCIAL_DISTANCING>|<MISSING_MASK>;ViolationDetection = <VDETECTED>|<VNOTDETECTED>;CRAction = <WARNING_MESSAGE_TO_PERSONS>;SdroneMode = <IDLE>|<WORKING>;SDroneAction = <SENSE_VIOLATION>|<INFO_TO_ACTORDRONE>;AdroneMode = <IDLE>|<WORKING>;ADroneAction = <INFO_TO_CLUSTERHEAD>|<SANITIZATION>|<PRODUCE_ALARM>;ClusterHeadMode = <IDLE>|<WORKING>;ClusterHeadAction = <INFO_SENDTO_CR>;valuesSdinfeet: nat =6;In given specification, the types of the system are defined; first field is ID with type token. Second field is Droneid defined as a token type; third field is statuss which is defined as enumeration type which have 2 states active or sleep. Embeddedsensors and Camera are defined as token type. Enrgy is defined as it can be either high or low. The next two fields Alarm and Violation are also defined as enumeration types; both have two states. Every drone (sensor, actor, and cluster head) mode is defined as either IDLE or WORKING. In values, social distancing mearing in feet is valued as Sdinfeet.Code 2.
Sgnl :: received:boolnot_recieved:bool;Infor :: received:boolnot_recieved:bool;Database :: ID : tokenPid : IDperson : tokenpersonDetails : token;Drones :: Sensordrone: set of SDroneactordrones : set of ADroneembeddedsensor: Embeddedsensorcamera: Cameraviolationdetection:ViolationDetection;In above specifications, some composite objects are defined such as Sgnl and Info is defined as bool type which means it will be true or false. Database consists of four fields; ID defined as token, Pid as ID type, person, and presonDetails is defined as token. In the next line, Drones is a composite object which have five fields; first is Sensordrone defined as a set of SDrone and actordrones defined as a set of ADrone; next is embeddedsensor defined as Embeddedsensor type, camera is defined as Camera, and violationdetection is defined as ViolationDetection.Code 3.
Nde::Ndeid:IDenrgy:Enrgystatuss:Statusssgnl:Sgnlinfor : Infor;Edgeesss = set of Edgeeinv edg == forall mk_(Ndeid1,Ndeid2)in set edg &mk_(Ndeid2,Ndeid1) in set edg;Edgee = ID∗IDinv eg == let mk_(Ndeid1,Ndeid2) =eg in Ndeid1<>Ndeid2;In the given specification, the invariant of node describes that every node has a connection with every other node but a node is not connected to itself which means no loop exists.Code 4.
Controlroom ::cr: IDdb : map ID to Databasedrones : set of Dronesinfo : Inforcraction : CRActioninv mk_Controlroom( -,db,-,-,-)== forall person in set dom db & person = db(person).personDetails;In given specifications, Controlroom has five fields and the invariant of control room described that the control room has information of every person in the target area.Code 5.
SDrone::sdNde: NdesdNdemode: SdroneModesdNdeaction: SDroneActionviolation: Violationinv mk_SDrone(sdNde, sdNdemode, sdNdeaction, violation) == sdNde.enrgy = <HIGH>and sdNdemode = <WORKING> <=> sdNdeaction = <SENSE_VIOLATION>and if Sdinfeet < 6 or violation = <MISSING_MASK> thensdNdeaction = <INFO_TO_ACTORDRONE> else sdNdemode = <IDLE>;SDrone is defined as a composite object, and the invariant of SDrone describes that energy of sensor drone is high and mode of sensor drone will be working if and only if sensor drone will sense violation like missing mask or social distancing less than 6 feet, and then, sensor drone will send signal to actor drone or no violation found.Code 6.
ADrone::actordrone: Ndeactordronemode: AdroneModeactordroneaction: ADroneActioninv mk_ADrone(actordrone,actordronemode, actordroneaction) == actordrone.enrgy = <LOW> and actordronemode = <IDLE>and actordronemode = <WORKING> <=> actordrone.sgnl.received = true=> actordroneaction = <SANITIZATION> and actordroneaction = <INFO_TO_CLUSTERHEAD>;ADrone is identified as a composite object. The invariant indicates that the mode of actor drone is idle at first, and it goes in working mode if actor drone receives a signal from sensor drone. If actor drone receives a signal from sensor drone, actor drone will begin sanitization and send information to the cluster head.Code 7.
ClusterHead :: chNde : Ndesendssgnl : set of Dronesactdrone : set of ADronechmode: ClusterHeadModechaction: ClusterHeadActioninv mk_ClusterHead(chNde, -, -, chmode, chaction) == chNde.enrgy = <HIGH> and if chNde.sgnl.received = true then chmode = <WORKING> and chaction = <INFO_SENDTO_CR> else chmode = <IDLE>;Clusterhead is specified as a composite object which includes five fields, and the invariant describes that the energy of cluster head is high, and mode of cluster head will become working if and only if the cluster head receives signal from actor drone, and then, cluster head will send info to control room for further operations, or the mode will remain idle.Code 8.
ClusterHead :: chNde : Ndesendssgnl : set of Dronesactdrone : set of ADronechmode: ClusterHeadModechaction: ClusterHeadActioninv mk_ClusterHead(chNde, -, -, chmode, chaction) == chNde.enrgy = <HIGH> and if chNde.sgnl.received = true then chmode = <WORKING> and chaction = <INFO_SENDTO_CR> else chmode = <IDLE>;In the above specification, Cluster is defined as a composite object which includes four fields which are clusterhead, sensordrones, actordrones, and egd. The invariant of cluster describes that every node has a connection, sensor drone has a connection with other sensor drones, and sensor drone has a connection with actor drone. Actor drones have a connection with other actor drones, and every actor drone has a connection with cluster head.Code 9.
Topology :: clushead : set of ClusterHeadcrm : set of Controlroomclusterr : set of Clusteredgs : Edgeesssinv mk_Topology(clushead, crm, clusterr, edgs) ==forall ch in set clushead &exists crr in set crm &exists cc in set edgs &mk_(ch.chNde.Ndeid, crr.cr) = cc andforall cc in set edgs &exists cl1,cl2 in set clusterr &mk_(cl1.clusterhead.chNde.Ndeid,cl2.clusterhead.chNde.Ndeid) = cc andforall cl1, cl2 in set clusterr &exists cc in set edgs &mk_(cl1.clusterhead.chNde.Ndeid,cl2.clusterhead.chNde.Ndeid) = cc;In the above specifications, the graph theory-based topology of monitoring is described that includes clusters. Every cluster has a cluster head, and each cluster head has a connection with every other cluster heads, and every cluster head has a connection with control room.Code 10.
state SopsMonitoring oftopo : [Topology]sdrones : set of SDroneadrone : set of ADroneclusters : set of Clusterch : set of ClusterHeadcrom : set of Controlroomedg : Edgeesssinit sm == sm = mk_SopsMonitoring(nil, {},{}, {}, {}, {},{})endThe state of the monitoring system is defined which includes seven fields, and these will be used in the dynamic part of specification.Code 11.
operationsSOPsViolationDetection(cluster : Cluster) detected : boolext rd topo : [Topology]rd sdrones : set of SDronepreexists sd in set sdrones & sd in set cluster.sensordronespost detected <=> forall sd in set sdrones &sd.sdNdemode = <WORKING> andSdinfeet < 6 and sd.violation = <MISSING_MASK> and sd.sdNdeaction = <INFO_TO_ACTORDRONE>;In above specifications, the dynamic part of the system is defined. The pre/postcondition describes that the violations of SOPs are detected if and only if the mode of sensor drone is working and social distancing is less than 6 feet and mask is missing, and sensor drone sends info to actor drone.Code 12.
Adperformingactions(detected : bool) action : boolext rd topo : [Topology]rd adrone : set of ADronepre detected = truepost action <=> forall ad in set adrone &ad.actordrone.sgnl.received = true andad.actordronemode = <WORKING> and ad.actordroneaction = <PRODUCE_ALARM> and ad.actordroneaction = <SANITIZATION> and ad.actordroneaction = <INFO_TO_CLUSTERHEAD>;Adperformingactions describes the actions of actor drones. The pre/postcondition describes that actor drone mode will be working and will produce alarm sound and do sanitization and then sends violation information to the cluster head.Code 13.
InfoTransmitingtoControlroom(action : bool) transmited : boolext rd topo : [Topology]rd ch : set of ClusterHeadrd crom : set of Controlroompre action = truepost transmited <=> forall cluh in set ch &cluh.chNde.infor.received = true and cluh.chaction = <INFO_SENDTO_CR>;In the above operation, information is now transmitting to control room for further actions. The postcondition describes that when cluster head receives information from actor drone, it will send violation information to the control room.Code 14.
ControlroomActions(transmited : bool)ext rd topo : [Topology]rd crom : set of Controlroompre transmited = truepost exists cr in set crom &http://cr.info/.received = true => cr.craction = <WARNING_MESSAGE_TO_PERSONS>;The above operation describes the actions of the control room. The postcondition describes that when control room will receive information from cluster head, then control room sends warning message to the person.Another module of the proposed system is identifying corona patients by using wearable sensors. Formal model of this module is given below.Code 15.
typesID = token;Energy = <HIGH>|<LOW>;InfectInformation = <INFORMATION_SENT_to_SDRONE>|<INFORMATION_RECIEVED>|<NO_INFORMATION>;PeopleCondition = <NATURAL>|<FATIGUE>|<COUGH>;SdroneMode = <IDLE>|<WORK>;Statuss = <ACTIVE>|<SLEEP>;SDroneAction = <SGNL_TO_ACTORDRONE>;ActorDroneMode = <IDLE>|<WORK>;ActorDroneAction= <PRODUCE_ALARM>|<SANITIZATION>|<INFORMATION_TO_CLUSTERHEAD>;ClusterHeadMode = <IDLE>|<WORK>;ClusterHeadAction = <INFORMATION_SENDTO_CR>;MedDroneMode = <IDLE>|<WORK>;MedDroneAction= <DELIVER_KIT>;Ctrlaction = <ORDER_TO_MEDDRONE>|<MESSAGE_TO_PEOPLE>;In the above specifications, all the types are defined that will be used in the next specifications. First is ID defined as token; next all fields are defined as enumeration types that have different states, some have two and some have more than two. Every type of drone has two modes idle or working, and they have different actions. Sdrone has an action of signal to actor drone, and actor drone has actions which are produced alarm and sanitization and sends information to the cluster head. Cluster head action is sending info to the control room, and medicine drone action is to deliver medicine, and control room actions are issuing an order to medicine drone and send warning message to people.Code 16.
Sgnl :: sgnl_recieved:bool;Information :: Information_recieved:bool;Database :: peopleid : IDpeopleInformation : token;BodyBodyTemperature ::bodybodyBodyTemperature:real natbodybodyBodyTemperature:real;Rsystem:: bodyrsystem:real natrsystem:real;In above specifications, some composite objects are defined Sgnl and Information is defined as Boolean type. The database is defined as a composite object with a peopleid and peopleInformation of token type. Some COVID-19 indicators, such as fatigue and coughing, as well as body temperature, are considered to diagnose the patient.Code 17.
Nde::ndeid:IDenergy:Energystatuss:Statusssgnl:SgnlInformation:Information;EDGSSs = set of EDGSSinv EDGss == forall mk_(ndeid1,ndeid2)in set EDGss &mk_(ndeid2,ndeid1) in set EDGss;EDGSS = ID∗IDinv eg == let mk_(ndeid1,ndeid2) =eg in ndeid1<>ndeid2;The invariant describes that any node is connected to every other node; for example, if ndid1 is connected to ndid2, therefore ndid2 is connected to ndid1 and one node is not connected to itself.Code 18.
WESensor::wnde:Ndepeople:map ID to DatabasebodyBodyTemperature:BodyBodyTemperaturersystem:Rsystempcond:PeopleConditionInformation:InfectInformationinv mk_WESensor(wnde, people, bodyBodyTemperature, rsystem, pcond, Information)==forall ps in set dom people & ps = wnde.ndeid and if bodyBodyTemperature.bodybodyBodyTemperature > bodyBodyTemperature.natbodybodyBodyTemperature andrsystem.bodyrsystem < rsystem.natrsystem or rsystem.bodyrsystem > rsystem.natrsystem andpcond = <FATIGUE> or pcond = <COUGH> thenwnde.statuss = <ACTIVE> and Information = <INFORMATION_SENT_to_SDRONE> else wnde.statuss = <SLEEP>;WESensor are listed as composite object and of node type. It has five fields: the first is people, which maps id to database, the second is bodyBodytemperature, which identifies temperature, and the third is rsystem, which identifies respiratory system. The fourth field is pcond and the last is information. The invariant demonstrates the conditions for identifying infected people using WESensor by comparing people body temperature and respiratory rates with natural temperatures and respiratory rates. If the body temperature is higher than natural, the respiratory rate is higher or lower than natural, and the person condition is fatigued or coughing, then sensor’s status will change to active; otherwise, the sensor’s status will remain sleep.Code 19.
SDrone::sdnde: Ndesdndemode: SdroneModesdndeaction: SDroneActionInformation: Informationinv mk_SDrone(sdnde, sdndemode, sdndeaction, -) == sdnde.energy = <HIGH>and sdndemode = <WORK> <=> sdnde.Information.Information_recieved = true =>sdndeaction = <SGNL_TO_ACTORDRONE>;Sdrone have four fields, and the invariant shows that the energy of sensor drone is high and mode is working if the sensor drone has received information; then, action will be sending signal to the actor drone.Code 20.
ActorDrone::adnde:NdeActorDronemode:ActorDroneModeActorDroneaction:ActorDroneActioninv mk_ActorDrone(adnde, ActorDronemode, ActorDroneaction)== adnde.energy = <LOW> and ActorDronemode = <IDLE>and ActorDronemode = <WORK> <=> adnde.Information.Information_recieved = true => ActorDroneaction = <SANITIZATION> andActorDroneaction = <PRODUCE_ALARM> andActorDroneaction = <INFORMATION_TO_CLUSTERHEAD>;The invariant of actor drone shows that mode of actor drone is working if actor drone receives a signal from sensor drone; then, action of actor drone will be to produce alarm and do sanitization and sends Information to cluster head.Code 21.
ClusterHead :: chnde : NdeActorDrone : set of ActorDronechmode: ClusterHeadModechaction: ClusterHeadActioninv mk_ClusterHead(chnde, -, chmode, chaction) == chnde.energy = <HIGH> and if chnde.Information.Information_recieved = true then chmode = <WORK> and chaction = <INFORMATION_SENDTO_CR> else chmode = <IDLE>;The invariant shows that the energy of cluster head is high, and if cluster head received information from actor drone, then cluster head mode will be working and action will be information sends to control room else mode will remain idle.Code 22.
CtrlR::cnode:IDctrlaction : Ctrlactiondb : map ID to DatabaseWESensors: set of WESensorsgnl:SgnlInformation:Informationinv mk_CtrlR( -,-,db,-,-,-)== forall people in set dom db & people = db(people).peopleInformation;The CtrlR is defined as a composite entity with four fields that involve database control room function as ctrlction wearable sensors as a collection of WESensor and sgnl. The invariant demonstrates that any user is in a certain domain of the database and has personal information of people.Code 23.
MedDrone::mdnde:Ndemdronemode:MedDroneModemdroneaction: MedDroneActioninv mk_MedDrone(mdnde, mdronemode, mdroneaction)== mdnde.energy = <LOW> and mdronemode = <IDLE>and mdronemode = <WORK> <=> mdnde.sgnl.sgnl_recieved = true => mdroneaction = <DELIVER_KIT>or mdronemode = <IDLE>;Medicine drones include two modes: idle and working, and actions include delivering medicines, and not delivering kits. MedDrone is described as a composite object that is used as a Nde type and has the following fields: drone mode and behavior as stated above. The invariants indicate that the mode is idle at first, and it will only work if and only if the medicine drone receives a signal from the control room, at which point the ctrlaction will deliver medication or not.Code 24.
Cluster :: clusterhead : ClusterHeadsensordrones : set of SDroneactordrones : set of ActorDroneWESensors: set of WESensorEDGss : EDGSSsinv mk_Cluster(clusterhead, sensordrones, actordrones, WESensors, EDGss) ==forall ws in set WESensors & exists c in set EDGss &forall sd in set sensordrones &mk_(ws.wnde.ndeid, sd.sdnde.ndeid) = c andforall sd1,sd2 in set sensordrones &exists c in set EDGss &mk_(sd1.sdnde.ndeid, sd2.sdnde.ndeid) = c andforall ad1, ad2 in set actordrones &exists c in set EDGss &mk_(ad1.adnde.ndeid, ad2.adnde.ndeid) = c andmk_(sd1.sdnde.ndeid, ad1.adnde.ndeid) = c andmk_(sd1.sdnde.ndeid, clusterhead.chnde.ndeid) = c andmk_(ad1.adnde.ndeid, clusterhead.chnde.ndeid) = c;Cluster is defined as a composite object which has six fields, and the invariant of cluster defines that every node has a connection; firstly, wearable sensor has a connection with sensor drone and sensor drone has a connection with actor drone and actor drones have connection with other actor drones and with cluster head.Code 25.
Topology :: clushead : set of ClusterHeadcrm : set of CtrlRmdrone : set of MedDroneclusterr : set of ClusterEDGsss : EDGSSsinv mk_Topology(clushead, crm, mdrone, clusterr, EDGsss) ==forall ch in set clushead &exists crr in set crm &exists cc in set EDGsss &mk_(ch.chnde.ndeid, crr.cnode) = cc andforall cc in set EDGsss &exists cl1,cl2 in set clusterr &mk_( cl1.clusterhead.chnde.ndeid,cl2.clusterhead.chnde.ndeid) = cc andforall cl1, cl2 in set clusterr &exists cc in set EDGsss &mk_(cl1.clusterhead.chnde.ndeid,cl2.clusterhead.chnde.ndeid) = cc andforall md in set mdrone &exists crr in set crm &exists cc in set EDGsss &mk_(crr.cnode, md.mdnde.ndeid) = cc;In above specifications, graph theory-based topology is defined which describe the connection of cluster with control room. Every cluster has a cluster head; therefore, one cluster head has a connection with other cluster head and also a connection with control room. The control room has a connection with medicine drone.Code 26.
state MedService oftopo : [Topology]sdrones : set of SDroneActDrone : set of ActorDronemeddrone : set of MedDroneclusters : set of Clusterch : set of ClusterHeadcrom : set of CtrlREDGss : EDGSSsinit ms == ms = mk_MedService(nil, {}, {}, {}, {}, {}, {},{})endThe attributes are initialized in the init function, and the system is defined as medical services in state.Code 27.
operationsIdentifyInfected(WESensors: WESensor) Identified : boolext rd topo : [Topology]rd sdrones : set of SDronepre truepost Identified <=> exists sd in set sdrones & WESensors.wnde.statuss = <ACTIVE> and WESensors.Information = <INFORMATION_SENT_to_SDRONE> => sd.sdndemode = <WORK> and sd.sdndeaction = <SGNL_TO_ACTORDRONE>;IdentifyInfected is an operation that takes wearable sensors as input and returns output in Identified such as True or false is determined. Pre/postcondition: the operation’s precondition is true. The postcondition indicates that the patient will be detected if and only if the wearable sensor status is activated and wearable sensors will send signal to sensor drone, and then, mode of sensor drone becomes active and action of sensor drone is send information to actor drone.Code 28.
ActorDroneActions(Identified:bool) action : boolext rd topo : [Topology]rd ActDrone : set of ActorDronepre Identified = truepost action <=> forall ad in set ActDrone &ad.adnde.sgnl.sgnl_recieved = true andad.ActorDronemode = <WORK> and ad.ActorDroneaction = <PRODUCE_ALARM> and ad.ActorDroneaction = <SANITIZATION> and ad.ActorDroneaction = <INFORMATION_TO_CLUSTERHEAD>;In the above operations, actions of actor drone is described which takes input identified and output action; in postcondition, it shows that action is true if actor drone receives a signal from actor drone and mode of actor drone will become working; then, action of actor drone will produce alarm and sanitization and send info to cluster head.Code 29.
IdentificationRepoted(action:bool) reported:boolext rd ch: set of ClusterHeadpre action = truepost reported <=> exists clush in set ch & clush.chnde.Information.Information_recieved = true and clush.chaction = <INFORMATION_SENDTO_CR>;IdentificationRepoted is an operation that takes a bool type input. Cr is described as a group of control rooms in the external clause. Pre/postcondition: the precondition specifies that the defined operation must be valid. The postcondition indicates that the identification is reported if and only if cr is in the control room collection and the control room has received the signal.Code 30.
MedicalDelivery(Identified: bool)ext rd meddrone: set of MedDronerd crom: set of CtrlRpre Identified = truepost forall md in set meddrone & exists ctrl in set crom & if ctrl.Information.Information_recieved = truethen ctrl.ctrlaction = <ORDER_TO_MEDDRONE> andctrl.ctrlaction = <MESSAGE_TO_PEOPLE> =>md.mdronemode = <WORK> else md.mdronemode = <IDLE>;Pre/postcondition: the precondition is stated as true and in postcondition if the control room receives the info, and then, control room will give an order to the MedDrone for the medical services and sends warning message to the person; otherwise, the mode of MedDrone will remain idle.Another module of the proposed model is maintenance of drones’ network such as in case of a drone failure new placement drone will be collision-free. Drones will be charged from time to time, and the neediest drone will charge first.Code 31.
typesID = token;BatteryStatus = <DOWN>|<LOWEST>;Voltage = <HIGH>|<LOW>;Info = <COMMUNICATING>|<NOT_COMMUNICATING>;Status = <FAILED_DRONE_DETECTED>|<NOT_DETECTED>;Link = <LINKED>|<NOT_LINKED>;Condition = <FAULTED>|<NOT_FAULTED>;Shift = <NEAREST_DRONE>;Empty_Space_Drone = <REPLACE_NEW_DRONE>;Charging = <CHARGE_FIRST>|<CHARGE>;In the above specification, different types of system maintenance are specified and their types are defined.Code 32.
Nde::ndeid:IDvoltage : Voltagestatus: Statuscondition: Conditionlink : Linkinfo : Info;Edgeesss = set of Edgeeinv edg == forall mk_(ndeid1,ndeid2)in set edg &mk_(ndeid2,ndeid1) in set edg;Edgee = ID∗IDinv eg == let mk_(ndeid1,ndeid2) =eg in ndeid1<>ndeid2;The invariant shows that each node is unique such as id of one node is not equal to id of other node that means any node is not connected to itself.Code 33.
Zones = <A>|<B>;Drones::dnde:Ndezones : Zonesbattry : BatteryStatusinv mk_Drones(dnde,-, -)== dnde.voltage = <LOW> anddnde.status = <FAILED_DRONE_DETECTED> <=>dnde.link = <LINKED> and dnde.condition = <FAULTED> or dnde.status = <NOT_DETECTED> <=>dnde.link = <NOT_LINKED> and dnde.condition = <NOT_FAULTED>;Controlroom ::cr: Ndecharging : Chargingshift : Shiftshifted : Empty_Space_Drone;The described specification states two composite objects Drones and Controlroom. Drones include three fields: dnode, zones, and battry. The invariant shows that a drone will be detected as failed if and only if a drone is not linked and condition of drone is faulted; otherwise, failure is not detected. Control room includes four fields: cr, charging, shift, and shifted.Code 34.
ClusterHead :: chnde : Ndeinv mk_ClusterHead(chnde)== chnde.voltage = <LOW> andchnde.status = <FAILED_DRONE_DETECTED> <=>chnde.link = <LINKED> and chnde.condition = <FAULTED> or chnde.status = <NOT_DETECTED> <=>chnde.link = <NOT_LINKED> and chnde.condition = <NOT_FAULTED>;Clusterhead composite object includes one field chnode, and invariant describes that cluster head will be detected as failed if and only if it is linked and condition is faulted; otherwise, cluster head is not failure detected.Code 35.
Cluster :: clusterhead : ClusterHeaddrones : set of Dronesedg : Edgeesssinv mk_Cluster(clusterhead, drones, edg) ==forall d1,d2 in set drones &exists c in set edg &mk_(d1.dnde.ndeid, d2.dnde.ndeid) = c andforall d1 in set drones &exists c in set edg &mk_(d1.dnde.ndeid, clusterhead.chnde.ndeid) = c;Cluster includes three fields and that the cluster is composed of drones and cluster head. The invariant describes that every drone has a connection with every other drone and drones have a connection with cluster head.Code 36.
Topology :: clushead : set of ClusterHeadcrm : set of Controlroomclusterr : set of Clusteredgs : Edgeesssinv mk_Topology(clushead, crm, clusterr, edgs) ==forall ch in set clushead &exists crr in set crm &exists cc in set edgs &mk_(ch.chnde.ndeid, crr.cr.ndeid) = cc andforall cc in set edgs &exists cl1,cl2 in set clusterr &mk_(cl1.clusterhead.chnde.ndeid,cl2.clusterhead.chnde.ndeid) = cc andforall cl1, cl2 in set clusterr &exists cc in set edgs &mk_(cl1.clusterhead.chnde.ndeid,cl2.clusterhead.chnde.ndeid) = cc;Above specifications are graph-based topology which shows the connection between clusters and control room. Every cluster head is connected to other cluster head, and every cluster head is connected to control room. The connection is showed in form of nodes and edges.Code 37.
state Maintenance oftopo : [Topology]drones : set of Dronesclusters : set of Clusterch : set of ClusterHeadcrom : set of Controlroomedg : Edgeesssinit MN == MN = mk_Maintenance(nil, {}, {}, {}, {}, {})endThe State has defined all fields and their types which will be used in the dynamic model of the maintenance.Code 38.
operationsAlotingDroneZone() aloted : boolext rd topo : [Topology]rd drones : set of Dronespre truepost aloted = true <=> exists d1,d2 in set drones & d1 <> d2 andd1.zones = <A> and d2.zones = <B>;Operations are defined in the given specification; first operation is AlotingDroneZone(). Every drone has allotted its zone for designing a collision-free network.Code 39.
FailureDetection(drones : set of Drones) detected : boolext rd topo : [Topology]pre truepost exists d in set drones & detected = true <=>d.dnde.status = <FAILED_DRONE_DETECTED> andd.dnde.link = <NOT_LINKED> and d.dnde.condition = <FAULTED>;In postcondition of this operation, it is indicated that a drone is detected by stating that the drone is not linked and the condition of a drone is faulted; otherwise, failure not detected.Code 40.
ShiftingDrone(detected : bool) shifted : boolext rd topo : [Topology]rd crom : set of Controlroompre detected = truepost exists cr in set crom &shifted = true <=> cr.shift = <NEAREST_DRONE> andcr.shifted = <REPLACE_NEW_DRONE>;ChargingDrones()ext rd topo : [Topology]rd drones : set of Dronesrd crom : set of Controlroompre truepost exists d in set drones & exists cr in set crom &if d.battry = <LOWEST> thencr.charging = <CHARGE_FIRST> elsecr.charging = <CHARGE>;In ShiftingDrone, the postcondition describes that in case of any drone failure, the nearest drone is shifted to the place of failed drone and a new drone is placed at the empty place of that shifted drone. In ChargingDrones postcondition describes that drones are charging from time to time, but the neediest drone which has the lowest battery will charge first.


## 5. Result Analysis

We believe construction of formal models of real-world systems is not sufficient to get full benefits of formal methods. Formal modeling in VDM-SL means that the semantics are very precisely described and can be analyzed using computer tools conforming requirements of the system. The process of analyzing a formal system in this way is termed as validation to insure correctness of a system. Validation and verification are two major principals that play an important role in development of correct systems. Validation addresses whether the produced system really fulfils the system’s requirements. On the other hand, verification attempts to establish whether a particular phase of the software process meets the requirements. In fact, validation of abstract models is a prerequisite for entering of real world of verification.In this paper, various facilities available in the VDM-SL toolbox are used for model analysis of the system. Proof obligation and simulation are two main techniques used for the formal analysis. A proof obligation is a logical expression which must hold for internal consistency checking that insures a correct use of language syntax and semantics in the formal specification. The data types and definitions are evaluated to make it sure that it does not violate the invariant or constraints over the data types. The functions are evaluated on the inputs to verify that its output is correct under the assumptions provided in the model. Pre- and postconditions used in the function definitions are checked as part of the proof obligation.The VDM-SL toolbox supports the VDM-SL which provides facilities to analyze a precise range of models and ensure its correctness at the initial stages. The tool includes syntax checker, grammar checker, interpreter, and C++ code generator which provide features to validate and verify and the model. Syntax checker checks that the given specification is correct and it is according to the definition of the VDM-SL language. If syntax checkers accept the given specification, then it will allow other features. Type checker checks the types are correct and contains no run type or logical error according to the model’s requirements. The integrity checker provides ability of static checking and checks inconsistency of the model which includes integrity violations, type violations, pre- and postconditions. The C++ code generator helps to get consistency during specification of the model. The pretty printer is used for the compatible mode of documentation and converts specifications into a pretty printer version. The pretty printer syntax check shows that no error exists in syntax that violates the syntax of the VDM-SL. Each module of the proposed model has been analyzed, validated, and verified using available facilities in the VDM-SL toolbox.Figure9 illustrates that code is error-free; syntax checker verified that code is conferring to the syntax of VDM language. Type checker checked all runtime and logical errors. C++ helps to achieve consistency of the model.Figure 9
VDM-SL toolbox results of monitoring.Pretty printer is used for the compatible mode of documentation in any software development and converts specifications into pretty printer version that is used for documentation purpose.The integrity property window checks inconsistency of the model and shows integrity violation of the code to achieve a consistent model. The integrity property increases static verification and generates a list of probable integrity attributes.It assures internal inconsistencies and integrity violations in the model definition, such as data type violations, invariants, precondition, postcondition, and map domains. It analyzes the genuine expression; if it analyzes the false expression, there might be an issue.The analysis of monitoring module shows that the static and dynamic model of this specification is free of any syntax and type violation of the language. Therefore, the correctness is ensured for this module. All the specifications are validated and verified by VDM-SL toolbox checker facilities.Figure10 shows that the code of maintenance module is error-free. “S” demonstrates syntax checker; it checks the code that is it according to the definition of VDM-SL or not. “T” represents type checker; it checks logical and runtime errors of the code. C++ helps to find inconsistency of the code.Figure 10
VDM-SL toolbox results of maintenance.“P” represents pretty printer that is used to make a compatible mode and can be used for documentation purpose.The integrity property of maintenance module checks inconsistency of the static model and checks pre- and postconditions. There exist no inconsistencies in the given specifications.The given snapshot of this module shows that the model is validated and verified; therefore, the correctness is ensured.Figure11 illustrates that the specifications of medical services module are error-free; the syntax check is checked that shows the code is conferring to the syntax of VDM-SL, and type check verifies the runtime and logical errors. C++ is error-free, and pretty printer is used for documentation purpose in the code. This ensures the correctness of the model, and the integrity properties of medical services check the inconsistencies of the model. These property analyses help to make an error-free specification of this module.Figure 11
VDM-SL toolbox results of medical services.


## 6. Conclusion

The rapid spread of coronavirus has become the biggest problem for the whole world due to its viral nature. There is no proper cure that exists for COVID-19; therefore, it is essential to control the spread of this virus. The World Health Organization (WHO) has set up some standard operating procedures (SOPs) which contain social distancing, wearing a mask, and using sanitizer to control the spread of coronavirus. People are not strictly following these SOPs; therefore, this should be monitored that people are following SOPs or not. If people’s interactions are reduced, the spread of COVID-19 can be managed. Many techniques are contributing to minimizing the spread of virus.We had presented an IoT-based framework in this paper, which includes a network of cluster-based drones for the monitoring of SOP violations and performs an action such as producing alarm sound and sanitization and sends information to control room for further actions. The network is well maintained; in case of any failure of drones, the placement of new drones is collision-free as every drone has allotted its zone. Furthermore, wearable sensors are used to capture the movement of persons; when drones are monitoring, these wearable sensors are used to monitor people’s temperature and respiratory rates. If any person has high temperature or an unbalanced respiratory rate, the sensors send information to the network of drones for communication and to perform actions such as sanitization and producing alarm sound. The control room then gives a command to medicine drone to provide medical supplies to a person’s home who has been identified infected. Unified modeling language (UML) in terms of sequence diagram has been used to make the proposed model easily understandable by showing the flow of process in a sequence. Graph theory is used to represent the whole system and its connectivity using some suitable topology. The model is specified in Vienna Development Method-Specification language (VDM-SL) and ensured correctness by using the services available in the VDM-SL toolbox.



---

*Source: 6052771-2022-08-31.xml*