使用Relational NetKAT进行网络变更验证

《Proceedings of the ACM on Programming Languages》：Network Change Validation with Relational NetKAT

Relational NetKAT（RN）是一种新规范语言，用于验证网络变更。工程师通过trace relation R映射预变更和后变更的流量轨迹，检查实际结果与预期的一致。RN使用组合子构建trace relation，并转化为NetKAT转换器，构建自动机验证网络变更，提供形式语义和算法正确性证明，工具实现并通过生产网络和Batfish基准测试。

　　

摘要人工智能摘要

要查看此由人工智能生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

Relational NetKAT (RN) 是一种用于网络变更验证的新规范语言。工程师通过提供 trace 关系 R 来指定预期的变更，该关系将变更前的网络中的现有数据包跟踪映射到变更后的网络中的预期数据包跟踪。然后可以将这些 预期 的跟踪与变更后的 实际 跟踪进行比较，以发现实施中的错误。Trace 关系是通过组合器语言构建的，这些组合器包括跟踪插入、跟踪删除和数据包转换，以及用于关系连接、合并和迭代的常规操作符。我们提供了将 trace 关系转换为 NetKAT 转换器的新形式的算法，以及构建能够识别 NetKAT 转换器下的 NetKAT 自动机图像的自动机的算法。这些算法，加上现有的 NetKAT 自动机等价性决策程序，足以用于验证网络变更。我们为我们的规范语言提供了表示语义，证明了我们的编译算法的正确性，实现了一个用于网络变更验证的工具，并在来自生产网络和 Amazon 的 Batfish 工具包的一组基准测试上对其进行了评估。

人工智能摘要

人工智能生成的摘要（实验性）

此摘要是使用自动化工具生成的，并非由文章作者编写或审核的。它旨在帮助发现、帮助读者评估相关性，并协助来自相关研究领域的读者理解该工作。它旨在补充作者提供的摘要，后者仍然是论文的主要摘要。完整文章是权威版本。点击此处了解更多。

点击 此处 对此摘要的准确性、清晰度和有用性进行评论。这样做将有助于改进和未来重新生成的版本。

要查看此由人工智能生成的纯文本摘要，您必须具有高级访问权限。