[KNS02a] M. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In H. Hermanns and R. Segala (editors), Proc. PAPM/PROBMIV'02, volume 2399 of Lecture Notes in Computer Science, pages 169-187, Springer. July 2002. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (119 KB)  pdf pdf (342 KB)  bib bib
Notes: Further information and verification results are available from the PRISM web page. The original publication is available at link.springer.com.
Links: [Google] [Google Scholar]
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, randomized exponential backoff rules are used in the retransmission scheme to minimize 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."