Sciweavers

Share
FMICS
2010
Springer

Correctness of Sensor Network Applications by Software Bounded Model Checking

11 years 5 months ago
Correctness of Sensor Network Applications by Software Bounded Model Checking
We investigate the application of the software bounded model checking tool CBMC to the domain of wireless sensor networks (WSNs). We automatically generate a software behavior model from a network protocol (ESAWN) implementation in a WSN development and deployment platform (TinyOS), which is used to rigorously verify the protocol. Our work is a proof of concept that automatic verification of programs of practical size ( 21 000 LoC) and complexity is possible with CBMC and can be integrated into TinyOS. The developer can automatically check for pointer dereference and array index out of bound errors. She can also check additional, e.g., functional, properties that she provides by assume- and assert-statements. This experience paper shows that our approach is in general feasible since we managed to verify about half of the properties. We made the verification process scalable in the the code by abstraction (eg, from hardware) and by simplification heuristics. The latter also achieved sca...
Frank Werner, David Faragó
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where FMICS
Authors Frank Werner, David Faragó
Comments (0)
books