## 5 Formal Specification and Analysis
### Formal Specification of PCR Algorithm  
In this section, a formal specification of the proposed failure recovery algorithm for wireless sensor and actor network is described using Z. Formal analysis of the specification is provided using the Z/Eves toolset in the next section. First of all, topology under the wireless sensor and actor network is described, which must be maintained throughout the life of the network. The topology consists of a set of nodes and a set of edges. The set of nodes is a power set of _Node_ where _Node_ is assumed as a set at an abstract level of specification in Z notation. In modeling using sets in Z, a high level of abstraction is supposed. For example, we do not define any effective procedure for deciding whether an arbitrary element is a member of the abstract set. Consequently, _Node_ defined below is a set over which operators of set theory cannot be defined. For example, cardinality to know the number of elements in the _Node_ cannot be defined. Similarly, the subset, union, intersection and complement operators are not well-defined as well. To define such operations new set must be created based on the abstract set. The set of edges of the topology is a relation over the collection of the nodes. The topology schema is denoted by _Topology_ which consists of two variables _nodes_ and _edges_ contained in the first part of the schema. The invariants over the topology are defined in the second part of it:  
**Invariants**: (1) For every node in the network topology, there is an ordered pair (edge) such that the node is either first or the second element of the ordered pair. (2) For every edge in the network, there exist two nodes such that the nodes formulate a link called edge in the network topology. It is assumed that the topology is a connected graph, that is, for any two nodes there is an edge. Any isolated actor in the network is not a part of the network topology. Wireless sensor actor networks employ a number of sensor nodes that report an event of interest to one or multiple actors. The sensors are inexpensive and have scarce resources, whereas, actors are more powerful nodes in terms of energy, communication and computation power. Formal specification of the sensor is described below by the schema Sensor. The schema contains five variables, namely, sensor identifier, its state, information about any event, neighbors and connectivity which are denoted by _id_, _state_, _information_, _neighbors_ and _connectivity_, respectively. The state is a two-valued variable used to check if any event is captured. In the _information_ variable, detail of the event is stored. As the sensor can communicate only with its neighbors, hence, information about neighbors is stored in the _neighbors_ variable. The _connectivity_ variable is used to check the status of the node which is either connected or disconnected to the network. [_Data_]; _S \(==\) Node State \(::=\) OK \(|\) NOTOK Connectivity \(::=\) CONNECTED \(|\) DISCONNECTED Sensor id: S state: State information: F Data neighbours: F Node connectivity: Connectivity \(\bullet\)\(\bullet\  
**Invariants**: (1) The sensor is responsible for continuous monitoring of the environment. If an unwanted object is detected the data will be collected by the sensor and stored in the _information_ variable. In this property, it is stated that if state of sensor is normal (_OK_) then there is no information in the sensor. If state of sensor is not normal then there must be some information stored in the sensor. (2) As the wireless sensor and actor network is a distributed system, hence, it is assumed that every node will have information about its neighbours at 1-hop. In this property, it is stated that a node is connected if the collection of its neighbours is a non-empty set. The node is disconnected if the set of its neighbours is an empty set. The role of an actor is extremely crucial for a timely response in order to prevent any serious consequences after a sensor node has reported an event.