Formal modelling and verification of Wireless Sensor Networks in PVS

Wireless sensor networks (WSNs) are massively distributed systems composed of a large number of communicating nodes. Each node in the network is a tiny battery-powered device, equipped with an embedded microcontroller, a wireless radio transceiver, and various sensing hardware. WSNs are typically used to monitor a physical phenomenon over a large time scale: the physical proximity of sensors to the observed phenomenon and the programmability of nodes enhance the level of accuracy with respect to traditional solutions.

Designing and verifying communication protocols for WSNs is challenging: protocols ought to be efficient, since nodes in the network have small amount of memory and limited energy budget, and robust, since nodes are self-configuring and supposed to run unattended for long periods of time.

In the early stages of design, protocols are usually specified in a semi-formal language, and verification involves simulation and testing of a prototype implementation of the protocol with network simulator. This way to proceed has some weak points: protocols can be under-specified and open to different interpretations, and verification by simulation and testing does not represent a proof of correctness since the whole domain of reachable states is not explored. Also, some effort is usually required to translate the specification into an implementation for the simulator.

We explore the possibility of using the PVS theorem prover to specify, test and verify communication protocols in the very early stages of their design. In particular, we propose a formal model of the WSN that can be used to describe communication protocols, to automatically generate an implementation suitable for simulation and testing, and to verify desired properties. Further work includes the definition of strategies for automatic proof of specific properties.