Oxford logo
[BK10b] D. Bucur and M. Kwiatkowska. On Software Verification for Sensor Nodes. Technical report RR-10-25, Oxford University Computing Laboratory. November 2010. [pdf] [bib]
Downloads:  pdf pdf (424 KB)  bib bib
Notes: Accompanying software can be found here:
Abstract. We consider software written for networked, wireless sensor nodes, and specialize software verification techniques for standard C programs in order to locate programming errors in sensor applications before the software’s deployment on motes. Ensuring the reliability of sensor applications is challenging: low-level, interrupt-driven code runs without memory protection in dynamic environments. The difficulties lie with (i) being able to automatically extract standard C models out of the particular flavours of embedded C used in sensor programming solutions, and (ii) decreasing the resulting program’s state space to a degree that allows practical verification times.

We contribute a platform-dependent, OS-independent software verification tool for OS-wide programs written in MSP430 em- bedded C with asynchronous hardware interrupts. Our tool automatically translates the program into standard C by modelling the MCU’s memory map and direct memory access. To emulate the existence of hardware interrupts, calls to hardware interrupt han- dlers are added, and their occurrence is minimized with a partial-order reduction technique, in order to decrease the program’s state space, while preserving program semantics. Safety specifications are written as C assertions embedded in the code. The resulting sequential program is then passed to CBMC, a bounded software verifier for sequential ANSI C. Besides standard errors (e.g., out-of-bounds arrays, null-pointer dereferences), this tool chain is able to verify application-specific assertions, including low-level assertions upon the state of the registers and peripherals.

Verification for wireless sensor network applications is an emerging field of research; thus, as a final note, we survey current research on the topic.

QAV:

Home

People

Projects

Publications