## 5 Formal Specification and Analysis
### Formal Specification of PCR Algorithm
Formal specification of identifying critical nodes is given below using the schema _CriticalsIdentification_. The schema takes _WSAN_ as input and returns the set of critical nodes as output by using the _criticals!_ variable. In Z notation, the symbol \"!\" is used after end of the output variable. As defined in the informal description of PCR algorithm, it employs a simple localized cut-vertex detection procedure that only requires 1-hop positional information to detect critical nodes. The 1-hop information is stored in terms of neighbors of any node. The formal description of the critical nodes identification procedure is given in second part of the schema and its informal description is provided in terms of properties following the schema. _CriticalsIdentification___  
\(\Xi\)_WSAN_  
_criticals! :_ F _Actor_  
\(\forall a\)_: Actor_\(|\)\(a\in\)_criticals!_\(a\in\)_actors_  
\(\forall\)_: cat_\(\forall\)  
is determined that the backup is critical or non-critical. A non-critical actor is preferred to serve as backup. A non-critical actor with the least degree is a suitable candidate. The close backup actor is preferred in order to reduce the movement overhead and shorten the recovery time. _BackupsAssigning_  
\(\Delta\)_WSAN_  
_CriticalsIdentification_  
\(\forall\)_a: Actor / a_ \(\in\) _criticals!_ _(\(\exists\)_hbr: Neighbour_  
\(\mid\)_nbr_ \(\in\) _a. neighbours_ \(\wedge\)_nbr_ \(.\) _criticality_ \(=\)_NONCRITICAL_  
\(\wedge\) _(\(\forall\)nbr1: Neighbour / nbr1_ \(\in\) _a. neighbours_  
\(\wedge\)_nbr1_ \(\
eq\)_nbr_ \(\wedge\)_nbr_ \(.\) _neighbours_ \(\in\)__F Node_ \(\wedge\)_nbr1_ \(.\) _neighbours_ \(\in\)__F Node_  
\(\bullet\)_# nbr_ \(.\) _neighbours_ \(\leqslant\)_# nbr1_ \(.\) _neighbours_ \(\rangle\)_a_ \(.\) _backup_ \(=\)_nbr_  
\(\vee\) _(\(\exists\)nbr1: Neighbour / nbr1_ \(\in\) _a. neighbours_  
\(\wedge\) _(\(\forall\)nbr2: Neighbour / nbr2_ \(\in\) _a. neighbours_ \(\wedge\)_nbr2_ \(\
eq\)_nbr1_  
\(\bullet\)_nbr1_ \(.\) _distance_ \(\leqslant\)_nbr2_ \(.\) _distance_ \()\(.\) _a. backup_ \(=\)_nbr1_)_  
**Properties**: For every critical actor of WSAN as identified by the above schema, the backups are assigned by the following criteria: backup must be preferably non-critical, has the least degree among its neighbours and, has least distance as compared to all other backup candidates. In the above schemas, a formal procedure of identifying the critical nodes is defined and then a criteria of assigning a backup to the critical node is described. Now formal specification of assigning backups to the critical nodes is described below using the schema _CriticalsBackups_. The schema takes _WSAN_ as input and assigns the backups to the critical nodes using the variable _cribackups!_. At first the critical node is verified and then an appropriate neighbor to the critical node is assigned as a backup meeting the required criteria. In the backup assigning, initially, the backup neighbor is preferred to be non-critical. Then least degree and close distance properties are verified as preferred requirements. If no such backup exists, then the condition of non-criticality is relaxed, however, the other conditions of assigning the backup must be satisfied.