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

AbstractThis 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