基于JPF的软件模型检测分析与应用
| 摘要 | 第1-4页 |
| ABSTRACT | 第4-9页 |
| 第1章 引言 | 第9-13页 |
| ·课题背景 | 第9-10页 |
| ·相关技术简介 | 第10-12页 |
| ·形式化验证方法 | 第10页 |
| ·JPF | 第10-12页 |
| ·本文的主要内容 | 第12-13页 |
| 第2章 基本理论 | 第13-25页 |
| ·模型检测 | 第13-16页 |
| ·模型检测过程 | 第13-14页 |
| ·模型表示 | 第14-15页 |
| ·性质描述和 LTL逻辑 | 第15页 |
| ·模型检测算法 | 第15-16页 |
| ·软件模型检测 | 第16-21页 |
| ·谓词抽象 | 第16-18页 |
| ·反例引导的抽象求精 | 第18-19页 |
| ·面向源代码的软件模型检测 | 第19-21页 |
| ·软件模型检测工具 | 第21页 |
| ·Java模型检测 | 第21-24页 |
| ·Java程序特点 | 第22-23页 |
| ·状态爆炸可行性解决方案 | 第23-24页 |
| ·小结 | 第24-25页 |
| 第3章 基于 JPF的Java程序验证 | 第25-35页 |
| ·JPF工作原理 | 第25-27页 |
| ·JPF体系结构 | 第27-29页 |
| ·JPF的关键技术 | 第29-34页 |
| ·显式状态与回溯 | 第29页 |
| ·减少状态数目策略 | 第29-30页 |
| ·偏序规约与对称规约 | 第30-32页 |
| ·内核扩展、状态匹配与运行路径配置 | 第32-33页 |
| ·符号执行 | 第33-34页 |
| ·小结 | 第34-35页 |
| 第4章 软件模型检测工具设计策略 | 第35-51页 |
| ·通用内核组成 | 第35-40页 |
| ·状态管理 | 第35-38页 |
| ·搜索策略 | 第38页 |
| ·环境模拟 | 第38-40页 |
| ·系统子功能 | 第40-47页 |
| ·对象工厂 | 第40-42页 |
| ·程序模型接口 | 第42-43页 |
| ·监听器 | 第43-46页 |
| ·报告系统 | 第46-47页 |
| ·系统交互 | 第47-50页 |
| ·代码标注 | 第48页 |
| ·开放验证 API | 第48-50页 |
| ·小结 | 第50-51页 |
| 第5章 Java程序模型检测平台开发 | 第51-62页 |
| ·JPF功能扩展方式 | 第51-52页 |
| ·静态配置 | 第51-52页 |
| ·动态配置 | 第52页 |
| ·平台设计与实现 | 第52-60页 |
| ·OSGI | 第53-54页 |
| ·Eclipse插件开发 | 第54-56页 |
| ·基于JPF的 Eclipse模型检测平台实现 | 第56-60页 |
| ·自定义轻量级错误轨迹监听器 | 第60-61页 |
| ·小结 | 第61-62页 |
| 第6章 平台应用实例 | 第62-70页 |
| ·并行相关 | 第62-65页 |
| ·死锁 | 第62-63页 |
| ·数据竞争 | 第63-65页 |
| ·未处理异常 | 第65-66页 |
| ·其他 | 第66-69页 |
| ·随机数问题 | 第66-68页 |
| ·哲学家进餐问题 | 第68-69页 |
| ·小结 | 第69-70页 |
| 第7章 结论与展望 | 第70-73页 |
| ·结论 | 第70-72页 |
| ·进一步工作的方向 | 第72-73页 |
| 致谢 | 第73-74页 |
| 参考文献 | 第74-77页 |
| 附录 A 程序配置文件 | 第77-79页 |
| 攻读学位期间的研究成果 | 第79页 |
