Formal Specification and Analysis of 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, the authors propose a formal model for the point coordination function of the 802.11 MAC layer using systems of communicating machines. Their goal is to analyze 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. They also show that liveness is guaranteed in the PCF protocol.