Toward Formal Verification of 802.11 MAC Protocols: Verifying a Petri-Net Model of 802.11 PCF

The delivery of traffic with stringent Quality of Service (QoS) requirements over wireless local area networks (WLAN) is a vital research topic. A solution is to adopt centralized control functions, which allocate part of the bandwidth to polling traffic and part to contending traffic. Reliable means of performing this allocation are required as this allocation directly determines how well the two forms of traffic can coexist. In an earlier publication we presented an extended Petri-net model of an IEEE802.11 centralized control scheme, and used this model in the manner of a simulation tool to analyze performance, promising analysis of the model to come. Here we perform verification on aspects of the model to verify key properties of the system, something that is only possible by virtue of the strong mathematical basis of Petri-nets.