Abstract
Wireless sensor networks may be used to conduct critical tasks like fire detection or surveillance monitoring. It is thus important to guarantee the correctness of such systems by systematically analyzing their behaviors. Formal verification of wireless sensor networks is an extremely challenging task as the state space of sensor networks is huge, e.g., due to interleaving of sensors and intra-sensor interrupts. In this work, we develop a method to reduce the state space significantly so that state space exploration methods can be applied to a much smaller state space without missing a counterexample. Our method explores the nature of networked NesC programs and uses a novel two-level partial order reduction approach to reduce interleaving among sensors and intra-sensor interrupts. We define systematic rules for identifying dependence at sensor and network levels so that partial order reduction can be applied effectively. We have proved the soundness of the proposed reduction technique, and present experimental results to demonstrate the effectiveness of our approach.
This research is partially supported by project IDG31100105/IDD11100102 from Singapore University of Technology and Design.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Experiment Materials, http://www.comp.nus.edu.sg/~pat/NesC/por
Akyildiz, I., Su, W., Sankarasubramaniam, Y., Cayirci, E.: Wireless Sensor Networks: a Survey. Computer Networks 38(4), 393–422 (2002)
Archer, W., Levis, P., Regehr, J.: Interface contracts for TinyOS. In: IPSN, Massachusetts, USA, pp. 158–165 (2007)
Bucur, D., Kwiatkowska, M.: Bug-Free Sensors: The Automatic Verification of Context-Aware TinyOS Applications. In: Tscheligi, M., de Ruyter, B., Markopoulus, P., Wichert, R., Mirlacher, T., Meschterjakov, A., Reitberger, W. (eds.) AmI 2009. LNCS, vol. 5859, pp. 101–105. Springer, Heidelberg (2009)
Bucur, D., Kwiatkowska, M.Z.: On software verification for sensor nodes. Journal of Systems and Software 84(10), 1693–1707 (2011)
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)
Culler, D.E., Hill, J., Buonadonna, P., Szewczyk, R., Woo, A.: A Network-Centric Approach to Embedded Software for Tiny Devices. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 114–130. Springer, Heidelberg (2001)
Dunkels, A., Grönvall, B., Voigt, T.: Contiki - A Lightweight and Flexible Operating System for Tiny Networked Sensors. In: LCN, pp. 455–462 (2004)
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110–121. ACM (2005)
Gay, D., Levis, P., von Behren, R., Welsh, M., Brewer, E., Culler, D.: The nesC Language: A Holistic Approach to Networked Embedded Systems. In: PLDI, pp. 1–11 (2003)
Godefroid, P., Wolper, P.: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Formal Methods in System Design 2(2), 149–164 (1993)
Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian Partial-Order Reduction. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 95–112. Springer, Heidelberg (2007)
Hanna, Y., Rajan, H., Zhang, W.: SLEDE: a domain-specific verification framework for sensor network security protocol implementations. In: WISEC, pp. 109–118 (2008)
Levis, P., Gay, D.: TinyOS Programming, 1st edn. Cambridge University Press (2009)
Levis, P., Lee, N., Welsh, M., Culler, D.E.: TOSSIM: Accurate and Scalable Simulation of Entire TinyOS Applications. In: SenSys, pp. 126–137 (2003)
Levis, P., Patel, N., Culler, D.E., Shenker, S.: Trickle: A Self-Regulating Algorithm for Code Propagation and Maintenance in Wireless Sensor Networks. In: NSDI, California, USA, pp. 15–28 (2004)
Li, P., Regehr, J.: T-Check: bug finding for sensor networks. In: IPSN, Stockholm, Sweden, pp. 174–185 (2010)
Luttik, B., Trčka, N.: Stuttering Congruence for Chi. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 185–199. Springer, Heidelberg (2005)
McInnes, A.I.: Using CSP to Model and Analyze TinyOS Applications. In: ECBS, California, USA, pp. 79–88 (2009)
Mottola, L., Voigt, T., Osterlind, F., Eriksson, J., Baresi, L., Ghezzi, C.: Anquiro: Enabling Efficient Static Verification of Sensor Network Software. In: SESENA, pp. 32–37 (2010)
Robby, Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: ESEC/SIGSOFT FSE, pp. 267–276 (2003)
Robby, Dwyer, M.B., Hatcliff, J.: Bogor: A Flexible Framework for Creating Software Model Checkers. In: TAIC PART, pp. 3–22 (2006)
Werner, F., Faragó, D.: Correctness of Sensor Network Applications by Software Bounded Model Checking. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 115–131. Springer, Heidelberg (2010)
Yang, Y., Chen, X., Gopalakrishnan, G.C., Kirby, R.M.: Efficient Stateful Dynamic Partial Order Reduction. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 288–305. Springer, Heidelberg (2008)
Zheng, M., Sun, J., Liu, Y., Dong, J.S., Gu, Y.: Towards a Model Checker for NesC and Wireless Sensor Networks. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 372–387. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zheng, M., Sanán, D., Sun, J., Liu, Y., Dong, J.S., Gu, Y. (2013). State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2013. Lecture Notes in Computer Science, vol 7737. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35873-9_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-35873-9_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35872-2
Online ISBN: 978-3-642-35873-9
eBook Packages: Computer ScienceComputer Science (R0)