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

Research on Method of Modeling and Formal Verification of the CTCS-3 Train Control System Specification

作　　者：谢雨飞[1] 唐涛[1] 徐田华[1] 赵林[1] 

机构地区：[1]北京交通大学轨道交通控制与安全国家重点实验室,北京100044

出　　处：《铁道学报》2011年第7期67-72,共6页Journal of the China Railway Society

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

摘　　要：CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节。然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验证显得十分必要。本文提出CTCS-3级列控系统规范建模与形式化验证方法,此方法的特点是能够在系统规范、模型、验证工具以及验证结果之间建立一条跟踪链,从而始终保证系统规范、模型及程序代码之间的一致性。结合笔者运用此方法对CTCS-3级列控系统规范建模与形式化验证的实践,证明这种方法是可行的、高效的。The specifications of the CTCS-3 train control system is the basis of design and development of the CTCS-3 train control system,and it is crucial for realization of good interoperability and high efficiency and security of the system.However,specifications compiled by experience or intuitive thought inevitably bring about defects or hidden dangers.So it is necessary to carry out modeling and formal verification of the system specifications.The paper proposes the method of modeling and formal verification of the CTCS-3 train control system specifications.The method establishes a track chain of the system specifications,model,model checking tools and verification results so as to ensure the consistency of the system specifications,models and program codes.Our practice has proved that this method is feasible and efficient.

关 键 词：CTCS-3级列控系统 系统规范 建模 形式化验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构] U284.48[自动化与计算机技术—计算机科学与技术]