|
 
|
[ZBB10] Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol
Revue Internationale avec comité de lecture : Journal International Journal of Wireless & Mobile Networks, vol. 2(2), pp. 156-170, 2010
motcle:
Résumé:
Communication protocols and techniques are often evaluated using simulation techniques. However, the
use of formal modeling and analysis techniques for verification and evaluation in particular for Wireless
Sensor Networks (WSN) becomes a necessity. In this paper we present a formal analysis of the backoff
procedure integrated in the medium access control protocol named ECo-MAC designed for WSN. We
describe this backoff procedure in terms of discrete time Markov chains (DTMCs) and evaluated using
the well known probabilistic model checker PRISM. After checking the different invariants of the
proposed model, we study the effect of contention window length (in number of time contention unit) on
the acceptable number of simultaneous senders in a neighborhood of a given receiver. The obtained
quantitative results confirm those provided by the simulation using OPNET tool and justify the validity of
the adopted value for the time contention unit TCU.
Keywords: Wireless Sensor Network, ECo-MAC protocol, probabilistic model checking.
For further information, please visit this web site.
Keywords: Wireless Sensor Network, ECo-MAC protocol, probabilistic model checking.
For further information, please visit this web site.
BibTeX
| @article { | |||
| ZBB10, | |||
| title | = | "{Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol}", | |
| author | = | "H. Zayani and K. Barkaoui and R. Ben Ayed", | |
| journal | = | "International Journal of Wireless & Mobile Networks", | |
| year | = | 2010, | |
| volume | = | 2, | |
| number | = | 2, | |
| pages | = | "156-170", | |
| } | |||
