Abstract: The C3+ATO system is in the experimental stage in our country and has the characteristics of high automation degree and high safety requirement at present. In order to confirm whether the specific function of the high-speed railway C3+ATO system meets the corresponding technical specification under the specific scene, a formal modeling and verification method based on the timed automata is proposed. The station automatic departure scene is selected as the modeling object. The functional requirements of C3+ATO system specification are extracted and the timed automata model of the scene is established. The message sequence chart of the corresponding process is generated, and the functional attributes of the system are verified and the model is simulated at the C3+ATO train control simulation platform. The simulation results show that the model meets the security function attributes and restricted activity attributes of the system technical specification, and can provide theoretical reference for the system design, practical application and improvement of related specifications.

Key words: C3+ATO system, timed automata, UPPAAL, station automatic departure, message sequence chart