We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling frame collisions. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse two versions of the Carrier-Sense Multiple Access with Collision Avoidance (CSMA CA) protocol. Our analysis confirms the hidden station problem for the version without virtual carrier sensing. However, we show that the version with virtual carrier sensing not only overcomes this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.
-3pt Following the spirit of the above-mentioned research of model checking CSMA, Fruth @cite_18 analyses CSMA CA using PTAs and . He considers properties such as the minimum probability of two nodes successfully completing their transmissions, and maximum expected number of collisions until two nodes have successfully completed their transmissions. As before, this analysis technique does not scale; in @cite_18 the experiments are limited to two contending nodes only.
@cite_18
2137013587
The international standard IEEE 802.15.4 defines low-rate wireless personal area networks, a central communication infrastructure of pervasive computing. In order to avoid conflicts caused by multiple devices transmitting at the same time, it uses a contention resolution algorithm based on randomised exponential backoff that is similar to the ones used in IEEE 802.3 for Ethernet and IEEE 802.11 for Wireless LAN. We model the protocol using probabilistic timed automata, a formalism in which both nondeterministic and probabilistic choice can be represented. The probabilistic timed automaton is transformed into a finite-state Markov decision process via a property-preserving integral-time semantics. Using the probabilistic model checker PRISM, we verify correctness properties, compare different operation modes of the protocol, and analyse performance and accuracy of different model abstractions.