| 传值进程模型检测中诊断信息的生成 |
| 其他题名 | diagnostic information generation in model checking value-passing processes
|
| 刘剑; 林惠民
|
| 2003
|
| 发表期刊 | 软件学报
 |
| ISSN | 1000-9825
|
| 卷号 | 14期号:1页码:40186 |
| 摘要 | 诊断信息自动生成是模型检测方法的基本特征之一，对分析和排错具有重要的意义，讨论了传值进程模型检测中诊断信息的生成问题，引入了两种诊断信息的表示结构：证明图和示例；提出了两种诊断信息的构造算法，所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例，这样可以继承已有的信息，从而减少计算量，相应的算法已经实现并用实例作了分析测试，实验结果表明该方法是有效的。 |
| 收录类别 | ei,wanfang,cscd
|
| 关键词 | 进程代数
模型检测
证明图
示例
诊断生成 Process Algebra
Model Checking
Proof Graph
Witness
Diagnosis Generation
|
| 部门归属 | 计算机科学国家重点实验室
|
| 资助者 | 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
|
| 语种 | 中文
|
| 内容类型 | 期刊论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/4458
|
| 专题 | 基础软件与系统重点实验室
|
推荐引用方式
GB/T 7714 |
刘剑,林惠民. 传值进程模型检测中诊断信息的生成[J]. 软件学报,2003,14(1):40186.
|
| APA |
刘剑,&林惠民.(2003).传值进程模型检测中诊断信息的生成.软件学报,14(1),40186.
|
| MLA |
刘剑,et al."传值进程模型检测中诊断信息的生成".软件学报 14.1(2003):40186.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论