陈永刚，丁春平

(兰州交通大学自动化与电气工程学院，兰州　730070)



基于TRSL的RBC等级转换场景研究

陈永刚，丁春平

(兰州交通大学自动化与电气工程学院，兰州730070)

无线闭塞中心等级转换场景作为中国列车运行控制系统主要场景之一，切换成功与否直接影响高速列车的安全和运行效率。通过对形式化验证方法的分析，采用基于定理证明的时间化工业软件工程规范语言的严格方法(Timed Rigorous Approach to Industrial Software Engineering Specification Language，TRSL)，在对等级转换过程进行分析的基础上，设计交互信息图，构建状态迁移图，并结合域建模方法实现对该场景的TRSL描述，最后利用语言推理规则，结合系统特性，实现对切换正确性和实时性的双重验证，结果表明：该场景满足系统规范对功能性和实时性的要求，继而说明该方法的有效性、正确性和通用性，为我国列控系统的设计开发和验证提供一种新的途径和依据。

列车运行控制系统；RBC等级转换；TRSL；场景切换正确性

为保证高速列车安全、高效地运行，我国铁路部门在参照欧洲列车控制系统的基础上，研发了满足我国铁路线路的中国列车运行控制系统(Chinese Train Control System，CTCS)[1]。CTCS-3级列控系统具有分布式结构、连续式响应、实时性强的特性，如何选取有效而又合适的方法来实现系统特性的描述和验证，已成为高铁列控系统研究领域中的重要研究内容。目前，一般通过3种手段：仿真、测试以及最具严格性的形式化方法来验证系统特性，由于前两者的代价昂贵、花费时长，而且只能在系统投入前处理典型情况，无法实现状态、路径的穷举遍历[2]，针对安全苛求系统，采用形式化方法不仅可实现更严谨的系统描述和验证，而且可避免以上方法的不足[3，4]。……