LDP标记分发协议的模型检查

为了验证LDP协议特定模式下的标记分发过程能否正常进行，使用CPNTools工具对LDP标记分发协议进行了抽象、建模分析，设计了相应的CPN模型，基于协议模型模拟和分析LDP协议标记分发机理，得到协议模型的状态空间统计信息。根据CPN模型检测理论，使用分支时序逻辑ASK—CTL公式进一步证明了协议在特定工作模式下能够按照协议规格说明分发标记，标记分发过程是正确的。