软件定义网络的形式化建模与验证
软件工程
2020-04-10 v1
摘要
在云计算中，软件定义网络（SDN）因其在网络配置方面提升网络性能与网络监控的优势而受到更多关注。SDN 通过允许对网络系统集中控制，解决了传统网络中静态架构的问题。SDN 包含集中式网络智能模块，该模块将转发数据包的过程（数据平面）与数据包路由过程（控制平面）分离。由于其中数据传输的安全性，确保 SDN 的正确性至关重要。在本文中，选用模型检测来验证 SDN 网络。计算树逻辑（CTL）与线性时态逻辑（LTL）被用作表达 SDN 属性的规约。随后正式定义了完整的 SDN 结构及其 Kripke 结构。最后，针对 SDN Kripke 模型分析时态属性，以确信 SDN 的属性正确。
引用
@article{arxiv.2004.04425,
title = {Formal Modelling and Verification of Software Defined Network},
author = {Jnanamurthy H K and Vijay Varadharajan},
journal= {arXiv preprint arXiv:2004.04425},
year = {2020}
}