Abstract
We describe an approach to the analysis of protocols for wireless sensor networks in scenarios with mobile nodes and dynamic link quality. The approach is based on the theorem proving system PVS and can be used for formal specification, automated simulation and verification of the behaviour of the protocol. In order to demonstrate the applicability of the approach, we analyse the reverse path forwarding algorithm, which is the basic technique used for diffusion protocols for wireless sensor networks.
This work was partially supported by the European Commission through the Network of Excellence ReSIST (IST-026764).
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
Akyldiz, I., Su, W., Sankarasubramaniam, Y., Cayirci, E.: Wireless Sensor Networks: a Survey. Computer Networks 38, 393–422 (2002)
Varga, A.: The Omnet++ Discrete Event Simulation System. In: Proceedings of the European Simulation Multiconference (ESM 2001) (June 2001)
Buck, J., Ha, S., Lee, E.A., Messerschmitt, D.G.: Ptolemy: a Framework for Simulating and Prototyping Heterogeneous Systems. In: Readings in hardware/software co-design, pp. 527–543. Kluwer Academic Publishers, Dordrecht (2002)
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)
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)
Bhargavan, K., Gunter, C., Lee, I., Sokolsky, O., Kim, M., Obradovic, D., Viswanathan, M.: Verisim: Formal Analysis of Network Simulations. IEEE Trans. Software Engineering 28(2), 129–145 (2002)
Bernardeschi, C., Masci, P., Pfeifer, H.: Early Prototyping of Wireless Sensor Network Algorithms in PVS. In: Harrison, M.D., Sujan, M.-A. (eds.) SAFECOMP 2008. LNCS, vol. 5219, pp. 346–359. Springer, Heidelberg (2008)
Owre, S., Rushby, J., Shankar, N., Henke, F.v.: Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Trans. on Software Engineering 21(2), 107–125 (1995)
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)
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)
Butler, R., Sjogren, J.: A pvs graph theory library. Nasa Technical Memorandum 1998-206923, NASA Langley Research Center, Hampton, Virginia (1998)
Dalal, Y., Metcalfe, R.: Reverse Path Forwarding of Broadcast Packets. Communications of ACM 21(12), 1040–1048 (1978)
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)
Texas Instruments: Chipcon CC2420 Datasheet (2007), http://focus.ti.com/lit/ds/symlink/cc2420.pdf
Clausen, T., Larsen, N., Olesen, T., Viennot, L.: Investigating Data Broadcast Performance in Mobile ad hoc Networks. In: The 5th International Symposium on Wireless Personal Multimedia Communications, WPMC (2002)
Ö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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bernardeschi, C., Masci, P., Pfeifer, H. (2009). Analysis of Wireless Sensor Network Protocols in Dynamic Scenarios. In: Guerraoui, R., Petit, F. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2009. Lecture Notes in Computer Science, vol 5873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05118-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-05118-0_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05117-3
Online ISBN: 978-3-642-05118-0
eBook Packages: Computer ScienceComputer Science (R0)