The Verification of Temporary Speed Restriction of Train Control System Based on Timed Automata

Temporary speed restriction (TSR) refers to the speed restriction within given time bounds beyond the required speed restriction by the lines. TSR system is a typical real-time system. There are strict logical order relations and precise time constraints for the settings, execution, confirmation and cancel of TSR command. So it is important to ensure real-time performance of TSR system. In this paper we focused on the verification of the existing specification of the TSR system of Chinese Train Control System (CTCS) which was used in high-speed railway. We expected to find some imperfections of the working process or the configuration parameters of TSR system. Therefore, a model of the timed automata for the working process of the TSR system was established on the basis of the specification which was published by the administrator of the railway. UPPAAL verification tool was applied to verify the safety and bounded liveness properties of TSR system. The result of the verification showed that some time-related configuration parameters cannot achieve real-time requirements in the existing technical specifications. We also recommended how to correct this imperfection. It showed that the modeling and verification methods we proposed can be useful to study real-time performance of train control system of high-speed railway.