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)