传值进程模型检测中诊断信息的生成
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

(Supported by the National Natural Science Foundation of China under Grant No.69833020 (国家自然科学基金)


Diagnostic Information Generation in Model Checking Value-Passing Processes
Author:
Affiliation:

Fund Project:

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

    诊断信息自动生成是模型检测方法的基本特征之一,对分析和排错具有重要的意义.讨论了传值进程模型检测中诊断信息的生成问题.引入了两种诊断信息的表示结构:证明图和示例;提出了两种诊断信息构造算法.所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例,这样可以继承已有的信息,从而减少计算量.相应的算法已经实现并用实例作了分析测试.实验结果表明该方法是有效的.

    Abstract:

    Automatic diagnostic information generation is one of the remarkable advantages of model checking methods. It is very important to understand the reason for the failure and fix the problem. In this paper, how to generate effective diagnosis in model checking value-passing processes is discussed. Two diagnostic forms, proof graph and witness, are defined. Moreover, algorithms are proposed to construct them from the search states space in model checking process. By this way, useful diagnoses are generated from the existing information by less calculation. Besides above, the algorithms have been implemented and used to analyze several cases. The experimental results show that this method is efficient.

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

刘剑,林惠民.传值进程模型检测中诊断信息的生成.软件学报,2003,14(1):1-8

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2002-05-10
  • 最后修改日期:2002-07-29
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号