Java并发程序的模型提取与模型检测技术研究
| 摘要 | 第1-6页 |
| Abstract | 第6-13页 |
| 第1章 绪论 | 第13-24页 |
| ·研究背景 | 第13-19页 |
| ·Java 语言 | 第13-15页 |
| ·模型检测 | 第15-19页 |
| ·相关工作介绍 | 第19-21页 |
| ·本课题的研究内容 | 第21-22页 |
| ·本文组织结构 | 第22-24页 |
| 第2章 Java 并发程序分析 | 第24-38页 |
| ·Java 的并发机制介绍 | 第24-35页 |
| ·Java 并发程序锁的问题 | 第25-28页 |
| ·Java 并发程序的通信问题 | 第28-32页 |
| ·Java 并发程序的同步问题 | 第32-35页 |
| ·JAVACC 简介 | 第35-36页 |
| ·JTB 简介 | 第36-37页 |
| ·产生的文件 | 第36页 |
| ·自动产生的类 | 第36-37页 |
| ·小结 | 第37-38页 |
| 第3章 模型检测理论及工具 | 第38-50页 |
| ·模型检测简介 | 第38-40页 |
| ·模型检测工具 | 第40-45页 |
| ·模型检测工具SPIN | 第40页 |
| ·SPIN 工作原理及相关定义 | 第40-42页 |
| ·SPIN 的基本结构 | 第42-43页 |
| ·SPIN 搜索算法 | 第43-44页 |
| ·偏序规约 | 第44-45页 |
| ·线性时序逻辑LTL | 第45-46页 |
| ·Java 并发程序模型检测 | 第46-49页 |
| ·小结 | 第49-50页 |
| 第4章 Java 并发程序的模型检测 | 第50-64页 |
| ·Java 程序分析 | 第50-51页 |
| ·建立promela 模型 | 第51-54页 |
| ·类 | 第52页 |
| ·方法 | 第52-53页 |
| ·属性 | 第53页 |
| ·方法内部语句 | 第53-54页 |
| ·Java 并发程序的特殊控制结构 | 第54-59页 |
| ·锁模型 | 第54-55页 |
| ·通信控制模型 | 第55-58页 |
| ·同步控制模型 | 第58-59页 |
| ·检测结果 | 第59-60页 |
| ·模拟路径分析 | 第60-62页 |
| ·实验 | 第62-63页 |
| ·小结 | 第63-64页 |
| 第5章 基于Java 内存模型的并发程序模型检测 | 第64-74页 |
| ·模型定义与算法 | 第64-66页 |
| ·模型建立与检测 | 第66-72页 |
| ·简单乱序模型 | 第66页 |
| ·包含Volatile 变量的乱序模型 | 第66-69页 |
| ·包含依赖关系的乱序模型 | 第69-72页 |
| ·小结 | 第72-74页 |
| 结论 | 第74-76页 |
| 参考文献 | 第76-80页 |
| 致谢 | 第80-81页 |
| 附录 A 攻读学位期间所发表的论文 | 第81-82页 |
| 附录 B 攻读学位期间所参与的科研活动 | 第82页 |
