中文摘要：

由于CTCS-2级列控系统设计复杂，因此提出一种将统一建模语言（UML）与符号模型检验相结合的形式化建模与验证方法。分析CTCS-2级列控车载设备的模式转换场景，对其进行UML建模得到UML类图和状态图，制定转换规则对UML模型进行扩展和抽象，使其转化为NuSMV模型。将待验证的系统性质和转化后的检验程序输入符号模型检验系统进行验证，验证结果都为true，表明CTCS-2级列控车载设备的模式转化场景具有活性、可达性和安全性。

英文摘要：

For the designing complexity of CTCS-2 system, this paper proposes the method combining Unified Modeling Language（UML） and Symbolic Model Checking（SMC） for modeling and formal verification. It analyzes the mode conversion scene of CTCS-2 on-board equipment. The mode conversion scene of CTCS-2 on-board equipment is modeled by using the UML, and UML class diagrams and UML state diagrams are gotten as well, through formulating some exchanging rules to extend and abstract UML model and exchanging it to the NuSMV model. The property of to be verified system and system Symbolic Model Verifier（SMV） model are inputted to symbolic model verifier to check. The verified results are true, and it shows that mode conversion scene of CTCS-2 on-board equipment has activity, accessibility and security.