Abstract
The international standard IEEE 802.11 was developed recently in recognition of the increased demand for wireless local area networks. Its medium access control mechanism is described according to a variant of the Carrier Sense Multiple Access with Collision Avoidance (CSMA/CA) scheme. Although collisions cannot always be prevented, randomised exponential backoff rules are used in the retransmission scheme to minimise the likelihood of repeated collisions. More precisely, the backoff procedure involves a uniform probabilistic choice of an integer-valued delay from an interval, where the size of the interval grows exponentially with regard to the number of retransmissions of the current data packet. We model the two-way handshake mechanism of the IEEE 802.11 standard with a fixed network topology using probabilistic timed automata, a formal description mechanism in which both nondeterministic choice and probabilistic choice can be represented. From our probabilistic timed automaton model, we obtain a finite-state Markov decision process via a property-preserving discrete-time semantics. The Markov decision process is then verified using Prism, a probabilistic model checking tool, against probabilistic, timed properties such as “at most 5,000 microseconds pass before a station sends its packet correctly.”
Supported in part by the EPSRC grant GR/N22960, the CNR grant No.99.01716.CTO1, and the EU within the DepAuDE project IST-2001-25434.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994.
R. Alur, A. Itai, R.P. Kurshan, and M. Yannakakis. Timing verification by successive approximation. Information and Computation, 18(1):142–157, 1995.
D. Beyer. Improvements in BDD-based reachability analysis of timed automata. In Proc. FME’01, volume 2021 of LNCS, pages 318–343. Springer, 2001.
G. Bianchi. Performance analysis of the IEEE 802.11 distributed coordination function. IEEE Journal on Selected Areas in Communication, 18:535–547, 2000.
A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. FSTTCS’95, volume 1026 of LNCS, pages 499–513. Springer, 1995.
E.M. Clarke, M. Fujita, P. McGeer, K. McMillan, J. Yang, and X. Zhao. Multi-Terminal Binary Decision Diagrams: An efficient data structure for matrix representation. In Proc. IWLS’93, pages 6a:1–15, 1993. Also available in Formal Methods in System Design, 10(2/3), 1997.
C. Daws and S. Yovine. Two examples of verification of multirate timed automata with Kronos. In Proc. RTSS’95, pages 66–75. IEEE Computer Society Press, 1995.
L. de Alfaro. Computing minimum and maximum reachability times in probabilistic systems. In Proc. CONCUR’99, volume 1664 of LNCS, pages 66–81. Springer, 1999.
C. Derman. Finite-State Markovian Decision Processes. Academic Press, 1970.
H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.
A. Heindl and R. German. Performance modeling of IEEE 802.11 wireless LANs with stochastic Petri nets. Performance Evaluation, 44:139–164, 2001.
T. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to HyTech. In Proc. TACAS’95, volume 1019 of LNCS, pages 41–71. Springer, 1995.
H. Jensen, K. Larsen, and A. Skou. Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction. In Proc. FTRTFT 2000, volume 1926 of LNCS, pages 19–30. Springer, 2000.
J. G. Kemeny, J. L. Snell, and A. W. Knapp. Denumerable Markov Chains. Graduate Texts in Mathematics. Springer, 2nd edition, 1976.
A. Koepsel, J.-P. Ebert, and A. Wolisz. A performance comparison of point and distributed coordination function of an IEEE 802.11 WLAN in the presence of real-time requirements. In Proc. MoMuC 2000, 2000.
M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with Prism: A hybrid approach. In Proc. TACAS 2002, volume 2280 of LNCS, pages 52–66. Springer, 2002.
M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 286, 2002. To appear.
M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Submitted. Extended abstract appears in Proc. Int. Workshop on Application of Formal Methods to IEEE 1394 Standard, 2001.
M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. Technical Report CSR-02-05, School of Computer Science, University of Birmingham, 2002.
K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1+2):134–152, 1997.
Prism web page. http://www.cs.bham.ac.uk/~dxp/prism/.
R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995.
R. Segala and N. A. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250–273, 1995.
D. Simons and M. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Software Tools for Technology Transfer, 3(4):469–485, 2001.
S. Tripakis. The formal analysis of timed systems in practice. PhD thesis, Université Joseph Fourier, 1998.
S. Tripakis. Timed diagnostics for reachability properties. In Proc. TACAS’99, volume 1579 of LNCS, pages 59–73. Springer, 1999.
M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. FOCS’85, pages 327–338. IEEE Computer Society Press, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kwiatkowska, M., Norman, G., Sproston, J. (2002). Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In: Hermanns, H., Segala, R. (eds) Process Algebra and Probabilistic Methods: Performance Modeling and Verification. PAPM-PROBMIV 2002. Lecture Notes in Computer Science, vol 2399. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45605-8_11
Download citation
DOI: https://doi.org/10.1007/3-540-45605-8_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43913-4
Online ISBN: 978-3-540-45605-6
eBook Packages: Springer Book Archive