Abstract

Wireless Sensor Networks (WSNs) are ad-hoc wireless networks of typically hundreds or even thousands of small low-cost sensor nodes, that communicate in a wireless way. A sensor node is a small autonomous unit, often running on batteries, with hardware to sense environmental characteristics, a processor and a radio transceiver. All nodes send their sensor data to a central gateway node for future analysis.

Existing network protocols are not suitable for the WSN setting, since they often require a lot of information exchange and bookkeeping. Therefore, dedicated WSN protocols are required and their correctness and robustness is essential. However, only few techniques are available to support the design of these protocols. One possibility is to mathemat- ically prove that the design is correct, but this usually requires many assumptions and simplifications. Another possibility is simulation and testing, but this may not uncover all undesirable aspects of a protocol. We therefore formulated the following main re- search question: Is formal verification (and more specifically: Model Checking) suitable for supporting the design of WSN protocols?.

In order to find an answer to this question, we took a concept design of a WSN protocol (developed at the University of Twente). It is a routing protocol that attempts to build a Shortest Path Tree (SPT) in a distributed fashion. We first made this protocol explicit by specifying both an informal and formal description. Then we constructed models of it for the state-of-the-art model checkers UPPAAL, SPIN, and PRISM. The main correctness properties that we checked for these models were deadlock freedom, correct parent selection and correct distance computation. Furthermore, we performed verification experiments with variants of the protocol.

The main results of this research project are an informal and formal specification of the given protocol, models for the different tools, together with correctness properties, a fea- sibility limit of 4 nodes, the idea of formal experiments and valuable insights in modelling and verification of this protocol and of WSN protocols in general. No errors were found in the protocol.

The answer to our research question has two sides: based on our research, the limitations found and on the current state of the art, the answer is negative. On the other hand, experimentation using formal verification turned out to be a powerful tool to support WSN protocol design. Further research is required to find suitable abstraction techniques to exploit the quantitative character of the verification.

Additional Resources

1. The paper