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

Russell Haines; Gary Clemo; Alistair Munro

doi:10.1109/VTCF.2006.462

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

Russell Haines, Gary Clemo, Alistair Munro

Department of Electrical & Electronic Engineering

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

5 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 language	English
Title of host publication	IEEE 64th Vehicular Technology Conference
Subtitle of host publication	VTC 2006-Fall
Place of Publication	Montreal, Canada
Pages	2315-2319
ISBN (Electronic)	1-4244-0063-5
DOIs	https://doi.org/10.1109/VTCF.2006.462
Publication status	Published - 27 Sept 2006

Keywords

Modeling of the MAC
WLAN
formal verification

Access to Document

10.1109/VTCF.2006.462

Handle.net

Persistent link

Cite this

@inproceedings{31a7560811ba4fe8b2191ef8d8157c59,

title = "Toward Formal Verification of 802.11 MAC Protocols: Verifying a Petri-net Model of 802.11 PCF",

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.",

keywords = "Modeling of the MAC, WLAN, formal verification",

author = "Russell Haines and Gary Clemo and Alistair Munro",

year = "2006",

month = sep,

day = "27",

doi = "10.1109/VTCF.2006.462",

language = "English",

isbn = "1-4244-0062-7 ",

pages = "2315--2319",

booktitle = "IEEE 64th Vehicular Technology Conference",

}

TY - GEN

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

AU - Haines, Russell

AU - Clemo, Gary

AU - Munro, Alistair

PY - 2006/9/27

Y1 - 2006/9/27

N2 - 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.

AB - 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.

KW - Modeling of the MAC

KW - WLAN

KW - formal verification

U2 - 10.1109/VTCF.2006.462

DO - 10.1109/VTCF.2006.462

M3 - Conference Contribution (Conference Proceeding)

SN - 1-4244-0062-7

SP - 2315

EP - 2319

BT - IEEE 64th Vehicular Technology Conference

CY - Montreal, Canada

ER -

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

Abstract

Keywords

Access to Document

Handle.net

Fingerprint

Cite this