Specification and Analysis of the DCF Protocol in the 802.11 Standard using Systems of Communicating Machines

Abstract

The 802.11 specification is an emerging standard for WLANs. In this paper, we propose a formal model for a section of the 802.11 MAC protocol using systems of communicating machines. We model the ad-hoc mode of the DCF, i.e., CSMA/CA protocol and the MACA\footnote{The 802.11 standard does not refer to RTS/CTS exchanges as MACA. However, the paper which introduced this idea called it the MACA, and we use this name.} using RTS/CTS sequences. Each station is modelled as a finite state machine which has a set of local variables, and the Wireless Medium is modelled as a shared variable. Analyses show that the 802.11 MAC CSMA/CA protocol and the MACA using RTS/CTS exchanges are free from state deadlocks and non-executable transitions. However, the MACA protocol has a potential livelock, though it is unlikely it will come to pass in normal operation. (Also UMIACS-TR-2002-37)