联锁系统UML模型的建立与形式化验证

• 作者: 刘征 武晓春
• 来源期刊: 铁道标准设计
• 学科: 交通运输
• 关键词: 形式化验证 计算机联锁系统 UML NuSMV 模型转换
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: 通信/信号
• 页码范围: 164-170
• 页数: 7页
• 分类号: TP301.2|U284.36
• 字数: 4882字
• 语种: 中文
• DOI: 10.13238/j.issn.1004-2954.201707050007

摘要

针对目前计算机联锁系统建模与验证难度较大的问题,提出一种UML(Unified Modeling Language)与NuSMV(New Symbolic Model Verifier)相结合的计算机联锁模型形式化检验方法.以一个标准站场中的一条接车进路建立过程为例,对联锁系统需求进行分析并通过UML建立相应的模型,再列出它与NuSMV之间的映射关系并实现将UML模型自动转换为NuSMV形式化模型,最后完成对计算机联锁系统的验证,检测其需求中可能存在的漏洞.该方法能够降低对计算机联锁系统形式化建模与验证的难度与减少人工建模时可能出现的错误,为计算机联锁系统形式化模型的建立与验证提供一种新思路.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	武晓春	兰州交通大学自动化与电气工程学院	50	190	8.0	12.0
2	刘征	兰州交通大学自动化与电气工程学院	2	2	1.0	1.0