Wireless sensor networks (WSNs) employ small power constrained nodes. The communication protocols used to route data in these networks is a decisive factor in determining the efficiency and the life of the networks. The Rumor Routing (RR) protocol is a variant of directed diffusion family of routing protocols used in WSNs which lack location awareness. Formal modeling is used by researchers these days for the comprehensive testing of different communication protocols. The results from formal verification are valid for all possible scenarios facing the model, making this technique better than other testing techniques. Automated verification of properties is done using computer-based tools such as the SPIN model checker. Based on formal modeling, we have developed a formal framework which can automatically verify different wireless routing protocols against multiple factors like security attacks, efficiency, network life, energy conservation etc. Our framework is a combination of formal methods and computer simulations to exhaustively test any given protocol. In this paper, we apply our formal framework to the RR protocol. The RR protocol has been converted to finite state models using model checking tools and then verified by applying LTL properties. The framework has confirmed to us the existence or absence of errors. Traces were generated showing the reason(s) as to why and how if any of these properties had failed. These traces are then simulated using simulators for analysis of the reason(s) of failure. This work to our knowledge is novel and the RR protocol has not been verified earlier for energy efficiency before using this methodology.
展开▼
