Oxford logo
[BK10a] D. Bucur and M. Kwiatkowska. Software Verification for TinyOS. In Proc. Information Processing in Sensor Networks (IPSN'10), pages 400-401, ACM. April 2010. [pdf] [bib]
Downloads:  pdf pdf (168 KB)  bib bib
Notes: An extended version of this paper is available here.

Accompanying software can be found here:
Abstract. We describe the first software tool for the verification of TinyOS 2, MSP430 applications at compile-time. Given assertions upon the state of the sensor node, the tool boundedly explores all program executions and returns to the programmer an error trace leading to any assertion violation. Besides memory-related errors (out-of-bounds arrays, null- pointer dereferences), we verify application-specific assertions, including low-level assertions upon the state of the registers and peripherals.