ABSTRACT
We present Anquiro, a domain-specific model checker for statically verifying the correctness of sensor network software. In this context, static verification has hitherto received little attention, as state space explosion problems may prevent applying these techniques. Anquiro overcomes this limitation by providing different abstraction levels depending on the functionality to verify, and by implementing domain-specific state abstractions within the checking engine. We demonstrate the use of Anquiro in verifying the correctness of a widely used data dissemination protocol. This study allows us to identify issues that the protocol may overlook. Moreover, our evaluation of Anquiro's performance shows that it drastically reduces the number of states generated during the verification, preventing state space explosion problems.
- L. Baresi, G. Gerosa, C. Ghezzi, and L. Mottola. Playing with time in publish-subscribe using a domain-specific model checker. In Proc. of the SAVCBS Workshop, 2007. Google ScholarDigital Library
- L. Baresi, C. Ghezzi, and L. Mottola. On accurate automatic verification of publish-subscribe architectures. In Proc. of the 29th Int. Conf. on Software Engineering (ICSE), 2007. Google ScholarDigital Library
- D. Bucur and M. Kwiatkowska. Bug-free sensors: The automatic verification of context-aware TinyOS applications. In Proc. of the European Conference on Ambient Intelligence (AmI), 2009. Google ScholarDigital Library
- W. Cao, T. Abdelzaher, J. Stankovic, K. Whitehouse, and L. Luo. Declarative tracepoints: a programmable and application independent debugging system for wireless sensor networks. In Proc. of the Int. Conf. on Embedded Network Sensor Systems (SENSYS), 2008. Google ScholarDigital Library
- E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), 2004.Google ScholarCross Ref
- DJProf. Java Memory Profiler. www.mcs.vuw.ac.nz/djp/djprof/.Google Scholar
- A. Dunkels, B. Grönvall, and T. Voigt. Contiki - a Lightweight and Flexible Operating System for Tiny Networked Sensors. In Proc. of the Workshop on Embedded Networked Sensors (EmNetS), 2004.Google ScholarDigital Library
- Y. Hanna, H. Rajan, and W. Zhang. Slede: A domain-specific verification framework for sensor network security protocol implementations. In Proceedings of the ACM Conf. on Wireless network security, 2008. Google ScholarDigital Library
- G. J. Holzmann. The model checker spin. IEEE Trans. Softw. Eng., 23(5), 1997. Google ScholarDigital Library
- K. Langendoen, A. Baggio, and O. Visser. Murphy loves potatoes: experiences from a pilot sensor network deployment in precision agriculture. In Proceedings of the 20th Int. Parallel and Distributed Processing Symposium (IPDPS 2006), 2006. Google ScholarDigital Library
- P. Levis, N. Lee, M. Welsh, and D. Culler. Tossim: accurate and scalable simulation of entire tinyos applications. In Proc. of the Conf. on Embedded Networked Sensor Systems (SENSYS), 2003. Google ScholarDigital Library
- P. Levis, N. Patel, D. Culler, and S. Shenker. Trickle: A self-regulating algorithm for code propagation and maintenance in wireless sensor networks. In Proc. of NSDI, Mar. 2004. Google ScholarDigital Library
- K. Liu, M. Li, Y. Liu, M. Li, Z. Guo, and F. Hong. Passive diagnosis for wireless sensor networks. In Proc. of the Conf. on Embedded Network Ssensor Systems (SENSYS), 2008. Google ScholarDigital Library
- L. Luo, T. He, G. Zhou, L. Gu, T. F. Abdelzaher, and J. A. Stankovic. Achieving repeatability of asynchronous events in wireless sensor networks with EnviroLog. In Proc. of INFOCOM, 2006.Google ScholarCross Ref
- P. Merino and J. M. Troya. Modelling and verification of the ITU-T multipoint communication service with SPIN. In Proc. of the 2nd Int. Wrkshp. on SPIN Verification, 1996.Google Scholar
- NESL. Lighthouse Project. projects.nesl.ucla.edu/public/lighthouse/.Google Scholar
- F. Österlind, A. Dunkels, J. Eriksson, N. Finne, and T. Voigt. Cross-level sensor network simulation with COOJA. In Proc. of the Workshop on Practical Issues in Building Sensor Network Applications (SenseApp), 2006.Google ScholarCross Ref
- N. Ramanathan, K. Chang, R. Kapur, L. Girod, E. Kohler, and D. Estrin. Sympathy for the sensor network debugger. In Proc. of the Conf. on Embedded Networked Sensor Systems (SENSYS), 2005. Google ScholarDigital Library
- Robby, M.-B. Dwyer, and J. Hatcliff. Bogor: an extensible and highly-modular software model checking framework. In Proc. of the 9th European Software Engineering Conf., 2003. Google ScholarDigital Library
- K. Römer and J. Ma. PDA: passive distributed assertions for sensor networks. In Proc. of the Conf. on Information Processing in Sensor Networks (IPSN), 2009. Google ScholarDigital Library
- T. Sookoor, T. Hnat, P. Hooimeijer, W. Weimer, and K. Whitehouse. Macrodebugging: global views of distributed program execution. In Proc. of the Conf. on Embedded Networked Sensor Systems (SENSYS), 2009. Google ScholarDigital Library
- F. Stann, J. Heidemann, R. Shroff, and M. Z. Murtaza. RBP: robust broadcast propagation in wireless networks. In Proc. of the Conf. on Embedded Networked Sensor Systems (SENSYS), 2006. Google ScholarDigital Library
- B. Titzer, D. Lee, and J. Palsberg. Avrora: scalable sensor network simulation with precise timing. In Proc. of Conf. on Information Processing in Sensor Networks (IPSN), 2005. Google ScholarDigital Library
- S. Tschirner, L. Xuedong, and W. Yi. Model-based validation of QoS properties of biomedical sensor networks. In Proc. of the 8th ACM Int. Conf. on Embedded Software (EMSOFT), 2008. Google ScholarDigital Library
- K. Whitehouse, G. Tolle, J. Taneja, C. Sharp, S. Kim, J. Jeong, J. Hui, P. Dutta, and D. Culler. Marionette: using RPC for interactive development and debugging of wireless embedded networks. In Proc. of Conf. on Information Processing in Sensor Networks (IPSN), 2006. Google ScholarDigital Library
- M. Woehrle, C. Plessl, J. Beutel, and L. Thiele. Increasing the reliability of wireless sensor networks with a distributed testing framework. In Proc. of the Workshop on Embedded Networked Sensors, 2007. Google ScholarDigital Library
- J. Yang, M. Soffa, L. Selavo, and K. Whitehouse. Clairvoyant: a comprehensive source-level debugger for wireless sensor networks. Proc. of the Conf. on Embedded Networked Sensor Systems (SENSYS), 2007. Google ScholarDigital Library
Index Terms
Anquiro: enabling efficient static verification of sensor network software
Recommendations
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The ...
Faster and More Complete Extended Static Checking for the Java Modeling Language
Extended Static Checking (ESC) is a fully automated formal verification technique. Verification in ESC is achieved by translating programs and their specifications into verification conditions (VCs). Proof of a VC establishes the correctness of the ...
Sound Gradual Verification with Symbolic Execution
Gradual verification, which supports explicitly partial specifications and verifies them with a combination of static and dynamic checks, makes verification more incremental and provides earlier feedback to developers. While an abstract, weakest ...
Comments