层次移动IPv6 (Hierachical Mobile IPv6, HMIPv6)是在MIPv6(移动IPv6)的基础上针对MN(移动结点)在小范围内快速移动所作出的一种改进技术。HMIPv6针对MIPv6将全局性的大范围移动与一个区域内的小范围的移动都用一种方式处理,对移动结点MN在小范围内快速移动切换时更新报文频繁问题提出了解决方法。HMIPv6对网络进行了层次化的划分,HMIPv6在每个区域内引入了一个新的实体——移动锚点(MAP),使得移动结点的移动分为“宏移动”和“微移动”两种情况,改进了最基本的MIPv6切换方案,减少了移动过程中的丢包率和传输延时,提高了通信质量。对HMIPv6进行形式化验证不仅可以给出协议的一种形式化的规范描述,并且可以为后续协议改进提供了基础模型,便于协议改进的分析,并为软件的实现提供了可信性保障。本文采用“基于事件”的分析方法对HMIPv6协议进行属性提取,并采用了层次化方法和“通用模块”思想,构建了着色Petri网(Color Petri Nets, CPN)的层次化模型,最后使用集成分析方法,采用了模拟执行、状态空间报告、全状态空间分析、ASKCTL模型检验确认模型满足协议要求。本文中使用的CPN采用图形语言和有效的形式化模型的组合,可以直观的模拟执行,并且在描述复杂数据,层次化建模、并发、通信、同步中方面都有较强的优势。