CTCS-1级列控系统等级转换场景建模与验证

随着CTCS-1级列控系统关键技术研究工作的开展，必然要面临装载CTCS-1级车载设备的列车跨线运营至CTCS-0级线路的问题，而系统等级转换的顺利进行是实现列车安全跨线运营的基础。通过系统功能分析，建立了系统多分辨率功能模型，以识别等级转换场景需求；根据场景需求，结合现行系统规范，完善了CTCS-1级系统等级转换场景的方案；采用基于UML的NuSMV建模与验证方法，建立了等级转换场景的UML模型和NuSMV模型，并验证了场景模型的活性、确定性等属性，从而证明了完善后的场景方案满足场景需求，且符合系统规范。文中对CTCS-1级系统等级转换场景的探讨可为相关规范的修订提供支持。

Modeling and Verification of Level Transition Scenario of Train Control System CTCS-1

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.