CTCS-3级列控系统规范的建模与形式化验证方法研究

• 作者: 唐涛 徐田华 谢雨飞 赵林
• 来源期刊: 铁道学报
• 学科: 交通运输
• 关键词: CTCS-3级列控系统 系统规范 建模 形式化验证
• 年，卷（期）: 2011,（7）
• 所属期刊栏目: 铁道通信信号
• 页码范围: 67-72
• 分类号: TP301|U284.48
• 字数: 4778字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2011.07.011

摘要

CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节.然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验证显得十分必要.本文提出CTCS-3级列控系统规范建模与形式化验证方法,此方法的特点是能够在系统规范、模型、验证工具以及验证结果之间建立一条跟踪链,从而始终保证系统规范、模型及程序代码之间的一致性.结合笔者运用此方法对CTCS-3级列控系统规范建模与形式化验证的实践,证明这种方法是可行的、高效的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
2	徐田华	北京交通大学轨道交通控制与安全国家重点实验室	21	347	11.0	18.0
3	赵林	北京交通大学轨道交通控制与安全国家重点实验室	11	160	8.0	11.0
4	谢雨飞	北京交通大学轨道交通控制与安全国家重点实验室	3	41	2.0	3.0