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

摘要：

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

关键词：形式化验证、计算机联锁系统、UML、NuSMV、模型转换

所属期刊栏目：62

分类号：TP301.2;U284.36(计算技术、计算机技术)

资助基金：国家自然科学基金地区项目61661027

在线出版日期：2018-07-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：164-170