¹State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China
²Scheduling and Control Group, Centre for Industrial and Applied Mathematics, University of South Australia, Mawson Lakes 5095, Australia

---

Abstract—The correct implementation of Train Control Center (TCC) software has great significance on the safe operation of high-speed railways. There are some problems in the currently used timed automata (TA) method for modeling TCC software, such as subjectivity and uncertainty in the modeling. In order to better verify the features of TCC software, this paper presents a new modeling method which combines Unified Modeling Language (UML) and Timed Automata (TA). As track circuit encoding function is a key function in TCC software, this paper takes it as an example to show the effectiveness of the proposed modeling method. Firstly, the UML class diagrams and state diagrams of TCC software were established based on the detailed analysis on TCC software. Secondly, the TA models are built according to the corresponding rules between UML and TA model. Finally, TA models were simulated and validated in the validation tool, UPPAAL. The simulation results show that TCC software can meets its functional requirements and performance requirements.

Index Terms—TCC software, timed automata, UML, UPPAAL, track circuit encoding

[PDF]

Cite: Lei Yuan, Lijuan Wang, Dewang Chen, Amie Albrecht, "Modeling and Verification for Track Circuit Encoding in Train Control Center Based on UML and TA," Journal of Software vol. 9, no. 10, pp. 2693-2698, 2014.