基于模型检测技术的Java静态缺陷检查
| 摘要 | 第4-5页 |
| ABSTRACT | 第5页 |
| 1 引言 | 第8-11页 |
| 1.1 研究背景 | 第8-9页 |
| 1.2 研究现状 | 第9-10页 |
| 1.3 研究内容 | 第10页 |
| 1.4 论文组织结构 | 第10-11页 |
| 2 形式化的静态分析 | 第11-19页 |
| 2.1 程序静态分析 | 第11-13页 |
| 2.1.1 静态分析相关技术 | 第12-13页 |
| 2.1.2 形式化静态分析的实现方式 | 第13页 |
| 2.2 软件形式化方法 | 第13-19页 |
| 2.2.1 形式化规约 | 第14-17页 |
| 2.2.2 形式化验证 | 第17-19页 |
| 3 基于模型检测的程序分析 | 第19-25页 |
| 3.1 Kripke结构 | 第20页 |
| 3.2 时态逻辑 | 第20-24页 |
| 3.2.1 CTL语法及语义 | 第21-22页 |
| 3.2.2 CTL等价关系 | 第22-24页 |
| 3.3 状态爆炸与模型验证工具 | 第24-25页 |
| 4 系统实现 | 第25-41页 |
| 4.1 系统整体框架 | 第25-27页 |
| 4.2 积木式缺陷规则集模型 | 第27-30页 |
| 4.2.1 缺陷的行为抽象 | 第28-29页 |
| 4.2.2 积木式构建模式 | 第29-30页 |
| 4.3 验证引擎 | 第30-35页 |
| 4.3.1 控制流结构与Kripke | 第31页 |
| 4.3.2 基于Soot的控制流抽取与分析 | 第31-33页 |
| 4.3.3 动态匹配原子命题 | 第33-35页 |
| 4.4 模型转换 | 第35-41页 |
| 4.4.1 NuSMV模型验证器 | 第35-37页 |
| 4.4.2 模型转换机制 | 第37-41页 |
| 5 实验结果 | 第41-51页 |
| 5.1 实验环境 | 第41页 |
| 5.2 积木式静态缺陷集 | 第41-45页 |
| 5.2.1 代表性 | 第43-44页 |
| 5.2.2 可扩展性 | 第44-45页 |
| 5.3 建模与检测 | 第45-51页 |
| 6 工作总结与展望 | 第51-53页 |
| 6.1 总结 | 第51-52页 |
| 6.2 展望 | 第52-53页 |
| 参考文献 | 第53-56页 |
| 个人简介 | 第56-57页 |
| 导师简介 | 第57-58页 |
| 获得成果目录 | 第58-59页 |
| 致谢 | 第59页 |
