论文标题
软件定义网络的正式建模和验证
Formal Modelling and Verification of Software Defined Network
论文作者
论文摘要
在云计算中，软件定义的网络（SDN）由于其在网络配置方面的优势而引起了更多关注，以提高网络性能和网络监视。 SDN通过允许对网络系统的集中控制来解决传统网络中静态体系结构的问题。 SDN包含集中式网络智能模块，该模块将转发数据包（数据平面）的过程与数据包路由过程（控制平面）分开。由于安全数据传输的安全数据，必须确保SDN的正确性。在本文中。选择模型检查以验证SDN网络。计算树逻辑（CTL）和线性时间逻辑（LTL）用作表达SDN属性的规范。然后，完整的SDN结构与其Kripke结构一起正式定义。最后，针对SDN Kripke模型分析时间属性，以确保SDN的性质是正确的。
In cloud computing, software-defined network (SDN) gaining more attention due to its advantages in network configuration to improve network performance and network monitoring. SDN addresses an issue of static architecture in traditional networks by allowing centralised control of a network system. SDN contains centralised network intelligence module which separates a process of forwarding packets (data plane) from packet routing process (control plane). It is essential to ensure the correctness of SDN due to secure data transmitting in it. In this paper. Model-checking is chosen to verify an SDN network. The Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) used as a specification to express properties of an SDN. Then complete SDN structure is defined formally along with its Kripke structure. Finally, temporal properties are analysed against the SDN Kripke model to assure the properties of SDN is correct.
