传值进程模型检测中诊断信息的生成
文献类型：期刊论文
| 作者 | 刘剑 ; 林惠民 |
| 刊名 | 软件学报
 |
| 出版日期 | 2003 |
| 卷号 | 14期号:1页码:40186 |
| 关键词 | 进程代数 模型检测 证明图 示例 诊断生成 process algebra model checking proof graph witness diagnosis generation |
| ISSN号 | 1000-9825 |
| 其他题名 | diagnostic information generation in model checking value-passing processes |
| 中文摘要 | 诊断信息自动生成是模型检测方法的基本特征之一，对分析和排错具有重要的意义，讨论了传值进程模型检测中诊断信息的生成问题，引入了两种诊断信息的表示结构：证明图和示例；提出了两种诊断信息的构造算法，所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例，这样可以继承已有的信息，从而减少计算量，相应的算法已经实现并用实例作了分析测试，实验结果表明该方法是有效的。 |
| 收录类别 | ei,wanfang,cscd |
| 资助信息 | National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office |
| 语种 | 中文 |
| 公开日期 | 2010-08-24 |
| 附注 | 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. |
| 源URL | [http://124.16.136.157/handle/311060/4458]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _期刊论文 |
| 推荐引用方式 GB/T 7714 | 刘剑,林惠民. 传值进程模型检测中诊断信息的生成[J]. 软件学报,2003,14(1):40186. |
| APA | 刘剑,&林惠民.(2003).传值进程模型检测中诊断信息的生成.软件学报,14(1),40186. |
| MLA | 刘剑,et al."传值进程模型检测中诊断信息的生成".软件学报 14.1(2003):40186. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。