Skip to content

Toward formal verification of 802.11 MAC protocols: a case study of applying Petri-nets to modeling the 802.11 PCF

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • RJ Haines
  • ATD Munro
  • GR Clemo
Original languageEnglish
Title of host publicationIEEE 63rd Vehicular Technology Conference, VTC 2006, Montreal, Canada, Spring
Publisher or commissioning bodyInstitute of Electrical and Electronics Engineers (IEEE)
Publication dateSep 2006
Pages1171 - 1175
Number of pages5
ISBN (Print)0780393929

Publication series

ISSN (Print)15502252


Conference63rd Vehicular Technology Conference 2006 (VTC 2006-Spring)
Period1/05/06 → …


Centralized control functions for the IEEE802.11 family of WLAN standards are vital for the distribution of traffic with stringent Quality of Service (QoS) requirements. These centralized control functions overlay a time-based organizational "super-frame" structure on the medium, allocating part of the super-frame to polling traffic and part to contending traffic. This allocation directly determines how well the two forms of traffic are supported. Given the vital role of this allocation in the success of a system, we must have confidence in the configuration used, beyond that provided by empirical simulation results. Formal mathematical methods are a means to conduct rigorous analysis that will permit us such confidence, and the Petri-net formalism offers an intuitive representation with formal semantics. We present an extended Petri-net model of the super-frame, and use this model to assess the performance of different super-frame configurations and the effects of different traffic patterns. We believe that using such a model to analyze performance in this manner is new in itself

Additional information

Rose publication type: Conference contribution Sponsorship: This work has been funded and supported by Toshiba Research Europe Limited, Telecommunications Research Laboratory Terms of use: Copyright © 2006 IEEE. Reprinted from IEEE 63rd Vehicular Technology Conference, 2006 (VTC 2006-Spring). This material is posted here with permission of the IEEE. Such permission of the IEEE does not in any way imply IEEE endorsement of any of the University of Bristol's products or services. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to By choosing to view this document, you agree to all provisions of the copyright laws protecting it.

Research areas

  • WLAN, MAC, formal venification, Petri-net, PCF


63rd Vehicular Technology Conference 2006 (VTC 2006-Spring)

Duration1 May 2006 → …

Event: Conference


View research connections

Related faculties, schools or groups