概率模型检验的CBTC系统通信协议的形式化验证

• 来源期刊: 北京交通大学学报
• 学科: 交通运输
• 关键词: CBTC系统 通信协议 概率模型检验 形式化验证
• 年，卷（期）: 2009,（5）
• 所属期刊栏目: 电子信息通信工程
• 页码范围: 35-39
• 页数: 5页
• 分类号: U238.2|TP301
• 字数: 3147字
• 语种: 中文

摘要

通信协议是CBTC系统重要的组成部分,它的正确性、稳定性和安全性对整个CBTC系统有重要影响.鉴于通信协议中某些参数具有随机特征,本文采用概率模型检验对其进行形式化验证.分析了概率模型检验的语义及语法,建立了通信协议的概率模型,用概率模型检验工具PRISM验证了典型的概率规范.结果证明,当信道正常概率为99%,系统无延时概率为99%时,通信协议失效率小于1.5×1010.说明了用概率模型检验验证具有随机特征参数的通信协议,方法简单快捷,结论清晰明了.