doi: 10.4304/jsw.9.6.1553-1560
Hierarchical Modeling and Verification for Highspeed Train Control Center by Time Automation
- 1 State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044，China
- 2 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.
Keywords
- TCC Software
- Time Automation
- UPPAAL
- H
How to Cite
Lei Yuan, Shiying Yang, Dewang Chen, and 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. https://doi.org/ 10.4304/jsw.9.6.1553-1560
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).