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 language | English |
---|---|
Title of host publication | Programming 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 |
Editors | Luís Caires |
Place of Publication | Cham |
Publisher | Springer |
Pages | 668-693 |
Number of pages | 26 |
ISBN (Electronic) | 978-3-030-17184-1 |
ISBN (Print) | 978-3-030-17183-4 |
DOIs | |
Publication status | Published - 6 Apr 2019 |
Event | 28th European Symposium on Programming - Prague, Czech Republic Duration: 8 Apr 2019 → 11 Apr 2019 Conference number: 28 https://conf.researchr.org/track/etaps-2019/esop-2019-papers |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Cham |
Volume | 11423 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Symposium
Symposium | 28th European Symposium on Programming |
---|---|
Abbreviated title | ESOP 2019 |
Country/Territory | Czech Republic |
City | Prague |
Period | 8/04/19 → 11/04/19 |
Internet address |