¹State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044，China
²National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing, China

---

Abstract—Chinese Train Control System level three (CTCS- 3) is a major technical system in Chinese high-speed rail and Train Control System (TCC) is indispensable component in the CTCS-3. Current researches on TCC are mainly based on the simulation, which cannot ensure that all conditions in TCC are tested. This paper presents a hierarchical modeling method and uses time automation (TA) to model the TCC software. We take the design of the active balise telegram editing, a major part in the TCC software, as an example. At first, the process of the active balise telegram editing is analyzed to obtain a hierarchical diagram containing several layers. Then, TA is employed to build one TA model for each layer. Lastly, we use UPPAAL (a model validation tool, developed by Uppsala University and Aalborg University) to construct a network of the TA models to verify the active balise telegram editing. The verification results demonstrate that this modeling method is feasible and the model can meet the functional requirements of the TCC software.

Index Terms—TCC Software, Time Automation, UPPAAL, Hierarchical Modeling

[PDF]

Cite: Lei Yuan, Shiying Yang, Dewang Chen, Kaicheng Li, "Hierarchical Modeling and Verification for Highspeed Train Control Center by Time Automation," Journal of Software vol. 9, no. 6, pp. 1553-1560, 2014.