Formal specification and analysis of the PCF protocol in the 802.11 standard using systems of communicating machines

With the widespread usage of the 802.11 protocol, it becomes important to study the protocol operation. In this paper we propose a formal model for the point coordination function (PCF) of the 802.11 MAC layer using systems of communicating machines. Our goal is to analyse the protocol for safety and liveness properties. These properties cannot be verified directly from the protocol description. Analysis shows that the PCF protocol is free from deadlocks and non-executable transitions. We also show that liveness is guaranteed in the PCF protocol.