伴随“互联网+”概念的提出，信息化在社会生产生活中起到的重要作用日益深入人心。其中网络作为促进信息流通的重要载体与具体手段，扮演着核心角色。随着新的网络范型不断出现，网络维度由最初的陆基网络扩展到了海基网络、空基网络以及天基网络。网络在越来越重要的同时，其具体表现形态变的越来越复杂。因此，如何持续保证底层网络的正确性，为上层应用提供可靠性保障，不仅在网络工程、网络运维中占有重要地位，在网络理论的学术研究中也日益凸显其地位。
　　论文针对软件定义网络环境下基于状态的网络测试与网络不变式验证进行研究，具体包含三部分工作，分别是软件定义网络环境下网络协议状态的研究、网络行为形式化建模以及生成路径序列的研究、基于路径矩阵的网络不变式验证的研究。通过网络协议状态的研究可以得到整体网络状态，在其指导下开展基于约束的形式化建模，并得到路径序列，继而构建路径矩阵，并对OpenFlow协议进行测试。在路径矩阵的指导下进行网络不变式验证，判断底层网络行为是否正确或与用户需求是否保持一致。
　　论文基于软件定义网络控制器Floodlight，扩充其相应代码模块，实现了网络不变式的验证功能。论文的主要工作和创新性成果如下：
　　1.提出网络全局状态视图定义并给出了状态视图栈扩充算法
　　本文按照因特网网络体系结构，对网络状态按照层次进行分析，提出网络状态统一视图和网络状态视图栈的概念以及形式化定义。结合上述概念提出网络全局状态视图构建算法以及网络状态视图栈扩充等算法，并以网络中的“敲门”应用为例说明了上述视图以及视图栈的应用，由此说明了上述扩充算法的一般性。逻辑上来说，可以全方位对网络状态进行分析，不断扩充该状态视图栈，在软件定义网络环境下为网络应用提供坚实的底层状态数据保障。
　　2.提出基于约束的序列生成算法，使模型更加贴合现实
　　基于关注的问题构建网络模型，后续研究依托模型展开，相应的验证、测试也是基于构建的模型进行，是网络研究中的重要手段。因此如何更好的构建网络模型，使得模型的建立与生产生活的具体需要贴合更紧密，是网络研究中需要着重探讨的问题。本文提出基于约束的序列生成算法，在所建立的网络模型中加入约束信息，并根据反馈不断修正上述约束，使得网络模型与具体场景拟合更加紧密。然后以OpenFlow协议为例说明了上述基于约束构建网络模型的有效性，并针对OpenFlow协议进行了测试，基于形式化的指导提出了一个测试系统框架，并编程实现上述框架，扩充该框架使其支持不同的测试方法。
　　3.提出基于路径矩阵的网络不变式验证算法
　　提出网络不变式的一般性形式化定义，并结合网络不变式验证流程，提出基于路径矩阵的网络不变式验证算法，针对常见网络场景中涉及到的网络不变式给出其具体定义，并利用不变式验证算法实现上述不变式验证。在软件定义网络环境下，针对网络转发循环不变式、网络黑洞不变式、网络多路径一致优先级不变式、网络可达不变式、网络隔离不变式、网络路径不相交不变式以及网络有界性不变式等属性开展了不变式验证过程，得到了有益的结论，证明了本文不变式验证算法的有效性。
　　本文在软件定义网络环境下，结合开源控制器Floodlight，在通读其源码的基础上扩充了相应功能模块，增加了相应形式化建模功能模块。整合基于约束的建模过程，构建网络全局状态视图以及状态视图栈，服务于网络上层应用。本文建立了开放易扩展的底层数据结构，逻辑上在传统的软件定义网络中构建验证与测试平面，对网络运行状态进行不间断验证，保证底层网络的正确性。