CTCS-3级列控车载设备的形式化建模与验证
作者:
作者单位:

1.兰州交通大学,自动化与电气工程学院,兰州 730070;2.兰州交通大学,甘肃省工业交通自动化工程技术研究中心,兰州 730070

作者简介:

何涛(1977—),男,教授,硕导,主要从事轨道交通测试研究方向研究。

通讯作者:

韩敬佳(1994—),女,硕士,主要从事列控系统建模分析方向研究,(E-mail)1558155326@qq.com。

中图分类号:

基金项目:

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


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

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

Fund Project:

Supported by National Natural Science Foundation of China(U2268206).

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    CTCS-3级列控系统安全苛求性较高,而列控车载设备是CTCS-3级列控系统的主体,主要功能是对列车进行操纵和控制,保证列车安全运行的关键。通过分析CTCS-3级列控车载设备之间的信息交互以及车载安全计算机中工作模式的转换规则,采用有色Petri网(CPN)建立车载设备的信息交互模型以及工作模式转换模型,使用ASK-CTL分支时序逻辑公式验证了模型的死标识、死锁以及分析工作模式下的系统行为等特性,验证构建的CPN模型符合系统规范要求的流程及规则,可为相关安全苛求系统的设计提供一定参考。

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

何涛,韩敬佳.CTCS-3级列控车载设备的形式化建模与验证[J].重庆大学学报,2023,46(9):120-129.

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2020-06-09
  • 最后修改日期:
  • 录用日期:
  • 在线发布日期: 2023-09-25
  • 出版日期: