一种用于链路层协议的进程代数
网络与互联网体系结构
2019-08-01 v1 计算机科学中的逻辑
摘要
我们提出了一种用于链路层协议的进程代数，其特点是一种用于建模帧冲突的独特机制。我们还在此框架内为所指定的链路层协议形式化了合适的活性性质。为展示适用性，我们对免冲突载波侦听多路访问（CSMA/CA）协议的两个版本进行了建模与分析。我们的分析证实了无虚拟载波侦听版本存在隐藏站问题。然而，我们表明带虚拟载波侦听的版本不仅克服了该问题，而且以概率 1 克服了暴露站问题。但该协议仍无法保证数据包交付，即便以概率 1 也不能。
引用
@article{arxiv.1907.13329,
title = {A Process Algebra for Link Layer Protocols},
author = {Rob van Glabbeek and Peter Höfner and Michael Markl},
journal= {arXiv preprint arXiv:1907.13329},
year = {2019}
}