Toward Formal Verification of 802.11 MAC Protocols: a Case Study of Applying Petri-nets to Modeling the 802.11 PCF

Russell Haines, Alistair T D Munro, Gary R Clemo

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

3 Citations (Scopus)
328 Downloads (Pure)

Abstract

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.
Translated title of the contributionToward Formal Verification of 802.11 MAC Protocols: a Case Study of Applying Petri-nets to Modeling the 802.11 PCF
Original languageEnglish
Title of host publication2006 IEEE 63rd Vehicular Technology Conference
Subtitle of host publicationProceedings of a meeting held 7-10 May 2006, Melbourne, Australia
Place of PublicationMelbourne, Australia
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages1171-1175
Number of pages5
Volume3
ISBN (Electronic)9780780393929
ISBN (Print)9780780393910
DOIs
Publication statusPublished - 8 May 2006
Event63rd Vehicular Technology Conference 2006 (VTC 2006-Spring) - Melbourne, Australia
Duration: 1 May 2006 → …

Publication series

NameIEEE Vehicular Technology Conference
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
ISSN (Print)1550-2252

Conference

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

Keywords

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

Fingerprint Dive into the research topics of 'Toward Formal Verification of 802.11 MAC Protocols: a Case Study of Applying Petri-nets to Modeling the 802.11 PCF'. Together they form a unique fingerprint.

Cite this