Abstract
An unattended deployment of wireless sensor and actor networks in a harsh and inhospitable environment may cause its failure by partitioning it into the disjoint segments. Although many variants of this problem are addressed using different approaches, it still needs to be investigated due to its various applications. In this article, an efficient, localized, hybrid failure detection and recovery algorithm is proposed which assumes planned deployment of nodes. The algorithm is approximate and distributed as its topology is partitioned into subnets localizing failure recovery procedure and efficient as the time complexity is reduced from nondeterministic polynomial-time-hard to polynomial time. The algorithm is hybrid as pre-failure planning and post-failure recovery is assumed for the critical nodes. Graph-based model is designed to represent static part which is then transformed into a formal model using Vienna Development Methodspecification language. The static model consists of subnets, circular topology, sensors, actors, and gateways as composite objects in Vienna Development Methodspecification language. The dynamic model is developed by defining its state space, functions, and possible operations to describe the failure recovery procedure. Invariants are defined on static model to assure correctness, and pre/post conditions are used in the dynamic model to control the behavior preventing system to enter into an unwanted situation. The formal specification is analyzed using Vienna Development Methodspecification language Toolbox to visualize the model.