skip to main content
10.1145/1809111.1809122acmconferencesArticle/Chapter ViewAbstractPublication PagesicseConference Proceedingsconference-collections
research-article

Anquiro: enabling efficient static verification of sensor network software

Published:03 May 2010Publication History

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.

References

  1. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  2. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  3. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  4. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  5. 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 ScholarGoogle ScholarCross RefCross Ref
  6. DJProf. Java Memory Profiler. www.mcs.vuw.ac.nz/djp/djprof/.Google ScholarGoogle Scholar
  7. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  8. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  9. G. J. Holzmann. The model checker spin. IEEE Trans. Softw. Eng., 23(5), 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  11. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  12. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  13. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  14. 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 ScholarGoogle ScholarCross RefCross Ref
  15. 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 ScholarGoogle Scholar
  16. NESL. Lighthouse Project. projects.nesl.ucla.edu/public/lighthouse/.Google ScholarGoogle Scholar
  17. 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 ScholarGoogle ScholarCross RefCross Ref
  18. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  19. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  20. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  21. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  22. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  23. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  24. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  25. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  26. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  27. 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 ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Anquiro: enabling efficient static verification of sensor network software

      Recommendations

      Comments

      Login options

      Check if you have access through your login credentials or your institution to get full access on this article.

      Sign in
      • Published in

        cover image ACM Conferences
        SESENA '10: Proceedings of the 2010 ICSE Workshop on Software Engineering for Sensor Network Applications
        May 2010
        91 pages
        ISBN:9781605589695
        DOI:10.1145/1809111
        • Conference Chairs:
        • Kurt Geihs,
        • Stefan Gruner,
        • Kay Römer

        Copyright © 2010 ACM

        Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        • Published: 3 May 2010

        Permissions

        Request permissions about this article.

        Request Permissions

        Check for updates

        Qualifiers

        • research-article

        Upcoming Conference

        ICSE 2024

      PDF Format

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader