On Software Verification for Sensor Nodes
The authors 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 being able to automatically extract standard C models out of the particular flavors of embedded C used in sensor programming solutions, and decreasing the resulting program's state space to a degree that allows practical verification times. They contribute a platform-dependent, OS-independent software verification tool for OS-wide programs written in MSP430 embedded C with asynchronous hardware interrupts.