主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第5期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
刘剑,林惠民.传值进程模型检测中诊断信息的生成.软件学报,2003,14(1):1-8
传值进程模型检测中诊断信息的生成
Diagnostic Information Generation in Model Checking Value-Passing Processes
投稿时间:2002-05-10  修订日期:2002-07-29
DOI:
中文关键词:  进程代数  模型检测  证明图  示例  诊断生成
英文关键词:process algebra  model cheching  proofgraph  witness  diagnosis generation
基金项目:(Supported by the National Natural Science Foundation of China under Grant No.69833020 (国家自然科学基金)
作者单位
刘剑 中国科学院,软件研究所,计算机科学重点实验室,北京,100080 
林惠民 中国科学院,软件研究所,计算机科学重点实验室,北京,100080 
摘要点击次数: 3123
全文下载次数: 2997
中文摘要:
      诊断信息自动生成是模型检测方法的基本特征之一,对分析和排错具有重要的意义.讨论了传值进程模型检测中诊断信息的生成问题.引入了两种诊断信息的表示结构:证明图和示例;提出了两种诊断信息构造算法.所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例,这样可以继承已有的信息,从而减少计算量.相应的算法已经实现并用实例作了分析测试.实验结果表明该方法是有效的.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利