利用SPIN实现对OpenFlow协议的形式化验证

扫码查看

原文链接

NETL
NSTL
万方数据
维普

中文摘要：为了验证OpenFlow网络中网络控制器NOX系统内典型应用程序Pyswitch的正确性,采用Promela语言对经简化的OpenFlow网络中的网络元素、连接通道及拓扑结构进行建模,并使用SPIN工具对所建模型进行形式化验证.结果表明,Pyswitch在主机不发生移动的情况下结果正确,但在主机发生移动情况下,会由于pyswitch的MAC地址学习算法存在设计缺陷而产生错误.

外文标题：The Formal Verification of OpenFlow Protocol using SPIN

作者：

石颖

展开 >

作者单位：

92723部队,北京100841

关键词：

OpenFlow网络 SPIN工具 Pyswitch程序建模形式化验证

出版年：

2014

计算机安全

信息产业部基础产品发展研究中心

计算机安全

影响因子：0.336

ISSN：1671-0428

年,卷(期)：2014.(3)

被引量2
参考文献量10