A Process Algebra for Link Layer Protocols

Rob van Glabbeek, Peter Höfner, Michael Markl

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationProgramming Languages and Systems: 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings
EditorsLuís Caires
Place of PublicationCham
PublisherSpringer
Pages668-693
Number of pages26
ISBN (Electronic)978-3-030-17184-1
ISBN (Print)978-3-030-17183-4
DOIs
Publication statusPublished - 6 Apr 2019
Event28th European Symposium on Programming - Prague, Czech Republic
Duration: 8 Apr 201911 Apr 2019
Conference number: 28
https://conf.researchr.org/track/etaps-2019/esop-2019-papers

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Cham
Volume11423
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Symposium

Symposium28th European Symposium on Programming
Abbreviated titleESOP 2019
Country/TerritoryCzech Republic
CityPrague
Period8/04/1911/04/19
Internet address

Fingerprint

Dive into the research topics of 'A Process Algebra for Link Layer Protocols'. Together they form a unique fingerprint.

Cite this