模型检验的反例解释

论文题目: 模型检验的反例解释

论文类型: 博士论文

论文专业: 计算机科学与技术

作者: 沈胜宇

导师: 李思昆

关键词: 形式化验证,模型检验,电子设计自动化,反例解释,错误定位,反例压缩

文献来源: 国防科学技术大学

发表年度: 2005

论文摘要: 近年来,随着硬件系统(尤其是超大规模集成电路)规模不断增大,单纯的动态模拟方法已经无法提供足够的覆盖率,以满足系统验证的充分性和完备性要求。因此模型检验等形式化验证方法成为复杂硬件系统验证的重要手段。与定理证明等其他形式化验证方法相比,模型检验的主要优点在于:当断言被违反时,模型检验方法能够给出反例,以解释断言被违反的原因。 然而复杂系统的反例非常难以理解,需要花费大量时间检查大量的变量和事件,才能够找到错误的根源。这就导致模型检验带来的验证效率提升,被浪费在低效的反例理解和错误定位上。因此从反例中提取有用信息,以帮助验证工程师高效地理解反例和定位错误,成为目前的研究热点。另外,许多模型检验算法需要存储和处理反例或证例(witness)。从反例中剔除无关变量,可以使这些算法在空间和时间复杂度上获得指数改进。因此,根据不同应用的要求,对模型检验的反例作进一步处理,具有重要的意义。我们将这些方法统称为反例解释。 不同的应用环境,对反例解释方法有不同的要求,主要反映在完备性、时间开销和结果尺寸方面。当反例解释的结果需要由验证工程师阅读、理解和定位错误时,对完备性和时间开销的要求不高,但要求结果一定要紧凑和精简。我们称之为″非完备的错误定位方法″。另一方面,当反例解释的结果需要由其他算法作进一步处理时(比如抽象精化模型检验方法),对完备性和时间开销的要求非常高,而将结果尺寸放在第二位。我们称之为″完备的反例压缩方法″。 本文对非完备和完备方法都进行了深入研究,完成的主要研究工作和取得的主要研究成果如下: 1.在非完备错误定位方法方面,提出了迭代式证例搜索算法。在对现有最近证例搜索算法进行深入分析时,我们发现:在广度优先的代码检查过程中,多个最近证例和高扇入节点会对错误定位的精度产生巨大影响。为了解决这一问题,我们提出了迭代式证例搜索算法。该算法迭代地搜索最近证例,每次迭代产生一个谓词差异集合,并添加到一个谓词列表的后端。越是位于列表前端的谓词,越有可能是实际的错误。使用该谓词列表作为定位结果,可以避免广度优先搜索导致的精度损失。试验结果证明,本算法与单纯的最近证例搜索算法相比,定位精度有很大提高。 2.针对确定性系统的路径反例(path-like counterexample),提出了基于悖论分析和增量式SAT求解的反例压缩算法,以降低BFL算法的时间开销。BFL是目前压缩效率最高的算法,通常能够剔除70%以上的无关变量。然而,BFL的线性收敛特性导致其时间开销过大。为此我们在BFL中引进了悖论分析方法。该算法通过分析导致悖论的原因,从而能够一次剔除多个无关变量,而不是象BFL那样一次只能剔除一个无关变量。同时我们发现,BFL中的相邻SAT问题非常相似,存在着大量的重叠状态空间。单独的求解这些SAT问题,将导致这些重叠状态空间被反复

论文目录:

插图索引

表格索引

摘要

ABSTRACT

第一章 绪论

1.1 研究背景

1.2 模型检验方法概述

1.2.1 系统描述

1.2.2 断言描述

1.2.3 模型检验算法

1.2.4 成功后处理

1.3 问题的提出和相关研究

1.3.1 反例压缩

1.3.2 错误定位方法

1.3.3 为反例标注证明步骤

1.3.4 其他方法

1.4 本文的主要工作和创新

1.5 论文结构

第二章 基于迭代式证例搜索的错误定位方法

2.1 引言

2.2 背景知识

2.2.1 反事实、距离度量与原因

2.2.2 伪布尔SAT

2.2.3 模型检验与限界模型检验

2.3 并列最近证例对定位精度的影响以及解决方法

2.4 错误定位算法

2.4.1 算法整体流程

2.4.2 谓词提取

2.4.3 证例搜索

2.4.4 谓词过滤

2.4.5 证例屏蔽

2.5 实验结果及分析

2.5.1 精确性度量

2.5.2 实验对象简介

2.5.3 实验结果

2.5.4 结果分析

2.6 结论

第三章 基于悖论分析和增量式求解的快速反例压缩算法

3.1 引言

3.2 背景知识

3.2.1 限界模型检验

3.2.2 SAT求解器中的冲突学习机制

3.2.3 BFL反例压缩算法及其问题

3.3 基于悖论分析的反例压缩算法

3.3.1 算法概述

3.3.2 悖论分析

3.3.3 正确性证明

3.3.4 复杂性分析

3.4 增量式SAT求解方法

3.5 实验结果及分析

3.5.1 试验对象

3.5.2 试验方法

3.5.3 试验结果

3.5.4 结果分析

3.6 结论

第四章 低存储开销的反例压缩算法

4.1 引言

4.2 背景知识

4.2.1 SAT求解器

4.2.2 模型检验及反例

4.2.3 BFL反例压缩算法

4.3 步进的BFL

4.3.1 问题分解

4.3.2 子问题求解

4.3.3 复杂度分析

4.4 步进的单位核提取

4.5 实验结果及讨论

4.6 结论

第五章 非确定系统中不变断言的反例压缩

5.1 引言

5.2 背景知识

5.2.1 SAT求解器

5.2.2 模型检验

5.2.3 状态集合的立方表示

5.2.4 基于SAT的前置映象运算

5.2.5 确定系统的反例压缩

5.3 非确定系统的反例压缩原理

5.3.1 压缩反例的标准

5.3.2 确定与非确定系统的区别

5.3.3 压缩反例的定义

5.4 算法的实现、证明与复杂性分析

5.4.1 算法描述

5.4.2 正确性证明

5.4.3 算法复杂度

5.5 实验结果及分析

5.6 结论

第六章 完备的ACTL反例压缩算法

6.1 引言

6.2 背景知识

6.2.1 二叉决策图(Binary Decision Diagrams)

6.2.2 CTL时态逻辑

6.2.3 模型检验

6.2.4 公平约束

6.2.5 反例产生

6.2.6 状态集合的立方表示

6.3 路径证例压缩算法

6.3.1 EX证例压缩

6.3.2 EU证例压缩

6.4 EG环形证例压缩

6.4.1 Loop压缩

6.4.2 Stem压缩

6.5 实验结果

6.6 结论

第七章 错误定位与反例压缩原型系统的实现

7.1 NuSMV模型检验器

7.2 Zchaff求解器

7.2.1 基本数据结构和操作

7.2.2 增量式求解机制

7.3 PBS伪布尔求解器

7.4 非完备错误定位原型系统

7.4.1 谓词提取

7.4.2 生成断言和反断言的CNF文件

7.4.3 提取信号映射关系、提取反例谓词赋值

7.4.4 生成证例约束

7.4.5 PBS最近证例搜索

7.4.6 谓词差异提取

7.4.7 广度优先代码搜索

7.5 完备的反例压缩原型系统

7.5.1 生成断言的CNF文件

7.5.2 提取信号映射关系

7.5.3 目标取反

7.5.4 添加完全约束

7.5.5 选择尚未被剔除的变量v，并删除v的赋值短句

7.5.6 添加v的赋值短句

7.5.7 剔除悖论分析结果

第八章 结语

8.1 本文主要贡献

8.2 对今后研究工作的展望

8.2.1 在非完备的反例解释方面：

8.2.2 在完备性反例压缩方面

8.2.3 在错误改正方面

攻读博士期间已发表录用和撰写的论文

攻读博士期间参与的主要科研项目

致谢

参考文献

发布时间: 2005-11-07

参考文献

• [1].基于多项式符号代数的数字电路形式验证方法研究[D]. 杨志.哈尔滨工程大学2009

相关论文

• [1].基于模拟理论的模型检测研究[D]. 袁志斌.华中科技大学2007
• [2].扩展时序逻辑的推理及符号化模型检验技术[D]. 刘万伟.国防科学技术大学2009
• [3].并发系统的模型检测与测试[D]. 吴鹏.中国科学院研究生院（软件研究所）2005
• [4].可满足性问题算法研究以及在时序电路等价验证中的应用[D]. 丁敏.复旦大学2005
• [5].基于接口自动机的组合验证方法研究[D]. 文艳军.国防科学技术大学2005
• [6].安全协议形式化验证技术的研究与实现[D]. 李梦君.国防科学技术大学2005
• [7].程序正确性验证的几个问题[D]. 范年柏.湖南大学2005
• [8].轨道交通列车运行控制系统的形式化建模和模型检验方法研究[D]. 燕飞.北京交通大学2006

标签：形式化验证论文;  模型检验论文;  电子设计自动化论文;  反例解释论文;  错误定位论文;  反例压缩论文;