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

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

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

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.