基于符号执行和约束求解的程序验证与测试工具
| 第1章 引言 | 第1-13页 |
| 1．1 测试的分类 | 第7-8页 |
| 1．2 测试的阶段 | 第8-10页 |
| 1．3 代码覆盖分析 | 第10-13页 |
| 1．3．1 语句覆盖 | 第11页 |
| 1．3．2 断言覆盖 | 第11-12页 |
| 1．3．3 条件覆盖 | 第12页 |
| 1．3．4 路径覆盖 | 第12-13页 |
| 第2章 扩展的有限状态机 | 第13-21页 |
| 2．1 测试数据自动生成的方法 | 第13-14页 |
| 2．2 控制流图 | 第14-16页 |
| 2．3 有限状态机（FSM） | 第16-17页 |
| 2．4 扩展的有限状态机（EFSM） | 第17-21页 |
| 第3章 构造与源程序等价的EFSM | 第21-31页 |
| 3．1 输入和输出 | 第21-22页 |
| 3．2 基本结构语句的处理 | 第22-23页 |
| 3．3 带函数程序的处理 | 第23-28页 |
| 3．3．1 基本思想 | 第23-24页 |
| 3．3．2 一些具体细节 | 第24-28页 |
| 3．4 其它一些工作 | 第28-31页 |
| 3．4．1 多维数组化为一维数组 | 第28页 |
| 3．4．2 EFSM的化简 | 第28-29页 |
| 3．4．3 EFSM正确性的检验工具 | 第29-31页 |
| 第4章 自动验证和测试工具EFAT | 第31-45页 |
| 4．1 工具BONUS | 第31-34页 |
| 4．1．1 线性规划 | 第31-32页 |
| 4．1．2 布尔表达式的满足问题 | 第32-33页 |
| 4．1．3 BoNuS的实现 | 第33-34页 |
| 4．2 搜索算法 | 第34页 |
| 4．3 数组的处理 | 第34-36页 |
| 4．4 关键数据结构 | 第36-38页 |
| 4．4．1 状态转换树 | 第36页 |
| 4．4．2 当前路径条件 | 第36-37页 |
| 4．4．3 变量值表 | 第37-38页 |
| 4．5 搜索策略 | 第38-41页 |
| 4．5．1 静态预测 | 第38-40页 |
| 4．5．2 动态增加 | 第40-41页 |
| 4．6 实验结果 | 第41-43页 |
| 4．7 第3章和第4章小结 | 第43-45页 |
| 第5章 白盒测试中数据库实例的自动生成 | 第45-57页 |
| 5．1 有关SQL的基本概念 | 第45-47页 |
| 5．1．1 关系模型 | 第45-46页 |
| 5．1．2 查询语言 | 第46页 |
| 5．1．3 嵌入式SQL | 第46-47页 |
| 5．2 数据库实例生成的基本问题和解决方法 | 第47-48页 |
| 5．2．1 需要解决的问题 | 第47页 |
| 5．2．2 约束满足方法 | 第47-48页 |
| 5．2．3 其它的约束 | 第48页 |
| 5．3 我们的自动工具 | 第48-55页 |
| 5．3．1 主要数据结构 | 第49-50页 |
| 5．3．2 算法和重要的代码 | 第50-53页 |
| 5．3．3 实验结果 | 第53-55页 |
| 5．4 本章小结 | 第55-57页 |
| 第6章 结论 | 第57-58页 |
| 参考文献 | 第58-62页 |
