Abstract
Wireless sensor networks (WSNs) are expected to run unattendedly for critical tasks. To guarantee the correctness of WSNs is important, but highly nontrivial due to the distributed nature. In this work, we present an automatic approach to directly verify WSNs built with TinyOS applications implemented in the NesC language. To achieve this target, we firstly define a set of formal operational semantics for most of the NesC language structures for the first time. This allows us to capture the behaviors of sensors by labelled transition systems (LTSs), which are the underlying semantic models of NesC programs. Secondly, WSNs are modeled as the composition of sensors with a network topology. Verifications of individual sensors and the whole WSN become possible by exploring the corresponding LTSs using model checking. With substantial engineering efforts, we implemented this approach in the tool NesC@PAT to support verifications of deadlock-freeness, state reachability and temporal properties for WSNs. NesC@PAT has been applied to analyze and verify WSNs, with unknown bugs being detected. To the best of our knowledge, NesC@PAT is the first model checker which takes NesC language as the modeling language and completely preserves the interrupt-driven feature of the TinyOS execution model.
This research is supported in part by Research Grant IDD11100102 of Singapore University of Technology and Design, IDC and MOE2009-T2-1-072 (Advanced Model Checking Systems).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
NesC@PAT, http://www.comp.nus.edu.sg/~pat/NesC/
Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., Cayirci, E.: Wireless sensor networks: a survey. Computer Networks 38, 132–138 (2001)
Archer, W., Levis, P., Regehr, J.: Interface contracts for TinyOS. In: IPSN, pp. 158–165 (2007)
Bucur, D., Kwiatkowska, M.Z.: Software verification for TinyOS. In: IPSN, pp. 400–401 (2010)
Emerson, E.A., Jha, S., Peled, D.: Combining Partial Order and Symmetry Reductions. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 19–34. Springer, Heidelberg (1997)
Gay, D., Levis, P., Culler, D.E.: Software design patterns for TinyOS. ACM Trans. Embedded Comput. Syst. 6(2) (2007)
Gay, D., Levis, P., Behren, R.v., Welsh, M., Brewer, E., Culler, D.: The nesC Language: A Holistic Approach to Networked Embedded Systems. In: PLDI, pp. 1–11 (2003)
Hanna, Y., Rajan, H.: Slede: Framework for automatic verification of sensor network security protocol implementations. In: ICSE Companion, pp. 427–428 (2009)
Hanna, Y., Rajan, H., Zhang, W.: Slede: a domain-specific verification framework for sensor network security protocol implementations. In: WISEC, pp. 109–118 (2008)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Holzmann, G.J.: Design and Validation of Protocols: A Tutorial. Computer Networks and ISDN Systems 25(9), 981–1017 (1993)
Klues, K., Liang, C.-J.M., Paek, J., Musaloiu-Elefteri, R., Levis, P., Terzis, A., Govindan, R.: TOSThreads: thread-safe and non-invasive preemption in TinyOS. In: SenSys, pp. 127–140 (2009)
Kothari, N., Millstein, T.D., Govindan, R.: Deriving State Machines from TinyOS Programs Using Symbolic Execution. In: IPSN, pp. 271–282 (2008)
Levis, P., Gay, D.: TinyOS Programming, 1st edn. Cambridge University Press, Cambridge (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., Madden, S., Polastre, J., Szewczyk, R., Woo, A., Gay, D., Hill, J., Welsh, M., Brewer, E., Culler, D.: TinyOS: An operating system for sensor networks. In: Ambient Intelligence. Springer, Heidelberg (2004)
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, pp. 15–28 (2004)
Li, P., Regehr, J.: T-check: bug finding for sensor networks. In: IPSN, pp. 174–185 (2010)
Liu, Y., Sun, J., Dong, J.S.: An Analyzer for Extended Compositional Process Algebras. In: ICSE Companion, pp. 919–920. ACM, New York (2008)
Liu, Y., Sun, J., Dong, J.S.: Developing Model Checkers Using PAT. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 371–377. Springer, Heidelberg (2010)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems:Specification. Springer, Heidelberg (1992)
Menrad, V., Garcia, M., Schupp, S.: Improving TinyOS Developer Productivity with State Charts. In: SOMSED (2009)
Nguyen, N.T.M., Soffa, M.L.: Program representations for testing wireless sensor network applications. In: DOSTA, pp. 20–26 (2007)
Peled, D.: Combining Partial Order Reductions with On-the-fly Model-Checking. Formal Methods in System Design 8(1), 39–64 (1996)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)
Sun, J., Liu, Y., Dong, J.S., Zhang, X.: Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 581–600. Springer, Heidelberg (2009)
Sun, J., Liu, Y., Roychoudhury, A., Liu, S., Dong, J.S.: Fair model checking with process counter abstraction. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 123–139. Springer, Heidelberg (2009)
Sun, J., Song, S., Liu, Y.: Model Checking Hierarchical Probabilistic Systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 388–403. Springer, Heidelberg (2010)
Zhang, S.J., Sun, J., Pang, J., Liu, Y., Dong, J.S.: On Combining State Space Reductions with Global Fairness Assumptions. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 432–447. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zheng, M., Sun, J., Liu, Y., Dong, J.S., Gu, Y. (2011). Towards a Model Checker for NesC and Wireless Sensor Networks. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-24559-6_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24558-9
Online ISBN: 978-3-642-24559-6
eBook Packages: Computer ScienceComputer Science (R0)