Formal modeling and verification of CTCS-3 train control on-board equipment
CSTR:
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

Clc Number:

Fund Project:

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

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Related Videos

Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:June 09,2020
  • Revised:
  • Adopted:
  • Online: September 25,2023
  • Published:
Article QR Code