Systematic and automatic verification of sensor networks

Abstract

We investigate how software verification techniques could be adopted to systematically model check SNs implemented in NesC/TinyOS, which is one of the most widely used platforms for developing SNs. Firstly, we translate a NesC program to a semantically equivalent specification in Stateful Timed CSP (STCSP), and hence model checkers for STCSP like PAT can be used to formally verify the NesC program. Then, we develop the direct verification approach so that the capability of revealing errors/bugs could be maximized. The complete semantics of SNs is defined as a set of 66 firing rules. Model checking algorithms are developed to verify SNs against safety properties and liveness properties. We also propose a novel two-level partial order reduction (POR) approach for SNs, which reduces unnecessary interleaving among sensors and among interrupts and tasks within each individual sensor. The POR approach is proved to be sound and complete, preserving LTL-X properties.