Trustworthy Systems

A process algebra for link layer protocols

Authors

Peter Hoefner, Rob van Glabbeek and Michael Markl

DATA61

Australian National University

UNSW Sydney

Abstract

We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling the collision of data packets. 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 also show that the version with virtual carrier sensing overcomes not only this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.

BibTeX Entry

  @inproceedings{Hoefner_GM_19,
    address          = {Prague, Czech Republic},
    author           = {H\"{o}fner, Peter and van Glabbeek, Robert and Markl, Michael},
    booktitle        = {European Symposium on Programming},
    date             = {2019-4-6},
    doi              = {https://doi.org/10.1007/978-3-030-17184-1\_24},
    month            = apr,
    numpages         = {25},
    paperurl         = {https://trustworthy.systems/publications/full_text/Hoefner_GM_19.pdf},
    publisher        = {Springer},
    title            = {{A} Process Algebra for Link Layer Protocols},
    volume           = {11423},
    year             = {2019}
  }

Download