Title: Using priced timed automata for the specification and verification of CSMA/CA in WSNs

Authors: Hmidi Zohra; Laid Kahloul; Saber Benharzallah

Addresses: LINFI Laboratory, Computer Science Department, Biskra University, Algeria ' LINFI Laboratory, Computer Science Department, Biskra University, Algeria ' LINFI Laboratory, Computer Science Department, Batna 2 University, Algeria

Abstract: Several contention-based MAC protocols for WSNs have been proposed. The control channel is accessed with carrier sense multiple access with collision avoidance (CSMA/CA) method. The complexity of this method and its criticality motivate the formal specification and verification of its basic algorithms. Most existing works do not deal with all possible aspects such as topology, number of nodes, node behaviour, and number of possible retransmissions. In this paper, we propose a stochastic generic model for the 802.11 MAC protocol for an arbitrary network topology which is independent of the number of sensors. In addition to the qualitative evaluation that proves the correctness of the model, we will make a quantitative evaluation using the statistical model checking to measure the probabilistic performance of the protocol.

Keywords: wireless sensor networks; WSNs; CSMA/CA; statistical model checking; SMC; priced timed automata; PTA; formal modelling; formal verification; UPPAAL.

DOI: 10.1504/IJICT.2020.108963

International Journal of Information and Communication Technology, 2020 Vol.17 No.2, pp.129 - 145

Accepted: 15 Jul 2019
Published online: 11 Aug 2020 *

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