With the development of train control system,CTCS-3 and CTCS-2 train control systems are mainly used in China's existing railway lines.Level transition plays an important role in the process of train operation control,and the correctness of its function is directly related to the safety of the train control sys-tem.In this paper,the timed automata modeling method is used to analyze the functional and real-time re-quirements of the level conversion scenario according to the requirements specification of the overall basic scheme of CTCS-3 train control system.The functional characteristics and time constraints in the conversion process of CTCS-3 and CTCS-2 train control systems are described.The level conversion scenario is modeled and simulated,and the correctness of the model is verified by formal verification.
关键词
列控系统/等级转换/UPPAAL建模/时间自动机
Key words
train control system/level conversion/UPPAAL modelling/timed automata
维普
万方数据