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

• DOI: 10.1016/j.entcs.2007.08.024
• Publication Date: 2008-02-06T09:08:54Z
• Authors: Frederico J.R. Ba...; Aline M.S. Andrade; Flávio Assis Silva; George Lima
• Keywords: Wireless Network; Software Reliability; 0202 electrical engineering, electronic engineering, information engineering; Real-Time Systems; Software Specification; 02 engineering and technology; Formal Methods; Theoretical Computer Science; Computer Science(all)

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