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.
International Journal of Information and Communication Technology, 2020 Vol.17 No.2, pp.129 - 145
Accepted: 15 Jul 2019
Published online: 09 Jul 2020 *