An Automatic Approach to Verify Sensor Network Systems

The programming language nesC for TinyOS applications supports special features of sensor network systems by providing a component-oriented programming model which is flexibly concurrent/reactive and event-driven. Sensor network systems are correctness critical since they are expected to work autonomously. Formal verification techniques such as model checking have been successfully applied to assure the reliability and correctness of concurrent systems and real-time systems. However, manually constructing a formal model is always a non-trivial task. We develop a lightweight framework for sensor network systems which automatically extracts real-time models from nesC implementations and verifies them against goals using model checking techniques. We believe that our approach contributes to systematically improving the quality of sensor network systems, with little overhead or cost caused by applying verification techniques.