基于带参系统Murphi模型的SMV自动建模
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:


Automatic Modeling in SMV Based on Murphi Model of Parameterized Systems
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    We present a method for automatic modeling in SMV of a parameterized system based on its corresponding Murphi Model. Modeling in Murphi for parameterized systems is easy because its parameterization feature, and a Murphi model code is relatively small and is not very complex to read, understand and modify. On the other hand, an SMV model could give more powerful operations, such as quick invariant checking and bounded model checking, but it is very hard to model in SMV for a parameterized system and to maintain an SMV model. We present a semantic model which is well able to describe a parameterized system, then analyze a Murphi model to create its semantic model, finally we get its corresponding SMV model which is effective for research work automatically by a series of conversion strategies.

    参考文献
    相似文献
    引证文献
引用本文

段凯强,李勇坚.基于带参系统Murphi模型的SMV自动建模.计算机系统应用,2016,25(11):178-182

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2016-03-03
  • 最后修改日期:2016-03-31
  • 录用日期:
  • 在线发布日期: 2016-11-15
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号