关键词: CTCS-1级列控系统, 等级转换场景, NuSMV模型, 模型验证

Abstract: With the development of key technologies of the CTCS-1 train control system, it is inevitable that the trains carrying CTCS-1 control system will run across to the CTCS-0 level line, and the smooth implementation of the system level transition is the basis for safe cross-line operations. Based on the system function analysis, a multi-resolution function model is established to identify the scenario requirement of level transition. According to the scenario requirement and the exsisting system specifications, the scheme of CTCS-1 system level transition scenario is improved. A UML-based NuSMV modeling and verification method is used to establish the UML model and NuSMV model of level transition scenario. The activity, certainty and other properties of the scenario model are verified, which proves that the improved scenario meets the scenario requirements and the system specifications. The discussion of the CTCS-1 level transition scenario can support the revision of the relevant specifications.

Key words: CTCS-1 train control system, scenario of level transition, NuSMV model, verification