Specification and Verification of the IEEE 802.11 Medium Access Control and an Analysis of its Applicability to Real-Time Systems

Abstract

The use domain of IEEE 802.11 networks has broadened to several types of application, including those that require quality of service and real-time guarantees. This trend in particular, has motivated the use of formal methods, not only to obtain a more precise knowledge of protocol properties, but also to specify and validate them. In this context, the contribution of this paper is twofold. First, we describe a formal specification of the IEEE 802.11 medium access control functions using UPPAAL, a freeware model checker tool. The described specification allowed us to verify important properties of these functions, taking into account both time and concurrency. Second, we report an experience of model checking a widely used and reasonably complex communication protocol, taking into consideration temporal requirements.