Formal Analysis of an Energy-aware Collision Resolution Protocol for Wireless Sensor Networks

This paper provides a comprehensive and rigorous study of a novel collision resolution algorithm for wireless sensor networks: 2CS-WSN. It is specifically designed to be used during the contention phase of IEEE 802.15.4. This algorithm has been modelled in terms of discrete time Markov chains (DTMCs...

Full description

Saved in:
Bibliographic Details
Published in:Procedia computer science 2016, Vol.80, p.1191-1201
Main Authors: Ruiz, M.C., Macià, H., Mateo, J.A., Calleja, J.
Format: Article
Language:English
Subjects:
Collision resolution algorithms
Markov chains
Modelling and simulation
Performance Evaluation
Probabilistic model checking
Wireless Sensor Networks
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper provides a comprehensive and rigorous study of a novel collision resolution algorithm for wireless sensor networks: 2CS-WSN. It is specifically designed to be used during the contention phase of IEEE 802.15.4. This algorithm has been modelled in terms of discrete time Markov chains (DTMCs) and, using the probabilistic symbolic model checker PRISM, correctness properties and different operation modes of the algorithm have been studied. Moreover, different model abstractions have been used in order to identify any inconsistencies or ambiguities, and to prove interesting properties for non-trivial, practical and relevant scenarios. Finally, since the biggest source of energy waste is the collision, this paper conducts a wide study of energy saving in this algorithm.
ISSN:1877-0509
1877-0509
DOI:10.1016/j.procs.2016.05.461