基于带参系统Murphi模型的SMV自动建模

摘要：

提出了一种基于带参系统的Murphi模型来完成对应的SMV自动化建模的方法.因为Murphi工具拥有带参特性,因此使用其对带参系统进行建模比较容易,而且得到的模型代码量比较少,易于阅读、理解和修改;而SMV模型则能实现更丰富的控制,如进行快速不变式检查和限界模型检测等,但是建模过程复杂,模型不易维护.我们通过对两者进行分析,首先提出了能够很好描述带参系统的一个语义模型,然后读入相应的Murphi模型并进行分析以获取其语义模型表示,最后再通过一系列的策略自动得到限定参数时的SMV模型,由此得到的模型能够满足实际科研工作的应用要求.

关键词：带参系统、模型检测、自动建模、形式验证

所属期刊栏目：25

分类号：TP3;V22

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

页数：共5页

页码：178-182