Title :
Formal modeling and verification of an enhanced variant of the IEEE 802.11 CSMA/CA protocol
Author :
Hammal, Youcef ; Ben-Othman, Jalel ; Mokdad, Lynda ; Abdelli, A.
Author_Institution :
Dept. of Comput. Sci., USTHB, Algiers, Algeria
Abstract :
In this paper, we present a formal method for modeling and checking an enhanced version of the carrier sense multiple access with collision avoidance protocol related to the IEEE 802.11 MAC layer, which has been proposed as the standard protocol for wireless local area networks. We deal mainly with the distributed coordination function (DCF) procedure of this protocol throughout a sequence of transformation steps. First, we use the unified modeling language state machines to thoroughly capture the behavior of wireless stations implementing a DCF, and then translate them into the input language of the UPPAAL model checking tool, which is a network of communicating timed automata. Finally, we proceed by checking of some of the safety and liveness properties, such as deadlock-freedom, using this tool.
Keywords :
carrier sense multiple access; finite state machines; telecommunication congestion control; wireless LAN; DCF procedure; IEEE 802.11 CSMA-CA protocol; IEEE 802.11 MAC layer; UPPAAL model checking tool; carrier sense multiple access protocol; collision avoidance protocol; deadlock-freedom tool; distributed coordination function procedure; enhanced variant verification; formal modeling; timed automata communication; transformation step sequence; unified modeling language state machine; wireless local area network; Automata; IEEE 802.11 Standards; Multiaccess communication; Protocols; Unified modeling language; Wireless communication; Wireless sensor networks; Carrier sense multiple access with collision avoidance; IEEE 802.11; UPPAAL; formal modeling; model checking; unified modeling language state machines;
Journal_Title :
Communications and Networks, Journal of
DOI :
10.1109/JCN.2014.000068
