概率模型检验的CBTC系统通信协议的形式化验证
谢雨飞
徐田华
唐涛
1.北京交通大学轨道交通控制与安全国家重点实验室,北京,1000442.北京交通大学轨道交通控制与安全国家重点实验室,北京,1000443.北京交通大学轨道交通控制与安全国家重点实验室,北京,100044
摘要：通信协议是CBTC系统重要的组成部分,它的正确性、稳定性和安全性对整个CBTC系统有重要影响.鉴于通信协议中某些参数具有随机特征,本文采用概率模型检验对其进行形式化验证.分析了概率模型检验的语义及语法,建立了通信协议的概率模型,用概率模型检验工具PRISM验证了典型的概率规范.结果证明,当信道正常概率为99%,系统无延时概率为99%时,通信协议失效率小于1.5×1010.说明了用概率模型检验验证具有随机特征参数的通信协议,方法简单快捷,结论清晰明了.
关键词：CBTC系统通信协议概率模型检验形式化验证
分类号：U238.2(特种铁路)TP301(计算技术、计算机技术)
资助基金：国家自然科学基金(60634010)
论文发表日期：2009-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：5( 35-39 )
英文信息