论文标题
ADAMMC：针对Flow-LTL的Transits的Petri网的模型检查器（完整版）
AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)
论文作者
论文摘要
网络的正确性通常是根据组件的各个数据流而不是其全球行为来描述的。在软件定义的网络中，指定数据包的正确行为比整个网络的全局行为要方便得多。带有过境的培养皿扩展了培养皿网，而流动-LTL扩展了LTL，以便可以跟踪令牌的数据流。我们将工具ADAMMC作为第一个具有针对Flow-LTL的petri网的模型检查器。我们描述了ADAMMC如何自动编码软件定义网络的同时更新为具有Transits的Petri网，以及如何在Flow-LTL中表达通用网络规格。基础ADAMMC是电路模型检查问题的减少。我们引入了一种新的还原方法，与以前的原型相比，该方法可改善性能。因此，ADAMMC可以处理具有多达82个开关的软件定义网络。
The correctness of networks is often described in terms of the individual data flow of components instead of their global behavior. In software-defined networks, it is far more convenient to specify the correct behavior of packets than the global behavior of the entire network. Petri nets with transits extend Petri nets and Flow-LTL extends LTL such that the data flows of tokens can be tracked. We present the tool AdamMC as the first model checker for Petri nets with transits against Flow-LTL. We describe how AdamMC can automatically encode concurrent updates of software-defined networks as Petri nets with transits and how common network specifications can be expressed in Flow-LTL. Underlying AdamMC is a reduction to a circuit model checking problem. We introduce a new reduction method that results in tremendous performance improvements compared to a previous prototype. Thereby, AdamMC can handle software-defined networks with up to 82 switches.
