Compositional Verification of Sensor Software Using Uppaal


Verification of wireless sensor networks has long been performed for communication protocols and for networklevel 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 nonfunctional (timed) properties for the sensor. This verification capability will enhance the trustworthiness of deployed sensor networks. Keywords-verification, wireless sensor networks, compositional analysis


    12 Figures and Tables

    Download Full PDF Version (Non-Commercial Use)