Modeling and Verification for Track Circuit Encoding in Train Control Center Based on UML and TA

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