OSPF 路由协议的形式化模型
网络与互联网体系结构
2020-04-29 v1 计算机科学中的逻辑
摘要
我们提出了 OSPF 路由协议的三个形式化模型。前两个在定时进程代数 T-AWN 中形式化，该代数不仅专为路由协议定制，还以易读的伪代码描述协议。两个模型之间的区别在于细节程度（抽象层级）。我们从较抽象的模型生成第三个模型。它基于定时自动机网络，并可在模型检测器 Uppaal 中执行。
引用
@article{arxiv.2004.13286,
title = {Formal Models of the OSPF Routing Protocol},
author = {Jack Drury and Peter Höfner and Weiyou Wang},
journal= {arXiv preprint arXiv:2004.13286},
year = {2020}
}
备注
In Proceedings MARS 2020, arXiv:2004.12403