## 5 Formal Specification and Analysis
### Formal Specification of PCR Algorithm
That is why it needs more information about its neighbors. The schema _Neighbour_ (used in definition of actor) consists of five variables, namely, _neighbour_ (identifier), _neighbours_, _type_, _criticality_ and _distance_. The variable _criticality_ is used because non-critical backup is preferred and, hence, this information is required for backup identification and assigning. The distance variable is used as it is also required for backup assigning and analysis. _Sensors_ **2012**, _12_  
_Type \(::=\) ACTOR \(|\) SENSOR_  
_Neighbour___  
_neighbour: Node_  
_neighbours: F Node_  
_type: Type_  
_criticality: Criticality_  
_distance:_ \(\mathbb{N}\)__  
As wireless sensor actor networks employs a number of sensors that report to actors and the concerned actors respond to events by following the network topology in order to prevent any serious consequences. The network is denoted by the schema _WSAN_ which consists of three components, that is, _sensors_, _actors_ and _topology_. The _sensors_ is a power set of _Sensor_ and similarly _actors_ is a power set of _Actor_. The definitions of sensor, actor and topology are already described by using the schemas _Sensor_, _Actor_ and _Topology_, respectively. All of these three main components of the network are put in first part of the schema and invariants are defined in second part of the schema in terms of predicates for well definedness. _WSAN___  
_Topology_  
_sensors: F Sensor_  
_actors: F Actor_  
_\(\forall s\): Sensor \(|\)\(s\in\)sensors \(\bullet\)\(s\). \(id\in\)nodes_  
_\(\forall n\): Node \(|\)\(n\in\)nodes \(\bullet\)\((\exists s\): Sensor \(|\)\(s\in\)sensors \(\bullet\)\(n=s\). \(id)\)_  
_\(\vee\)\(\langle\exists a\): Actor \(|\)\(a\in\)actors \(\bullet\)\(n=a\). \(id)\)_  
_\(\forall s\): Sensor \(|\)\(s\in\)sensors_  
_\(\forall n\): Node \(|\)\(nbr\in s\). neighbours \(\bullet\)\((s\). \(id\), \(nbr)\in\)edges_  
_\(\forall a\): Actor \(|\)\(a\in\)actors \(\bullet\)\(a\). \(id\in\)nodes_  
_\(\forall a\): Actor \(|\)\(a\in\)actors \(\bullet\)\((a\). \(id\), \(a\). backup \(.\)neighbour\()\)\(\in\)edges_  
_\(\forall a\): Actor \(|\)\(a\in\)actors \(\bullet\)\(\forall nbr\): Neighbour \(|\)\(nbr\in a\). neighbours_  
_\(\bullet\)\((a\). \(id\), \(nbr\). neighbour\()\)\(\in\)edges_  
_\(\forall\)actor: Actor \(|\)\(actor\in\)actors_  
_\(\exists\)sensor: Sensor \(|\)\(sensor\in\)sensors \(\bullet\) actor. \(id=sensor\). \(id\)_  
_\(\forall s\): Sensor \(|\)\(s\in\)sensors_  
_\(\exists a\): Actor; path: seq Node \(|\)\(a\in\)actors \(\wedge\)_ ran _path \(\subseteq\)nodes_  
_\(\forall i\): \(\mathbb{N}\)\(|\)\(i\in\)dom path \(\wedge\)\(i\)\(1\).. \(\#\)path - \(1\)\(\bullet\) path \(1=s\). \(id\)_  
_\(\wedge\)path \((\#\)path\()=a\). \(id\)\(\wedge\)\((\)path \(i\), path \((i+1))\)\(\in\)edges_  
**Invariants**: (1) Every sensor of the WSAN is a node in the topology. (2) Every node in the topology is either a sensor or an actor of the WSAN. (3) Every neighbour of every sensor is connected in the topology. (4) Every actor of the WSAN is also a node in the topology. (5) Any neighbour of the backup of an actor is not connected directly to the actor. (6) Every neighbour of every actor is connected with the actor in the topology. (7) For every actor there is a sensor having same identifier, that is, every actor acts as a sensor as well. (8) For every sensor there is a path from the sensor itself to some of the actors in the network. That is for every sensor there is, at least, one actor responsible for receiving information and performing an action. The path is defined as a sequence of nodes. The first element in the sequence is sensor and the last element is actor. Further, for every pair of consecutive elements in the sequence, it is an ordered pair and an edge in the network topology. As we know, failure of a critical actor divides the network into disjoint sub-networks. Hence, identification of critical actors is important after deployment of the network.