IPv6协议簇中路由协议的正确性保证是下一代互联网研究的重要课题。一致性测试是一种有效地检验其实现正确性的方法。由于IPv6路由协议具有行为与消息相互依赖的特点，集成数据与控制的符号化一致性测试方法成为检验协议实现正确性的重要手段。但是现有的符号化测试只集中在简单数据表示，而且只注重符号测试生成阶段，考虑了状态空间问题，而忽略了符号的数据选择、执行和评价问题，从而避开了由于符号选择所造成的数据空间爆炸问题。针对上面存在的问题，本文提出了统一的符号化测试方法，涵盖了从符号建模、符号化一致性关系、符号测试生成、符号数据选择、符号测试套选择到符号执行系统的全过程，并且在IPv6协议簇上取得了较好的测试效果。　　 该方法的出发点是建立描述协议规范的形式化模型。数据域模型的引入是为了描述路由协议中复杂的路由消息，不仅包括消息的表示，而且定义了消息上的操作算子。把数据域模型与标记变迁系统相结合提出了描述路由协议规范的标记变迁图模型，但它也适应于复杂协议建模。标记变迁图可以充分满足协议对数据与行为集成的需要，同时使得所产生的测试套覆盖度更高。　　 在符号变迁图模型的基础上，提出了符号化一致性关系并且给出了该一致性关系的形式化描述。该一致性关系定义了被测实现与协议规范是否一致的标准，并且指导测试生成，所以具有核心的作用。　　 根据符号化一致性关系，提出了符号化测试生成算法。该算法可以生成所有满足一致性关系的符号测试套。该算法采用了图论中的最小强连通理论、on-the-fly技术与测试目的策略，有效地裁剪了无用的分支，从而生成了满足覆盖性要求的符号测试套，同时避免了状态空间爆炸问题。　　 符号测试套在执行前，都需要经过数据选择，把符号转化为具体的消息数据。本文提出了一种基于贝叶斯学习的聚类方法，获得了数据的概率分布，通过选择概率大的数据进行实例化可以得到覆盖度和质量更高的测试套。　　 本文提出了一种基于假设检验的方法来选择更可用的测试套，如果测试例的执行结果落入协议规范确定的接受域，就认为是可以接受的；否则就是被拒绝的。这样就改善了符号测试套中的冗余性和可用性问题。　　 对于路由协议中的一些静态规则，如果人工检验是很困难的。本文提出了一种数据挖掘的方法，使用关联规则挖掘方法来检验协议中的静态规则。可以提高静态规则检验的效率。　　 本文实现了一个IPv6协议簇的符号执行系统，该系统不仅支持符号测试的执行，而且可以自动配置被测实现，极大地提高了测试执行的效率。　　 上述形式化方法在IPv6协议簇的路由协议测试中取得非常好的效果，并且所有测试例都已转化为商业运行版本。