Analyzing the Point Coordination Function of the IEEE 802.11 WLAN Protocol using a Systems of Communicating Machines Specification

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)