## 5 Formal Specification and Analysis
### Formal Specification of PCR Algorithm
For this purpose, actors need to coordinate with each other for an effective and optimal response synchronizing the required operations. Therefore, actors establish and maintain inter-actor network topology in order to enable such communication. As the failure of a critical actor may partition the inter-actor network into a disjoint sub-network, consequently, backup preferably non-critical to every such node is required for the failure recovery. The backup actor node continuously monitors its critical, if any failure is detected then it initiates the recovery process by moving towards the primary until connectivity is restored. Formal specification of the actor is described below by the schema _Actor_. Based on the functionality, eight variables are extracted to describe role of an actor. As each actor must be uniquely identified like a sensor, hence, the first variable is the actor identifier. The second variable is used to define the type of the actor node and has two values, _i.e._, either critical or non-critical. As in case of failure of a critical node, the backup is required, the third variable is used for this purpose. Of course the backup must be from its neighbors. The fourth variable is for storing information about neighbors, because an actor must know about its neighbors for a failure recovery. The _connectivity_ variable is to check if the actor is itself connected or disconnected. The last three variables are used to store information about the reported events from the sensors. The _detected_ variable is used for storing information about all reported events. The _pending_ variable is used to record events for which the action is still required. And the last one variable _completed_ is used for recording the information about events for which action is completed. _A == Node_  
_Criticality ::= CRITICAL | NONCRITICAL_  
_Actor_  
_id: A_  
_type: Criticality_  
_backup: Neighbour_  
_neighbours: F Neighbour_  
_connectivity: Connectivity_  
_detected: F Detected_  
_pending: F Detected_  
_completed: F Detected_  
_type = CRITICAL \(\Rightarrow\)# neighbours < 2 \(\wedge\) type = NONCRITICAL\(\Rightarrow\)# neighbours > 2_  
_backup. type = ACTOR_  
**Invariants**: (1) The node is critical if it has, at most, two neighbors and after its removal the network is partitioned, otherwise, the node is non-critical. (2) The backup of the actor node must be an actor node. (3) The backup of an actor node must be among one of its neighbours. (4) The backup of the node is the one with least degree among its neighbours. (5) The sensor node is connected if it has, at least one neighbour, otherwise it is disconnected. (6) As a safety property, in the set of detected sensors, if the action is pending then the detected issue exists in the database of the sensor. (7) In the set of detected sensors, if the action is completed then information is removed from the database of the sensor to make an optimized usage of the storage. (8) For each detected sensor, the action is either completed or pending. (9) For each sensor, if it is in the list of pending or completed then it must be in the list of detected sensors. The properties 8 and 9 are described for the consistency. The schema _Detected_ defined below is used to store the information about the reported events from any sensor to an actor. The schema consists of three variables, namely, reporting sensor identifier, the event details and action having two values, that is, completed or required. _Action \(::=\) PENDING \(|\) COMPLETED_  
_Detected_  
_sensor: Node_  
_data:_\(\mathbb{F}\) _Data_  
_action: Action_  
In case of sensor definition, only neighbor identifiers were defined, but in case of actors, more information about neighbors is required. This is because a sensor needs only to sense the event and report to the responsible actor(s). However, the actor is assumed more powerful and its job is to coordinate with other actors to complete the activity efficiently, accurately and effectively after receiving the information from the sensors.