Computer Science – Networking and Internet Architecture
Scientific paper
2010-05-12
International Journal of Wireless & Mobile Networks 2.2 (2010) 156-170
Computer Science
Networking and Internet Architecture
15 Pages, IJWMN 2010
Scientific paper
10.5121/ijwmn.2010.2211
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.
Ayed Rahma Ben
Barkaoui Kamel
Zayani Hafedh
No associations
LandOfFree
Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-499284