Formal modeling and verification of CTCS-3 train control on-board equipment
Article
Figures
Metrics
Preview PDF
Reference
Related
Cited by
Materials
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.
Keywords:
Project Supported:
Supported by National Natural Science Foundation of China(U2268206).
