Probabilistic verification and evaluation of Backoff procedure of the WSN ECo-MAC protocol

TL;DR

This paper presents a formal probabilistic analysis of the backoff procedure in the ECo-MAC protocol for WSNs using Markov chains and model checking, validating simulation results and parameter choices.

Contribution

It introduces a formal probabilistic model of the ECo-MAC backoff procedure and evaluates its behavior using PRISM, providing a rigorous verification approach for WSN protocols.

Findings

Validation of the backoff procedure through probabilistic model checking.

Confirmation of simulation results regarding contention window effects.

Justification of the chosen contention time unit TCU.

Abstract

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.