Compositional Verification of Sensor Software Using Uppall

Verification of wireless sensor networks has long been performed for communication protocols and for network-level behavior over multiple nodes, but not for the basic properties that should hold at a single node. Testing sensor networks, however, is extremely hard due to the lack of controllability, and complex simulation setups are often too expensive to undertake. Thus, verification of properties for a sensor node is desirable. We created a verification methodology that extracts timed models of the high-level behavior of a wireless sensor and then uses UPPAAL to verify both functional and non-functional (timed) properties for the sensor. This verification capability will enhance the trustworthiness of deployed sensor networks.