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

摘要

无线闭塞中心等级转换场景作为中国列车运行控制系统主要场景之一,切换成功与否直接影响高速列车的安全和运行效率。通过对形式化验证方法的分析,采用基于定理证明的时间化工业软件工程规范语言的严格方法( Timed Rigorous Approach to Industrial Software Engineering Specification Language,TRSL),在对等级转换过程进行分析的基础上,设计交互信息图,构建状态迁移图,并结合域建模方法实现对该场景的TRSL描述,最后利用语言推理规则,结合系统特性,实现对切换正确性和实时性的双重验证,结果表明：该场景满足系统规范对功能性和实时性的要求,继而说明该方法的有效性、正确性和通用性,为我国列控系统的设计开发和验证提供一种新的途径和依据。%As a main scene of the Chinese Train Control System, RBC ( Radio Block Center ) level transition scene, whether it can switch successfully, will directly affect high-speed train operating efficiency and safety. By analyzing the formal verification method, the method of time-based industrial software engineering specification language of theorem proving ( Timed Rigorous Approach to Industrial Software Engineering Specification Language,TRSL) is selected. On the basis of the analysis of level transition process, interactive information figure is designed, state transition diagram is constructed, TRSL descriptions of the scene are implemented combined with domain modeling method, and finally the double verification of interaction correctness and real-time capability is fulfilled by means of inference rules and associated system features. The results show the consistence of the scene with system specifications in terms of functionality and instantaneity, and demonstrate the effectiveness, accuracy and versatility of the method, which may provide a new way and basis for the design, development and validation of train control system.