Formal Specification and Validation of a Localized Algorithm for Segregation of Critical/Noncritical Nodes in MAHSNs

Timely segregation of critical/noncritical nodes is extremely crucial in mobile ad hoc and sensor networks. Most of the existing segregation schemes are centralized and require maintaining network wide information, which may not be feasible in large-scale dynamic networks. Moreover, these schemes lack rigorous validation and entirely rely on simulations. We present a localized algorithm for segregation of critical/noncritical nodes (LASCNN) to the network connectivity. LASCNN establishes and maintains a k-hop connection list and marks a node as critical if its k-hop neighbours become disconnected without the node and noncritical otherwise. A noncritical node with more than one connection is marked as intermediate and leaf noncritical otherwise. We use both formal and nonformal techniques for verification and validation of functional and nonfunctional properties. First, we model MAHSN as a dynamic graph and transform LASCNN to equivalent formal specification using Z notation. After analysing and validating the specification through Z eves tool, we simulate LASCNN specification to quantitatively demonstrate its efficiency. Simulation experiments demonstrate that the performance of LASCNN is scalable and is quite competitive compared to centralized scheme with global information. The accuracy of LASCNN in determining critical nodes is 87% (1-hop) and 93% (2-hop) and of noncritical nodes the accuracy is 91% (1-hop) and 93% (2-hop).