Early Prototyping of Wireless Sensor Network Algorithms in PVS

  • Cinzia Bernardeschi
  • Paolo Masci
  • Holger Pfeifer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5219)


We describe an approach of using the evaluation mechanism of the specification and verification system PVS to support formal design exploration of WSN algorithms at the early stages of their development. The specification of the algorithm is expressed with an extensible set of programming primitives, and properties of interest are evaluated with ad hoc network simulators automatically generated from the formal specification. In particular, we build on the PVSio package as the core base for the network simulator. According to requirements, properties of interest can be simulated at different levels of abstraction. We illustrate our approach by specifying and simulating a standard routing algorithm for wireless sensor networks.


WSN algorithms simulation PVS 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Xu, N., Rangwala, S., Chintalapudi, K., Ganesan, D., Broad, A., Govindan, R., Estrin, D.: A wireless sensor network for structural monitoring. In: Proc. Intl. Conf. on Embedded Networked Sensor Systems, pp. 13–24. ACM, New York (2004)CrossRefGoogle Scholar
  2. 2.
    Kim, S., Pakzad, S., Culler, D., Demmel, J., Fenves, G., Glaser, S., Turon, M.: Wireless sensor networks for structural health monitoring. In: Proc. Intl. Conf. on Embedded Networked Sensor Systems, pp. 427–428. ACM, New York (2006)CrossRefGoogle Scholar
  3. 3.
    Aboelela, E., Edberg, W., Papakonstantinou, C., Vokkarane, V.: Wireless sensor network based model for secure railway operations. In: Intl. Workshop on eSafety and Convergence of Heterogeneous Wireless Networks, pp. 623–628 (2006)Google Scholar
  4. 4.
    Lorincz, K., Malan, D.J., Fulford-Jones, T.R.F., Nawoj, A., Clavel, A., Shnayder, V., Mainland, G., Welsh, M., Moulton, S.: Sensor networks for emergency response: Challenges and opportunities. IEEE Pervasive Computing 3(4), 16–23 (2004)CrossRefGoogle Scholar
  5. 5.
    Stanford, V.: Using pervasive computing to deliver elder care. IEEE Pervasive Computing 1(1), 10–13 (2002)CrossRefMathSciNetGoogle Scholar
  6. 6.
    Chen, G., Branch, J., Pflug, J., Zhu, L., Szymanski, B.: Sense: A sensor network simulator. Advances in Pervasive Computing and Networking, 249–267 (2004)Google Scholar
  7. 7.
    Pawlikowski, K., Jeong, H., Lee, J.: On credibility of simulation studies of telecommunication networks. IEEE Communications Magazine 40(1), 132–139 (2002)CrossRefGoogle Scholar
  8. 8.
    Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Trans. on Software Engineering 21(2), 107–125 (1995)CrossRefGoogle Scholar
  9. 9.
    Owre, S., Rushby, J., Shankar, N., Stringer-Calvert, D.: PVS: an experience report. In: Applied Formal Methods. LNCS, vol. 1641, pp. 338–345. Springer, Heidelberg (1998)Google Scholar
  10. 10.
    Crow, J., Owre, S., Rushby, J., Shankar, N., Stringer-Calvert, D.: Evaluating, testing, and animating PVS specifications. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (2001)Google Scholar
  11. 11.
    Muñoz, C.: Rapid prototyping in PVS. Technical Report NIA Report No. 2003-03, NASA/CR-2003-212418, National Institute of Aerospace, Hampton, VA (2003)Google Scholar
  12. 12.
    Butler, R., Sjogren, J.: A pvs graph theory library. Nasa technical memorandum 1998-206923, NASA Langley Research Center, Hampton, Virginia (1998)Google Scholar
  13. 13.
    Heinzelman, W., Kulik, J., Balakrishnan, H.: Adaptive protocols for information dissemination in wireless sensor networks. In: Proc. Intl. Conf. on Mobile Computing and Networking, pp. 174–185. ACM, New York (1999)Google Scholar
  14. 14.
    Levis, P., Lee, N., Welsh, M., Culler, D.: TOSSim: accurate and scalable simulation of entire TinyOS applications. In: Proc. Intl. Conf. on Embedded Networked Sensor Systems, pp. 126–137. ACM Press, New York (2003)CrossRefGoogle Scholar
  15. 15.
    Shnayder, V., Hempstead, M., Chen, B., Allen, G., Welsh, M.: Simulating the power consumption of large-scale sensor network applications. In: Proc. Intl. Conf. on Embedded Networked Sensor Systems, pp. 188–200. ACM, New York (2004)CrossRefGoogle Scholar
  16. 16.
    Woo, A., Tong, T., Culler, D.: Taming the underlying challenges of reliable multihop routing in sensor networks. In: SenSys 2003, pp. 14–27. ACM Press, New York (2003)CrossRefGoogle Scholar
  17. 17.
    Bolton, C., Lowe, G.: Analyses of the reverse path forwarding routing algorithm. In: Proc. Intl. Conf. on Dependable Systems and Networks, pp. 485–494. IEEE Computer Society, Los Alamitos (2004)Google Scholar
  18. 18.
    Coleri, S., Ergen, M., Koo, T.J.: Lifetime analysis of a sensor network with hybrid automata modelling. In: Proc. Intl. Workshop on Wireless Sensor Networks and Applications, pp. 98–104. ACM, New York (2002)CrossRefGoogle Scholar
  19. 19.
    Xie, F., Browne, J.C.: Verified systems by composition from verified components. SIGSOFT Softw. Eng. Notes 28(5), 277–286 (2003)CrossRefGoogle Scholar
  20. 20.
    Nair, S., Cardell-Oliver, R.: Formal specification and analysis of performance variation in sensor network diffusion protocols. In: Proc. Symp. on Modeling, Analysis and Simulation of Wireless and Mobile Systems, pp. 170–173. ACM, New York (2004)CrossRefGoogle Scholar
  21. 21.
    Luo, Y., Tsai, J.J.P.: A graphical simulation system for modeling and analysis of sensor networks. In: ISM 2005: Proceedings of the Seventh IEEE International Symposium on Multimedia, pp. 474–482. IEEE Computer Society, Washington (2005)Google Scholar
  22. 22.
    Ölveczky, P., Thorvaldsen, S.: Formal modeling and analysis of the ogdc wireless sensor network algorithm in real-time maude. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 122–140. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Cinzia Bernardeschi
    • 1
  • Paolo Masci
    • 1
  • Holger Pfeifer
    • 2
  1. 1.Department of Information EngineeringUniversity of PisaItaly
  2. 2.Institute of Artificial IntelligenceUlm UniversityGermany

Personalised recommendations