Formal modeling and checking of an enhanced variant of the IEEE 802.11 CSMA/CA protocol

Author

Hammal, Youcef ; Ben-Othman, Jalel ; Mokdad, Lynda ; Abdelli, A.

Author_Institution

LSI, USTHB, Algiers, Algeria

fYear

2014

fDate

23-26 June 2014

Firstpage

1

Lastpage

6

Abstract

In this paper we present a formal modeling and verification method of an enhanced version of the CSMA/CA protocol related to the IEEE 802.11 MAC layer, which has been proposed as the standard protocol for wireless local area networks (LANs). We deal mainly with the DCF procedure of this protocol throughout a sequence of transformation steps. We first use UML state machines to capture the behavior of wireless stations implementing the DCF and we thereafter translate them into the input language of the UPPAAL model checker, that is a network of communicating timed automata. Last, we proceed with the checking of some safety and liveness properties by means of this tool, such as deadlock-freedom.

Keywords

Unified Modeling Language; carrier sense multiple access; finite state machines; formal verification; protocols; wireless LAN; CA protocol; CSMA protocol; DCF procedure; IEEE 802.11; LAN; MAC layer; UML state machines; UPPAAL model checker; carrier sense multiple access; collision avoidance protocol; deadlock-freedom; distributed coordination function; formal modeling; medium access control; transformation steps sequence; wireless local area networks; Computational modeling; Lead; Media Access Protocol;

fLanguage

English

Publisher

ieee

Conference_Titel

Computers and Communication (ISCC), 2014 IEEE Symposium on

Conference_Location

Funchal

Type

conf

DOI

10.1109/ISCC.2014.6912620

Filename

6912620