@article {6702,
	title = {Using priced timed automata for the specification and verification of CSMA/CA in WSNs},
	journal = {International Journal of Information and Communication Technology},
	volume = {17},
	number = {2},
	year = {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.

},
	url = {https://www.inderscience.com/info/inarticle.php?artid=108963},
	author = {Hmidi, Zohra and Kahloul, Laid and Benharzallah, Saber}
}
