Implementing Partitioning Detection and Connectivity Restoration in WSAN Using VDM-SL

Recently the interest in wireless sensor and actor networks has increased tremendously. Although there has been significant improvement in WSANs, but still many challenges are needed to overcome the issues of critical applications. In most of the published work the focus is on the performance analysis of non-functional properties but correctness of the approach is still ignored which is very important in large and complex systems. This paper introduces an alternative approach for formal specification, implementation and analysis of the Partitioning Detection and Connectivity Restoration (PCR) algorithm in WSANs. We model WSAN as a dynamic graph and use VDM-SL to describe the formal specification of the algorithm. Invariants are used to validate the algorithm and pre and post conditions confirm the correctness of the operations. VDM-SL is a formal specification language used for implementation of software systems and to illustrate detailed level examination. The PCR algorithm specification is implemented, verified, validated and analyzed through the VDM-SL toolbox.