近年来，随着网络变得越来越复杂化，成千上万网络设备以不同的方式来修改和转发数据包，执行复杂的网络功能，并导致了网络的易错。网络验证与测试领域已经越来越受到学术界的关注。当前的网络急速发展，互联网应用，互联网服务急速增长，变的越来越复杂，对网络的要求也同时越来越高，网络也需要发展来适应当前环境的需要。软件定义网络(SDN)革新了传统网络，将传统网络中的控制层和数据层解耦，使得整个网络可以集中式控制并编程，这简化了网络管理，也进一步推动了整个网络验证领域的发展。在数据层验证与测试上，SDN使得实时网络数据层验证与测试更为方便与可行的同时，也要求数据层验证与测试更高的实时更新处理效率。当前的研究在实时验证与测试的实时更新效率上都有着瓶颈，并且难以扩展到多域或者多层级SDN网络中去。本文首先提出了基于多终端二进制决策图(MTBDD)的预处理工具PreChecker，在高效动态划分等价类的同时，检测消除规则间的冲突，结合基于等价类的网络验证方法，使其更新效率进一步提高。其次，将MTBDD结构的头空间等价类动态划分方法引入到数据层测试中，提高了动态测试数据包生成效率。另外，本文设计了一个基于头空间的网络模型框架，并设计了规则变化时的动态更新算法，动态维持网络的可达性信息并检测要求的可达性不变量，并提出了验证工具NetV，提高了实时更新性能。最后，将各项常规的域内网络不变量映射到框架上，使用NetV动态检测满足性，并将框架进一步推广到域间检测中去，进一步提高了域间不变量检测的性能，并易于扩展到多层级SDN网络。本文的主要研究内容和贡献如下：
　　1)重新使用行为集定义了交换机内部的冲突，引入了SDN网络的行为集定义冲突，避免了伪冲突。基于MTBDD结构，提出了头空间等价类动态划分方法，设计了代表等价类的终端节点的结构和计算，有效维护划分的等价类的同时，动态检测规则冲突。整合实现提出PreChecker工具，作为网络数据层验证预处理结合到网络验证方法中去，提高了当前基于等价类的数据层验证方法的动态性能。
　　2)将MTBDD结构的头空间等价类动态划分方法引入到数据层测试中，进一步将数据层测试数据包的要求定义为特定的等价类，并且设计MTBDD的终端结构，和终端间计算方法，使得可以使用MTBDD快速划分，并且支持动态划分生成测试数据包，提高了当前测试数据包生成方法的动态性能。
　　3)基于头空间基础，定义了网络模型，首次定义了网络行为函数间复合的具体计算过程，而不是仅作用在数据包头上，支持使用代数计算的方式复合来描述规则之间的连通。设计了规则行为作用在二进制决策图(BDD)结构上的算法，使BDD描述能运用在规则函数间的复合上来规避通配符描述头空间带来的歧义和描述式数量爆发的问题。基于BDD描述的优势，结合MTBDD头空间等价类划分方法，合并了冗余规则，减少了整体规模和计算量。使用矩阵来描述建模整网规则的连通性，使规则的合并和复合更加直观可推导，并在矩阵模型上，提出增量更新方法并设计了算法，利用增量方式来验证网络的可达性，提高了动态验证可达性的性能。整合实现提出NetV工具，利用此模型维持所有合并规则的连通性，在规则动态变化的同时验证整网的可达性要求是否被满足，同时也可以实时进行可达性查询。
　　4)基于NetV模型推导得出各项的域内网络不变量在矩阵模型上的等价描述，使用NetV，在规则更新过程中，使用增量更新方法来验证其他域内网络不变量。进一步推广整个模型到域间多层控制器，并建立域间网络模型，使得域内具体规则信息被隐藏，一个域可以作为黑盒提供输入和输出间的简化的规则函数对应关系。使用增量更新的方式来检测域间不变量，使得域间的网络不变量检测和域内的网络不变量检测保持其一致性，并提高了域间不变量检测的性能，并易于扩展到多域或者多层级SDN网络中。