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

作　　者：萨仁高娃[1] 

机构地区：[1]内蒙古师范大学计算机与信息工程学院,内蒙古呼和浩特010000

出　　处：《内蒙古科技与经济》2011年第17期82-83,87,共3页Inner Mongolia Science Technology & Economy

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

关 键 词：模型检测 形式化描述 协议验证 LDP协议 ASK—CTL 

分 类 号：TN915[电子电信—通信与信息系统]