摘要
针对目前计算机联锁系统建模与验证难度较大的问题,提出一种UML(Unified Modeling Language)与NuSMV(New Symbolic Model Verifier)相结合的计算机联锁模型形式化检验方法。以一个标准站场中的一条接车进路建立过程为例,对联锁系统需求进行分析并通过UML建立相应的模型,再列出它与NuSMV之间的映射关系并实现将UML模型自动转换为NuSMV形式化模型,最后完成对计算机联锁系统的验证,检测其需求中可能存在的漏洞。该方法能够降低对计算机联锁系统形式化建模与验证的难度与减少人工建模时可能出现的错误,为计算机联锁系统形式化模型的建立与验证提供一种新思路。
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.
作者
刘征
武晓春
LIU Zheng;WU Xiao-chun(School of Automation ＆ Electrical Engineering,Lanzhou Jiaotong University,Lanzhou 730070,China)
出处
《铁道标准设计》
北大核心
2018年第6期164-170,共7页
Railway Standard Design
基金
国家自然科学基金地区项目(61661027)
