1.兰州交通大学，自动化与电气工程学院，兰州 730070;2.兰州交通大学，甘肃省工业交通自动化工程技术研究中心，兰州 730070
何涛（1977—），男，教授，硕导，主要从事轨道交通测试研究方向研究。
韩敬佳（1994—），女，硕士，主要从事列控系统建模分析方向研究，（E-mail）1558155326@qq.com。
国家自然科学基金资助项目(U2268206)。
1.School of Automation and Electrical Engineering, Lanzhou JiaoTong University, Lanzhou 730070, P. R. China;2.Gansu Research Center of Automation Engineering Technology for Industry &Transportation, Lanzhou JiaoTong University, Lanzhou 730070, P. R. China
Supported by National Natural Science Foundation of China(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.
何涛,韩敬佳.
