Title: Probabilistic model checking of IEEE 802.11 IBSS power save mode

Authors: Pravati Swain; Purandar Bhaduri; Sukumar Nandi

Addresses: Department of CSE, IIT Guwahati, Guwahati 781039, India ' Department of CSE, IIT Guwahati, Guwahati 781039, India ' Department of CSE, IIT Guwahati, Guwahati 781039, India

Abstract: The IEEE 802.11 standard for wireless local area network defines a power management algorithm for Independent Basic Service Set (IBSS). In the power management for IBSS, time is divided into Beacon Intervals (BIs) and each BI is divided into an Announcement Traffic Indication Message (ATIM) window and a data window. The stations that have successfully transmitted an ATIM frame within the ATIM window will compete to transmit a data frame in the data window. The rest of the stations go to sleep mode during the data window, thus saving power. The power management algorithm for IBSS mode, based on a randomised exponential backoff procedure, is defined in the IEEE 802.11 standard for wireless LANs. The probabilistic behaviour of the MAC mechanism enables us to design a probabilistic model suitable for model checking. This paper presents a finite state Markov Decision Process (MDP) and uses the tool PRISM to compute the performance of the IEEE 802.11 IBSS in PSM. A set of performance properties, such as expected delay and energy consumption, is specified as queries in the probabilistic temporal logic PCTL and computed using PRISM.

Keywords: IEEE 802.11 standard; MDP; Markov decision process; PCTL; ATIM frame; energy consumption; probabilistic model checking; IBSS power save mode; wireless LANs; WLANs; local area networks; power management; expected delay.

DOI: 10.1504/IJWMC.2014.064818

International Journal of Wireless and Mobile Computing, 2014 Vol.7 No.5, pp.465 - 474

Received: 23 Jul 2013
Accepted: 09 Feb 2014
Published online: 31 Oct 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article