Software verification for TinyOS
Doina Bucur, Marta Kwiatkowska · 2010
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, nullpointer dereferences), we verify application-specific assertions, including low-level assertions upon the state of the registers and peripherals.