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...

• Type: Conference
• Year: 2010
• Where: FMICS
• Authors: Frank Werner, David Faragó
• Keywords: FMICS 2010, Formal Methods, Software Behavior Model, Tool Cbmc, Wireless Sensor Networks