Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol

  • Marta Kwiatkowska
  • Gethin Norman
  • Jeremy Sproston
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2399)


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.”


Medium Access Control Model Check Data Packet Distribute Coordination Function Trace Distribution 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    R. Alur, A. Itai, R.P. Kurshan, and M. Yannakakis. Timing verification by successive approximation. Information and Computation, 18(1):142–157, 1995.CrossRefMathSciNetGoogle Scholar
  3. 3.
    D. Beyer. Improvements in BDD-based reachability analysis of timed automata. In Proc. FME’01, volume 2021 of LNCS, pages 318–343. Springer, 2001.Google Scholar
  4. 4.
    G. Bianchi. Performance analysis of the IEEE 802.11 distributed coordination function. IEEE Journal on Selected Areas in Communication, 18:535–547, 2000.CrossRefGoogle Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    C. Derman. Finite-State Markovian Decision Processes. Academic Press, 1970.Google Scholar
  10. 10.
    H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.zbMATHCrossRefGoogle Scholar
  11. 11.
    A. Heindl and R. German. Performance modeling of IEEE 802.11 wireless LANs with stochastic Petri nets. Performance Evaluation, 44:139–164, 2001.zbMATHCrossRefGoogle Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    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.Google Scholar
  14. 14.
    J. G. Kemeny, J. L. Snell, and A. W. Knapp. Denumerable Markov Chains. Graduate Texts in Mathematics. Springer, 2nd edition, 1976.Google Scholar
  15. 15.
    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.Google Scholar
  16. 16.
    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.Google Scholar
  17. 17.
    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.Google Scholar
  18. 18.
    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.Google Scholar
  19. 19.
    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.Google Scholar
  20. 20.
    K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1+2):134–152, 1997.zbMATHCrossRefGoogle Scholar
  21. 21.
  22. 22.
    R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995.Google Scholar
  23. 23.
    R. Segala and N. A. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250–273, 1995.zbMATHMathSciNetGoogle Scholar
  24. 24.
    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.zbMATHGoogle Scholar
  25. 25.
    S. Tripakis. The formal analysis of timed systems in practice. PhD thesis, Université Joseph Fourier, 1998.Google Scholar
  26. 26.
    S. Tripakis. Timed diagnostics for reachability properties. In Proc. TACAS’99, volume 1579 of LNCS, pages 59–73. Springer, 1999.Google Scholar
  27. 27.
    M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. FOCS’85, pages 327–338. IEEE Computer Society Press, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Marta Kwiatkowska
    • 1
  • Gethin Norman
    • 1
  • Jeremy Sproston
    • 2
  1. 1.School of Computer ScienceUniversity of BirminghamBirminghamUK
  2. 2.Dipartimento di InformaticaUniversità di TorinoTorinoItaly

Personalised recommendations