CTCS-2级列控系统的形式化建模与验证  

Formal Modeling and Verification of CTCS-2 Train Control System

作　　者：董昱[1] 水晶[1] 黎磊[1] 

机构地区：[1]兰州交通大学自动化与电气工程学院,兰州730070

出　　处：《计算机工程》2013年第3期12-15,共4页Computer Engineering

基　　金：国家自然科学基金资助项目(61164010);甘肃省教育厅硕导基金资助项目(210110)

摘　　要：由于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.

关 键 词：列控系统 符号模型检验 形式化方法 车载设备 模式转换 

分 类 号：N945[自然科学总论—系统科学]