论文标题
基于演员的模型检查SDN网络
Actor-Based Model Checking for SDN Networks
论文作者
论文摘要
软件定义的网络（SDN）是一个网络范式，在过去十年中越来越流行。它提供的网络全球行为的前所未有的控制为正式方法开放了一系列新的机会，并且在过去几年中，已经出现了许多工作，以提供SDN和验证之间的桥梁。本文推进了该研究线，并提供了SDN与传统工作的正式方法之间的联系，以验证并发和分布式软件 - 基于Actor的建模。我们展示了如何使用\ emph {Actors}无缝建模SDN程序，因此可以直接应用针对参与者开发的现有高级模型检查技术来验证SDN网络的一系列属性，包括流量表的一致性，违反安全策略和转发循环。我们用于SDN网络的模型检查器可通过在线Web界面获得，该界面还为许多众所周知的SDN基准提供了SDN Actor-Models。
Software-Defined Networking (SDN) is a networking paradigm that has become increasingly popular in the last decade. The unprecedented control over the global behavior of the network it provides opens a range of new opportunities for formal methods and much work has appeared in the last few years on providing bridges between SDN and verification. This article advances this research line and provides a link between SDN and traditional work on formal methods for verification of concurrent and distributed software---actor-based modelling. We show how SDN programs can be seamlessly modelled using \emph{actors}, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops. Our model checker for SDN networks is available through an online web interface, that also provides the SDN actor-models for a number of well-known SDN benchmarks.
