Formal modeling and checking of an enhanced variant of the IEEE 802.11 CSMA/CA protocol

In this paper we present a formal modeling and verification method of an enhanced version of the CSMA/CA protocol related to the IEEE 802.11 MAC layer, which has been proposed as the standard protocol for wireless local area networks (LANs). We deal mainly with the DCF procedure of this protocol throughout a sequence of transformation steps. We first use UML state machines to capture the behavior of wireless stations implementing the DCF and we thereafter translate them into the input language of the UPPAAL model checker, that is a network of communicating timed automata. Last, we proceed with the checking of some safety and liveness properties by means of this tool, such as deadlock-freedom.