DyNetKAT：动态网络代数
网络与互联网体系结构
2021-05-25 v4 形式语言与自动机理论
摘要
我们引入一种用于指定软件定义网络动态更新的形式化语言。我们的语言构建于带测试的网克莱尼代数（NetKAT）之上，并添加了同步与多包行为构造以捕获动态更新中控制平面与数据平面之间的交互。我们提供了该语言的一个可靠且基完全的演算公理系统。我们利用该等式理论为动态网络的安全性性质提供高效推理方法。我们在DyNetiKAT——一个基于Maude重写逻辑与NetKAT工具的工原型——中实现了我们的等式理论，并将其应用于一个案例研究。我们展示了利用初始工具原型可分析具有数百个交换机的网络的案例研究。
引用
@article{arxiv.2102.10035,
title = {DyNetKAT: An Algebra of Dynamic Networks},
author = {Georgiana Caltais and Hossein Hojjat and Mohammad Mousavi and Hunkar Can Tunc},
journal= {arXiv preprint arXiv:2102.10035},
year = {2021}
}