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.
|Title of host publication||IEEE 64th Vehicular Technology Conference|
|Subtitle of host publication||VTC 2006-Fall|
|Place of Publication||Montreal, Canada|
|Publication status||Published - 27 Sep 2006|
- Modeling of the MAC
- formal verification
Haines, R., Clemo, G., & Munro, A. (2006). Toward Formal Verification of 802.11 MAC Protocols: Verifying a Petri-net Model of 802.11 PCF. In IEEE 64th Vehicular Technology Conference: VTC 2006-Fall (pp. 2315-2319). https://doi.org/10.1109/VTCF.2006.462