CTCS-3 级列控车载设备的形式化建模与验证  

Formal modeling and verification of CTCS-3 train control on board equipment

作　　者：何涛[1,2] 韩敬佳 HE Tao;HAN Jingjia(School of Automation and Electrical Engineering,Lanzhou JiaoTong University,Lanzhou 730070,P.R.China;Gansu Research Center of Automation Engineering Technology for Industry&Transportation,Lanzhou JiaoTong University,Lanzhou 730070,P.R.China)

机构地区：[1]兰州交通大学自动化与电气工程学院,兰州730070 [2]兰州交通大学甘肃省工业交通自动化工程技术研究中心,兰州730070

出　　处：《重庆大学学报》2023年第9期120-129,共10页Journal of Chongqing University

基　　金：国家自然科学基金资助项目(U2268206)。

摘　　要：CTCS-3级列控系统安全苛求性较高,而列控车载设备是CTCS-3级列控系统的主体,主要功能是对列车进行操纵和控制,保证列车安全运行的关键。通过分析CTCS-3级列控车载设备之间的信息交互以及车载安全计算机中工作模式的转换规则,采用有色Petri网(CPN)建立车载设备的信息交互模型以及工作模式转换模型,使用ASK-CTL分支时序逻辑公式验证了模型的死标识、死锁以及分析工作模式下的系统行为等特性,验证构建的CPN模型符合系统规范要求的流程及规则,可为相关安全苛求系统的设计提供一定参考。The CTCS-3 train control system is subject to stringent safety requirements,with the train control on-board equipment serving as its core.This equipment plays a vital role in operating and controlling the train,ensuring the overall safety of train operation.In this study,the information interaction between CTCS-3 train control on-board devices and the work mode conversion rules in the on-boar safety computer was analyzed.To establish a comprehensive model,colored Petri nets(CPN)were used,enabling the construction of an information interaction model and work mode transformation model for the on-board equipment.To validate the model’s effectiveness,the ASK-CTL branching sequence logic formula was used to verify its performance concerning dead identification,deadlock and transferability under various working modes.The results show that the CPN model conforms to the system specification requirements,adhering to the expected process and rules.This research provides valuable ingishgts and serves as a reference for the design of the relevant security demanding systems.

关 键 词：列控系统 车载设备 模式转换 有色PETRI网 

分 类 号：TP391[自动化与计算机技术—计算机应用技术] U284[自动化与计算机技术—计算机科学与技术]