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

摘要

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