铁道标准设计2018，Vol.62Issue(6)：164-170,7.DOI:10.13238/j.issn.1004-2954.201707050007
联锁系统UML模型的建立与形式化验证
UML Model Establishment and Formal Verification for Interlocking System
摘要
Abstract
Aiming at the difficulties in the modeling and verification of the computer interlocking system,a formal model verification method of computer interlocking based on UML and NuSMV is proposed.Firstly taking a route setting process of a standard station as an example,this paper analyzes the requirements of the computer interlocking system and establishes the corresponding model with UML.Then the mapping relationship between UML and NuSMV is listed,and the conversion from UML model to NuSMV formal model is completed automatically.Finally,the formal model is verified to find possible vulnerabilities of the computer interlock system.This method can not only reduce the difficulties in formal modeling and verification of the system,but also avoid artificial modeling errors,thus providing a new way for the formal modeling and verification of the computer interlocking system.关键词
形式化验证/计算机联锁系统/UML/NuSMV/模型转换Key words
Formal model verification/Computer interlocking system/UML/NuSMV/Model transformation分类
信息技术与安全科学引用本文复制引用
刘征,武晓春..联锁系统UML模型的建立与形式化验证[J].铁道标准设计,2018,62(6):164-170,7.基金项目
国家自然科学基金地区项目(61661027) （61661027）
