doi: 10.4304/jsw.9.10.2693-2698
Modeling and Verification for Track Circuit Encoding in Train Control Center Based on UML and TA
- 1 State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China
- 2 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.
Keywords
- TCC software
- timed automata
- UML
- UPPAA
How to Cite
Lei Yuan, Lijuan Wang, Dewang Chen, and 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. https://doi.org/ 10.4304/jsw.9.10.2693-2698
Copyright & License
Copyright © 2014 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).