Using priced timed automata for the specification and verification of CSMA/CA in WSNs
by Hmidi Zohra; Laid Kahloul; Saber Benharzallah
International Journal of Information and Communication Technology (IJICT), Vol. 17, No. 2, 2020

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.

Online publication date: Tue, 11-Aug-2020

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Information and Communication Technology (IJICT):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com