Specification and analysis of the DCF and PCF protocols in the 802.11 standard using systems of communicating machines
Moustafa A. Youssef, A. Vasan, Raymond E. Miller · 2003
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.