%0 Conference Paper %1 CBMC10 %A Werner, Frank %A Faragó, David %B Formal Methods for Industrial Critical Systems - 15th International Workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010. Proceedings %D 2010 %I Springer %K VST4WSN bmc myown wsn %P 115--131 %T Correctness of Sensor Network Applications by Software Bounded Model Checking %X 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 deploy- ment 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 prop- erties. We made the verification process scalable in the size of the code by abstraction (eg, from hardware) and by simplification heuristics. The latter also achieved scalability in data type complexity for the proper- ties that were verifiable. The others require technical advancements for complex data types within CBMC’s core.

@inproceedings{CBMC10, abstract = {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 deploy- ment 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 prop- erties. We made the verification process scalable in the size of the code by abstraction (eg, from hardware) and by simplification heuristics. The latter also achieved scalability in data type complexity for the proper- ties that were verifiable. The others require technical advancements for complex data types within CBMC’s core. }, added-at = {2010-08-27T15:20:16.000+0200}, author = {Werner, Frank and Farag{\'o}, David}, biburl = {https://www.bibsonomy.org/bibtex/295f7eb755c022430eb2c09a9720ccf9d/davef}, booktitle = {Formal Methods for Industrial Critical Systems - 15th International Workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010. Proceedings}, interhash = {f6db6aab927bdb682b7da71aae115a1e}, intrahash = {95f7eb755c022430eb2c09a9720ccf9d}, keywords = {VST4WSN bmc myown wsn}, pages = {115--131}, publisher = {Springer}, series = {LNCS}, timestamp = {2014-06-07T19:14:30.000+0200}, title = {Correctness of Sensor Network Applications by Software Bounded Model Checking}, year = 2010 }