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

Russell Haines, Gary Clemo, Alistair Munro

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

4 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationIEEE 64th Vehicular Technology Conference
Subtitle of host publicationVTC 2006-Fall
Place of PublicationMontreal, Canada
Pages2315-2319
ISBN (Electronic)1-4244-0063-5
DOIs
Publication statusPublished - 27 Sep 2006

Keywords

  • Modeling of the MAC
  • WLAN
  • formal verification

Fingerprint Dive into the research topics of 'Toward Formal Verification of 802.11 MAC Protocols: Verifying a Petri-net Model of 802.11 PCF'. Together they form a unique fingerprint.

  • Cite this

    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