Formal modeling and analysis of learning-based routing in mobile wireless sensor networks

Abstract

Limited energy supply is a major concern when dealing with wireless sensor networks (WSNs). Therefore, routing protocols for WSNs should be designed to be energy efficient. This chapter considers a learning-based routing protocol for WSNs with mobile nodes, which is capable of handling both centralized and decentralized routing. A priori knowledge of the movement patterns of the nodes is exploited to select the best routing path, using a Bayesian learning algorithm. While simulation tools cannot generally prove that a protocol is correct, formal methods can explore all possible behaviors of network nodes to search for failures. We develop a formal model of the learning-based protocol and use the rewriting logic tool Maude to analyze both the correctness and efficiency of the model. Our experimental results show that the decentralized approach is twice as energy-efficient as the centralized scheme. It also outperforms the power-sensitive AODV (PS-AODV), an efficient but non-learning routing protocol. Our formal model of Bayesian learning integrates a real data-setwhich forces the model to conform to the real data. This technique seems useful beyond the case study of this chapter.