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

• 作者: 李勇坚 段凯强
• 来源期刊: 计算机系统应用
• 关键词: 带参系统 模型检测 自动建模 形式验证
• 年，卷（期）: 2016,（11）
• 所属期刊栏目: 软件技术·算法
• 页码范围: 178-182
• 页数: 5页
• 字数: 4677字
• 语种: 中文
• DOI: 10.15888/j.cnki.csa.005411

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李勇坚	中国科学院软件研究所计算机科学国家重点实验室	6	9	2.0	2.0
2	段凯强	中国科学院软件研究所计算机科学国家重点实验室	1	0	0.0	0.0