Abstract:
The protocol IEEE 802.11 is used for wireless local area networks. It is an example of a decentralized control algorithm. Frames are exchanged between stations which have different private information. The control objectives are: to deliver frames to other stations, to control the flow of frames, to control access to the wireless medium, to provide fault tolerant control, and to avoid deadlock. A model for the operation of a wireless network is formulated in terms of a layered architechture with at each level a finite-state automaton. A network of two and of four stations is constructed based on a model for each station and for the ether between the stations. Verification of the control objectives for these networks has been carried out using the tool UMDES (University of Michigan, Ann Arbor, MI, U.S.A.). The main contribution of the paper is the layered architecture for the protocol which will be useful for construction of future protocols.

Slides (.pdf)