随着网络通信技术的高速发展,网络协议标准也不断地更新和完善。如何更有效地保证网络协议的实现质量,已成为网络协议工程领域的关键问题之一。实践证明,以合理有效的方式将形式化方法应用于协议研发实践中,可以有效提高协议设计、实现、测试的效率,最大程度地保证协议实现的正确性。协议一致性测试用于检查协议实现是否符合协议设计的要求,是保障协议实现质量的有效方法。HMIPv6协议作为移动IPv6协议的优化,在行为特性、安全性等方面采用了新的技术。如何借助于形式化方法对此协议进行有效的一致性测试成为亟待解决的问题。本文采用Coloured Petri Nets对HMIPv6协议进行形式化建模,并且使用了层次化的建模方法,将HMIPv6协议按节点类型抽象成若干层,层次化的模型不但更能体现不同节点间的交互属性,而且由于层次间的相对独立性,使得模型的开发更加模块化。此类通信协议的特点是并发度较高,且交互行为较多,Coloured Petri Nets非常适合于描述具有这些特点的系统。CPN tools还支持模型相关性质的分析,从而保证了模型的正确性。在一致性测试方法上,本文提出了由协议属性指导的测试例生成。文中对属性也采用Coloured Petri Nets进行形式化描述,给出了基于属性的测试例生成算法。该算法使得测试例的生成过程简单,直接,且针对性强。算法的提出使得测试例自动生成成为可能,本文作者开发了基于CPNs的测试例生成工具,重点实现了本文提出的属性指导的测试例生成算法,实现了测试例生成的自动化,取得了良好的测试效果。