具体反例生成与图形化显示系统
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家科技重大专项(2012ZX01039-004)


CCGS System
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 增强出版
  • |
  • 文章评论
    摘要:

    模型检测是用来验证系统模型是否满足所期望性质的一种形式化方法, 模型检测相对于其它的模型检验方法有两个显著的特点, 一个是它对模型进行检测的过程是自动化的, 另一个是当系统不满足所验证的性质时, 它会给出一条反例路径, 这条反例路径可以为系统修正提供帮助. 本文研究的重点就是如何使这条反例路径的生成在高效的同时其反例信息又直观易懂, 为系统修正带来更方便快捷的帮助. 本文中实现了具体反例生成与图形化显示系统(简称CCGS), 它能快速生成离散语义下具体反例并图形化显示时间自动机沿着该具体反例的运行过程. 实验结果表明CCGS能够快速生成具体反例路径信息, 并且能够图形化显示具体反例信息, 为系统修正提供更直观的信息, 提高系统的正确性和安全性.

    Abstract:

    Model checking is a formal method to verify the system satisfies an expected property or not. Trere are two significant advantages of it, one is that it is fully automatic and the other is that if the system doesn't satisfy the checked property, it will generate an counterexamples which can help to fix errors in the system. The main purpose of this paper is to generate this counterexamples efficiently and intuitively. In order to generate the counterexamples efficiently and graphically display the operating processes of the system running alongside the concrete counterexamples, a system CCGS has been developed. Experimental results have shown that CCGS delivers an expected performance, and can help to improve the correctness and safety of the checked systems.

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

信贤卫.具体反例生成与图形化显示系统.计算机系统应用,2013,22(11):51-57

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

京公网安备 11040202500063号