WNetKAT：一种加权 SDN 编程与验证语言
网络与互联网体系结构
2016-12-01 v4
摘要
可编程性和可验证性是软件定义网络范式核心。虽然 OpenFlow 及其匹配-动作概念提供了操作硬件配置的基本操作，但过去几年中，已开发出数种更具表现力的网络编程语言。本文提出了 WNetKAT，这是第一种考虑到网络固有加权特性以及通信受容量约束（例如带宽）和成本（例如延迟或货币成本）影响的网络编程语言。WNetKAT 基于 NetKAT 代数的语法和语义扩展。我们展示了 WNetKAT 的几种相关应用，包括成本和容量感知的可达性，以及服务质量与公平性方面。这些应用不仅适用于经典的可分割和不可分割 (s; t)-流，还推广到更复杂的网络功能和服务链。例如，WNetKAT 允许对需要穿越某些可能改变流量速率的中继点功能的流进行建模。本文还展示了 WNetKAT 的等价性问题与加权有限自动机的等价性问题之间的关系，这意味着前者是不可判定的。然而，本文也成功证明了另一个有用问题的可判定性，这在许多实际场景中已足够：即一个表达式是否等于 0。此外，我们发起了对整个语言可判定子集的讨论。
引用
@article{arxiv.1608.08483,
title = {WNetKAT: A Weighted SDN Programming and Verification Language},
author = {Kim G. Larsen and Stefan Schmid and Bingtian Xue},
journal= {arXiv preprint arXiv:1608.08483},
year = {2016}
}