Open AccessSpecification and Verification of the IEEE 802.11 Medium Access Control and an Analysis of its Applicability to Real-Time Systems
Author(s) -
Frederico Barboza,
Aline Andrade,
Flávio Assis,
George Lima
Publication year - 2008
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2007.08.024
Subject(s) - computer science , model checking , concurrency , formal methods , access control , formal specification , formal verification , context (archaeology) , protocol (science) , domain (mathematical analysis) , distributed computing , programming language , computer network , medicine , paleontology , mathematical analysis , alternative medicine , mathematics , pathology , biology
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
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom