Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings
Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings
复制标题
软件科学与计算结构基础 - 第 25 届国际会议，FOSSACS 2022，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2022，德国慕尼黑，2022 年 4 月 2-7 日，会议记录
DOI：
10.1007/978-3-030-99253-8_10
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Caltais G
中科院分区：
文献类型：
--
作者：
Caltais G
我们介绍了一种形式化的语言，用于指定软件定义网络的动态更新。我们的语言建立在网络Kleene代数与测试（NetKAT），并增加了同步和多包行为的结构，以捕捉动态更新中的控制和数据平面之间的交互。我们提供了一个健全的和地面完整的公理化我们的语言。我们利用方程理论，并提供了一个有效的方法来推理安全性能。我们实现了我们的方程理论在DyNetiKAT-一个工具原型，基于Maude重写逻辑和NetKAT工具，并将其应用到一个案例研究。我们表明，我们可以使用我们的工具原型分析数百个交换机的网络的案例研究。
We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control-and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory and provide an efficient method for reasoning about safety properties. We implement our equational theory in DyNetiKAT–a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our tool prototype.