Modeling and verification of time constraints of operation scenarios of high-speed train control system

The high-speed train control system is a typical distributed real-time system, in which time constraints are mainly focused on the operation scenarios between subsystems. The extension of the temporal logic can not meet all needs of describing the properties of the distributed real-time system. The scenarios of the train control system are often described in terms of the deadline, time-out and wait until and so on. Insufficiency exists in the above formal descriptions and also in verification along with intensification of the complexity of the system. In this paper, the modeling and verification methods suitable for the scenarios of the train control system are introduced. Firstly, HCSP is used to model the distributed real-time system. Secondly, the HCSP models are transformed to the TA models according to transition rules. Finally, automatic verification is accomplished with the checking tool UPPAAL. The effectiveness of the proposed modeling and verification methods are proved through simulation and analysis of RBC handover scenarios.