基于时间自动机的列控系统等级转换建模与验证  

Modeling and Verification of Train Control System Level Transition Based on Timed Automata

作　　者：董家希 刘珂帆 鄢春花 杜利芳 周家宇 Dong Jiaxi;Liu Kefan;Yan Chunhua;Du Lifang;Zhou Jiayu(School of Automotive and Transportation,Chengdu Technological University,Chengdu,China)

机构地区：[1]成都工业学院汽车与交通学院,四川成都

出　　处：《科学技术创新》2024年第6期21-24,共4页Scientific and Technological Innovation

基　　金：成都工业学院2022年校级科研项目《基于模型的列控系统测试用例生成关键技术研究》(2022ZR040);四川省大学生创新创业训练计划《碳零光明——无电源光导照明装置》(S202311116040X)。

摘　　要：随着列控系统的发展,我国现有铁路线路主要应用有CTCS-3级和CTCS-2级两种列控系统。等级转换是在列车运行控制过程中起到重要作用,其功能的正确性直接关系到列控系统的安全性。本文采用时间自动机建模方法,依据CTCS-3级列控系统总体基础方案的需求规范,对等级转换场景进行了功能性及实时性的需求分析,描述CTCS-3级和CTCS-2级列控系统转换过程中的功能特性和时间约束,对等级转换场景进行建模仿真,并通过形式化验证的方式检验模型的正确性。With the development of train control system,CTCS-3 and CTCS-2 train control systems are mainly used in China's existing railway lines.Level transition plays an important role in the process of train operation control,and the correctness of its function is directly related to the safety of the train control system.In this paper,the timed automata modeling method is used to analyze the functional and real-time requirements of the level conversion scenario according to the requirements specification of the overall basic scheme of CTCS-3 train control system.The functional characteristics and time constraints in the conversion process of CTCS-3 and CTCS-2 train control systems are described.The level conversion scenario is modeled and simulated,and the correctness of the model is verified by formal verification.

关 键 词：列控系统 等级转换 UPPAAL建模 时间自动机 

分 类 号：U284.48[交通运输工程—交通信息工程及控制]