Title :
Specification and analysis of the DCF and PCF protocols in the 802.11 standard using systems of communicating machines
Author :
Youssef, Moustafa A. ; Vasan, Arunchandar ; Miller, Raymond E.
Author_Institution :
Dept. of Comput. Sci., Maryland Univ., College Park, MD, USA
Abstract :
We propose and analyze formal models for coordination functions of the 802.11 MAC layer using systems of communicating machines. We model the basic DCF (CSMA/CA) protocol, the DCF (distributed coordination function) protocol with RTS/CTS (MACA), and the PCF (point coordination function) protocol. Analyses show the following safety results: the CSMA/CA protocol is free from deadlocks and non-executable transitions; the MACA has a potential livelock, but is free from deadlocks and non-executable transitions; the PCF protocol is free from deadlocks and non-executable transitions. We also show that liveness is guaranteed in the PCF protocol.
Keywords :
access protocols; carrier sense multiple access; finite state machines; wireless LAN; CSMA/CA; CTS; IEEE 802.11 standard; MAC layer; RTS; WLAN; clear to send; communicating machines; deadlocks; distributed coordination function protocol; livelock; nonexecutable transitions; point coordination function protocol; request to send; state machine; wireless LAN; Access protocols; Communication standards; Computer science; Context modeling; Educational institutions; Multiaccess communication; System recovery; Terminology; Wireless LAN; Wireless communication;
Conference_Titel :
Network Protocols, 2002. Proceedings. 10th IEEE International Conference on
Print_ISBN :
0-7695-1856-7
DOI :
10.1109/ICNP.2002.1181394
