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

作     者：谢雨飞 唐涛 徐田华 赵林 XIE Yu-fei;TANG Tao;XU Tian-hua;ZHAO Lin

作者机构：北京交通大学轨道交通控制与安全国家重点实验室北京100044 

出 版 物：《铁道学报》 (Journal of the China Railway Society)

年 卷 期：2011年第33卷第7期

页      面：67-72页

核心收录：

学科分类：08[工学] 082302[工学-交通信息工程及控制] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 0823[工学-交通运输工程] 

基　　金：国家自然科学基金资助项目(60634010) 轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005) 

主　　题：CTCS-3级列控系统 系统规范 建模 形式化验证 

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