Learning-based routing in mobile wireless sensor networks: Applying formal modeling and analysis

Limited energy supply is one of the main concerns when dealing with wireless sensor networks (WSNs). Therefore, routing protocols should be designed with the goal of being energy efficient. In this paper, we select a routing protocol which is capable of handling both centralized and decentralized routing. Mobility, a priori knowledge of the movement patterns of the nodes is exploited to select the best routing path, using a Bayesian learning algorithm. Generally, simulation-based tools cannot prove if a protocol works correctly, but formal modeling methods are able to validate that by searching for failures through all possible behaviors of network nodes. This paper presents a formal model for a learning-based routing protocol for WSNs, based on a Bayesian learning method, using an Structural Operational Semantics (SOS) style. We use the rewriting logic tool Maude to analyze the model. Our experimental results show that decentralized approach is twice as energy-efficient as the centralized scheme. It also outperforms the power-sensitive AODV (PS-AODV) routing protocol (i.e. a non-learning efficient protocol). We use the Maude tool to validate a correctness property of the routing protocol. Our formal model of Bayesian learning integrates a real dataset which forces the model to conform to the real data. This technique seems useful beyond the case study of this paper.