Skip to main content
SpringerLink
Log in

Specifying and Verifying Sensor Networks: An Experiment of Formal Methods

  • Conference paper
Book cover Formal Methods and Software Engineering (ICFEM 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5256))

Included in the following conference series:

Abstract

With the development of sensor technology and electronic miniaturization, wireless sensor networks have shown a wide range of promising applications as well as challenges. Early stage sensor network analysis is critical, which allows us to reveal design errors before sensor deployment. Due to their distinguishable features, system specification and verification of sensor networks are highly non-trivial tasks. On the other hand, numerous formal theories and analysis tools have been developed in formal methods community, which may offer a systematic method for formal analysis of sensor networks. This paper presents our attempt on applying formal methods to sensor network specification/verification. An integrated notation named Active Sensor Processes is proposed for high-level specification. Next, we experiment formal verification techniques to reveal design flaws in sensor network applications.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., Cayirci, E.: Wireless Sensor Networks: a Survey. Computer Networks 38(4), 393–422 (2002)

    Article  Google Scholar 

  2. Bose, P., Morin, P., Stojmenovic, I., Urrutia, J.: Routing with Guaranteed Delivery in Ad Hoc Wireless Networks. Wireless Networks 7(6), 609–616 (2001)

    Article  MATH  Google Scholar 

  3. Botts, M.: Sensor Model Language (SensorML) (2006), http://vast.nsstc.uah.edu/SensorML/

  4. Boulis, A., Han, C.C., Srivastava, M.B.: Design and Implementation of a Framework for Efficient and Programmable Sensor Networks. In: Proceedings of International Conference on Mobile Systems, Applictions, and Services (MobiSys 2003) (2003)

    Google Scholar 

  5. Cardelli, L., Gordon, A.D.: Mobile Ambients. Theoretical Computer Science 240(1), 177–213 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  6. Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  7. Chen, C., Dong, J.S., Sun, J.: A verification system for timed interval calculus. In: Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), pp. 271–280. ACM Press, New York (2008)

    Google Scholar 

  8. Ciancio, A.G., Pattem, S., Ortega, A., Krishnamachari, B.: Energy-efficient Data Representation and Routing for Wireless Sensor Networks based on a Distributed Wavelet Compression Algorithm. In: Proceedings of Information Processing in Sensor Networks (IPSN 2006), pp. 309–316 (2006)

    Google Scholar 

  9. Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Dong, J.S., Hao, P., Qin, S.C., Sun, J., Wang, Y.: Timed Patterns: TCOZ to Timed Automata. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 483–498. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Dong, J.S., Hao, P., Sun, J., Zhang, X.: A Reasoning Method for Timed CSP Based on Constraint Solving. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 342–359. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Estrin, D., Govindan, R., Heidemann, J., Kumar, S.: Next Century Challenges: Scalable Coordination in Sensor Networks. In: Proceedings of ACM/IEEE International Conference on Mobile Computing and Networking (MobiCom 1999), pp. 263–270 (1999)

    Google Scholar 

  13. Frey, H., Stojmenovic, I.: On Delivery Guarantees of Face and Combined Greedy-face Routing in Ad Hoc and Sensor Networks. In: Proceedings of the 12th Annual International Conference on Mobile Computing and Networking (MOBICOM 2006), pp. 390–401 (2006)

    Google Scholar 

  14. Gay, D., Levis, P., von Behren, J.R., Welsh, M., Brewer, E.A., Culler, D.E.: The nesC Language: A Holistic Approach to Networked Embedded Systems. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003 (PLDI 2003), pp. 1–11. ACM Press, New York (2003)

    Google Scholar 

  15. Goel, A., Meng, S., Roychoudhury, A., Thiagarajan, P.S.: Interacting process classes. In: Proceedings of the 28th International Conference on Software Engineering (ICSE 2006), pp. 302–311. ACM Press, New York (2006)

    Google Scholar 

  16. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  17. Intanagonwiwat, C., Govindan, R., Estrin, D.: Directed Diffusion: a Scalable and Robust Communication Paradigm for Sensor Networks. In: Proceedings of International Conference on Mobile Computing and Networking (MOBICOM 2000), pp. 56–67 (2000)

    Google Scholar 

  18. Lamport, L.: Real-Time Model Checking Is Really Simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Larsen, K.G., Pettersson, P., Wang, Y.: Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)

    Article  MATH  Google Scholar 

  20. Levis, P., Culler, D.E.: Maté: a Tiny Virtual Machine for Sensor Networks. In: Proceedings of International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2002), pp. 85–95 (2002)

    Google Scholar 

  21. Levis, P., Patel, N., Culler, D.E., Shenker, S.: Trickle: A Self-Regulating Algorithm for Code Propagation and Maintenance in Wireless Sensor Networks. In: Proceedings of Networked Systems Design and Implementation (NSDI 2004), pp. 15–28 (2004)

    Google Scholar 

  22. Madden, S., Franklin, M.J., Hellerstein, J.M., Hong, W.: TinyDB: an Acquisitional Query Processing System for Sensor Networks. ACM Transactions on Database Systems 30(1), 122–173 (2005)

    Article  Google Scholar 

  23. Mahony, B., Dong, J.S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering 26(2) (February 2000)

    Google Scholar 

  24. Mezzetti, N., Sangiorgi, D.: Towards a Calculus For Wireless Systems. Electronic Notes in Theoretical Computer Science 158, 331–353 (2006)

    Article  MATH  Google Scholar 

  25. Prasad, K.V.S.: A Calculus of Broadcasting Systems. In: Abramsky, S. (ed.) TAPSOFT 1991. LNCS, vol. 493, pp. 338–358. Springer, Heidelberg (1991)

    Google Scholar 

  26. Schneider, S.: An Operational Semantics for Timed CSP. Information and Computation 116(2), 193–213 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  27. Schneider, S., Davies, J., Jackson, D.M., Reed, G.M., Reed, J.N., Roscoe, A.W.: Timed CSP: Theory and practice. Real-Time: Theory in Practice 600, 640–675 (1992)

    MathSciNet  Google Scholar 

  28. Sun, J., Dong, J.S.: Design Synthesis from Interaction and State-Based Specifications. IEEE Transactions on Software Engineering 32(6) (2006)

    Google Scholar 

  29. Sun, J., Liu, Y., Dong, J.S., Sun, J.: Bounded Model Checking of Compositional Processes. In: Proceedings of the Second IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 23–30. IEEE Computer Society Press, Los Alamitos (2008)

    Google Scholar 

  30. Thomsen, B.: Calculi for Higher Order Communicating Systems. PhD thesis (1990)

    Google Scholar 

  31. Tschirner, S., Xuedong, L., Yi, W.: Model-Based Validation of QoS Properties of Biomedical Sensor Networks. In: Proceedings of the International Conference on Embedded Software (EMSOFT 2008) (accepted, 2008)

    Google Scholar 

  32. von Eicken, T., Culler, D.E., Goldstein, S.C., Schauser, K.E.: Active Messages: A Mechanism for Integrated Communication and Computation. In: Proceedings of International Symposium on Computer Architecture 1992 (ISCA 1992), pp. 256–266 (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing, National University of Singapore, Singapore

    Jin Song Dong, Jun Sun & Xian Zhang

  2. Department of Computer Science, The University of Auckland, New Zealand

    Jing Sun

  3. Information Systems Architecture Research Division, Grace Center, National Institute of Informatics, Japan

    Kenji Taguchi

Authors
  1. Jin Song Dong
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jing Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jun Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Kenji Taguchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Xian Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Computer and Information Sciences, Hosei University, 3-7-2 Kajino-cho Koganei-shi, 184-8584, Tokoy, Japan

    Shaoying Liu

  2. Department of Computing and Software, McMaster University, 1280 Main St West, L8S 4K1, Hamilton, ON, Canada

    Tom Maibaum

  3. Department of Computer Science and Communication Engineering, , Graduate School of Information Science and Electrical Engineering, Kyushu University, 6-10-1-Hakozaki, 812-8581, Higashi-ku, Fukuoka, Japan

    Keijiro Araki

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dong, J.S., Sun, J., Sun, J., Taguchi, K., Zhang, X. (2008). Specifying and Verifying Sensor Networks: An Experiment of Formal Methods. In: Liu, S., Maibaum, T., Araki, K. (eds) Formal Methods and Software Engineering. ICFEM 2008. Lecture Notes in Computer Science, vol 5256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88194-0_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-88194-0_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-88193-3

  • Online ISBN: 978-3-540-88194-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation