Abstract
It is well-known that the performance of wireless protocols depends on the quality of the wireless links, which in turn is affected by the network topology. The aim of this paper is to investigate the use of probabilistic model checking in the analysis of performance of wireless protocols, using a probabilistic abstraction of wireless unreliability.
Our main contributions are first, to show how to formalise wireless link unreliability via probabilistic behaviour derived from the current best analytic models [12], and second, to show how such formal models can be generated automatically from a graphical representation of the network, and analysed with the PRISM model checker.
We also introduce CaVi, a graphical specification tool, which reduces the specification task to the design of the network layout, and provides a uniform design interface linking model checking with simulation. We illustrate our techniques with a randomised gossiping protocol.
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
Boulis, A.: Castalia: A simulator for wireless sensor networks, http://castalia.npc.nicta.com.au
Aziz, A., Singhal, V., Balarinand, F., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 155–165. Springer, Heidelberg (1995)
Cavin, D., Sasson, Y., Schiper, A.: On the accuracy of manet simulators. In: Proceedings of the second ACM international workshop on Principles of mobile computing, pp. 38–43. ACM Press, New York (2002)
Fehnker, A., Fruth, M., McIver, A.K.: Cavi: A graphical specification tool for wireless network protocols. In: The Proceedings of Quantitative Evaluation of Systems, 2008 (to appear) (2008)
Fehnker, A., Gao, P.: Formal verification and simulation for performance analysis for probabilistic broadcast protocols. In: Kunz, T., Ravi, S.S. (eds.) ADHOC-NOW 2006. LNCS, vol. 4104, pp. 128–141. Springer, Heidelberg (2006)
Fehnker, A., McIver, A.: Formal analysis of wireless protocols. In: Proc. 2nd International Symposium in Leveraging applications in formal methods, verification and validation, pp. 263–270. IEEE Computer society digital library, Los Alamitos (2007)
Kotz, K., Newport, C., Gray, R.S., Liu, J., Yuan, Y., Elliott, C.: Experimental evaluation of wireless simulation assumptions. In: Proceedings of the 7th ACM international symposium on Modeling, analysis and simulation of wireless and mobile systems, pp. 78–82. ACM Press, New York (2004)
The network simulator ns 2, http://www.isi.edu/nsnam/ns/
OPNET, http://www.opnet.com/
PRISM. Probabilistic symbolic model checker, http://www.prismmodelchecker.org/
Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. Statistical probabilistic model checking: An empirical study. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 46–60. Springer, Heidelberg (2004)
Zuniga, M., Krishnamachari, B.: Analyzing the transitional region in low power wireless links. In: First IEEE International Conference on Sensor and Ad hoc Communications and Networks (SECON), pp. 517–526. IEEE, Los Alamitos (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Fehnker, A., Fruth, M., McIver, A.K. (2009). Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds) Methods, Models and Tools for Fault Tolerance. Lecture Notes in Computer Science, vol 5454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00867-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-00867-2_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00866-5
Online ISBN: 978-3-642-00867-2
eBook Packages: Computer ScienceComputer Science (R0)