Analyzing the Point Coordination Function of the IEEE 802.11 WLAN Protocol using a Systems of Communicating Machines Specification
Analyzing the Point Coordination Function of the IEEE 802.11 WLAN Protocol using a Systems of Communicating Machines Specification
Loading...
Files
Publication or External Link
Date
2002-05-22
Authors
Youssef, Moustafa A.
Miller, Raymond E.
Advisor
Citation
DRUM DOI
Abstract
A model for the specification and analysis of communication protocols
called Systems of Communicating Machines is used to specify an IEEE
802.11 Point Coordination Function protocol, and to analyze it for
safety and certain restricted liveness properties. The model uses a
combination of finite state machines and variables in the specification
of each machine, and the communication between machines is accomplished
through shared variables. Enabling predicates and actions are associated
with each transition; the enabling predicates determine when a
transition may be taken, and the actions alter the variable values as
the network progresses.
One of the advantages which this model has over most other formal
description techniques is that simultaneous transitions are allowed.
Another advantage is the use of shared variables rather than FIFO queues
for communication between machines. This allows the modeling of the
shared medium as a single shared variable variable between all
communicating processes.
Unlike the SDL language which is used in the specification of the 802.11
standard, the Systems of Communicating Machines model is more compact,
easier to understand, and easier to analyze for safety and liveness.
(Also UMIACS-TR-2002-36)