Verification of The Minimum Cost Forwarding Protocol for Wireless Sensor Networks

Wireless sensor networks (WSN) consist of small self-contained devices with computational, sensing and wireless communication capabilities. They allow flexible, powerful, tetherless, automated data collection and monitoring systems to be created. Anticipated applications include environmental hazard monitoring, forest fire detection, machine instrumentation, etc. Many routing protocols have been proposed to facilitate data transport from sensor nodes to a base station; few of these protocols have been formally verified or operationally deployed however. The minimum cost forwarding (MCF) routing protocol (Ye et al., 2001), has been proposed. The application of MCF is restricted to networks possessing a single sink node and multiple source nodes. However, it offers several potential advantages for sensor nodes with limited resources. The MCF protocol is the subject of the current study with a view to its implementation in a prototype sensor network. The first phase of the work, and the subject of this paper, is the formal evaluation of the MCF protocol to increase confidence its correctness and study its ability to handle node failure and other errors. As a result of formal verification using a model checking tool, UPPAAL, we confirm the soundness of the protocol during its initialisation and operational phases and have identified significant weaknesses in the published protocol concerning equal-cost minimum cost paths and node failure. In particular, we identify a flaw in the previously suggested periodic initialisation broadcast to re-establish a minimum cost field. Here we present these results and offer improvements to overcome some deficiencies. It is expected that model checking may usefully be applied in the study of other WSN protocols.