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.
Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Wed 10 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Asynchronous timed session types: duality and time-sensitive processes ESOP Laura Bocchi University of Kent, Maurizio Murgia , Vasco T. Vasconcelos University of Lisbon, Portugal, Nobuko Yoshida Imperial College London Link to publication | ||
14:30 30mTalk | Manifest Deadlock-Freedom for Shared Session Types ESOP Stephanie Balzer Carnegie Mellon University, Bernardo Toninho Imperial College London, Frank Pfenning Carnegie Mellon University, USA Link to publication | ||
15:00 30mTalk | A Categorical Model of an i/o-typed pi-calculus ESOP Link to publication | ||
15:30 30mTalk | A Process Algebra for Link Layer Protocols ESOP Link to publication | ||