网络协议具有空间分布性、并发性和异步性,这些特性对网络协议的开发质量带来了巨大挑战。协议化验证是对协议的功能和性能进行校验过程,是保证协议开发质量的必要环节。协议形式’验证的前提是协议行为以及协议性质的形式描述。协议的行为可通过形式模型或者形式语言进行描述,而协议性质的描述方式是系统断言语言,如CTL、ASK-CTL等。模型检查作为一种形式化验证方法,能够自动验证一个系统是否满足设计规范,近年来被广泛应用于软硬件、协议验证中。通过协议模型,可以从整体上、宏观上把握协议,更早的发现问题或疏漏的地方。而且协议模型为协议实现代码生成提供依据,允许详细说明协议的结构或行为,给出了一个指导构造协议实现系统的模板。MPLS(MultiRotocol Label Switching,多协议标记交换)技术是随着Internet的发展而涌现出来的网络新技术中的一种。MPLS利用简单的定长的标记来转发分组,将传统网络层中复杂、灵活的路由协议与数据链路层便宜高速的交换硬件很好地结合起来。LDP (Label Distribution Protocol,标记分发协议)是为标记分发而专门制定的新协议,使用LDP可以实现MPLS中标记分发功能。论文首先使用CPN Tools工具设计和实现了LDP协议特定模式下的CPN(Colored Petri Net,着色Petri网)模型。然后使用CPN Tools的状态空间工具模拟得到了协议分析报告。最后在协议分析报告的基础上结合使用分支时序逻辑ASK-CTL公式进一步验证了LDP协议特定工作模式下能够正确建立标记交换路径LSP,其标记分发过程是正确的,协议模型的所有库所都是有界的,变迁都是公平的,存在两个死标识是协议正常的两种终结点。