| 授予学历硕士人员登记表 | 第4-6页 |
| 摘要 | 第6-7页 |
| Abstract | 第7-8页 |
| 第一章 绪论 | 第12-24页 |
| 1.1 选题背景与意义 | 第12-13页 |
| 1.2 国内外研究现状 | 第13-20页 |
| 1.3 本文研究目标与主要工作 | 第20-21页 |
| 1.4 本文的组织安排 | 第21-24页 |
| 第二章 研究基础 | 第24-38页 |
| 2.1 嵌入式系统及其基本结构 | 第24-25页 |
| 2.2 数据竞态条件 | 第25-26页 |
| 2.3 常见数据竞态条件的动态检测技术 | 第26-29页 |
| 2.3.1 基于监视器的检测技术 | 第27页 |
| 2.3.2 基于发生序的检测技术 | 第27-28页 |
| 2.3.3 基于锁集的检测技术 | 第28-29页 |
| 2.4 Valgrind插桩平台 | 第29-34页 |
| 2.4.1 插桩过程 | 第30-32页 |
| 2.4.2 插件工具编写 | 第32-34页 |
| 2.5 嵌入式虚拟化 | 第34-35页 |
| 2.6 Yices求解器中DPLL求解规则与策略 | 第35-38页 |
| 2.6.1 DPLL求解规则 | 第36页 |
| 2.6.2 DPLL求解策略 | 第36-38页 |
| 第三章 基于二进制动态插装的多线程程序的执行路径追踪技术 | 第38-50页 |
| 3.1 概述 | 第38-39页 |
| 3.2 路径追踪方法的相关概念 | 第39-40页 |
| 3.3 路径追踪方法的工作原理 | 第40-42页 |
| 3.4 路径追踪工具的整体设计与实现 | 第42-47页 |
| 3.4.1 整体设计 | 第42-43页 |
| 3.4.2 线程封装 | 第43-45页 |
| 3.4.3 动态插桩路径追踪 | 第45-47页 |
| 3.5 实验验证 | 第47-49页 |
| 3.6 本章小结 | 第49-50页 |
| 第四章 基于SMT求解器的嵌入式多线程程序数据竞态条件分析 | 第50-64页 |
| 4.1 概述 | 第50-52页 |
| 4.2 嵌入式多线程程序数据竞态条件描述 | 第52-53页 |
| 4.3 SMT(可满足性模理论)的概述 | 第53页 |
| 4.4 SMT理论求解器(T-求解器) | 第53-54页 |
| 4.5 基于SMT求解器数据竞态条件分析方法的相关概念与定理 | 第54-56页 |
| 4.6 基于SMT求解器的数据竞态条件检测方法 | 第56-61页 |
| 4.6.1 建立有关时序约束条件 | 第56-57页 |
| 4.6.2 构建Yices求解器的输入量 | 第57-58页 |
| 4.6.3 数据竞态条件的检测框架与分析流程 | 第58-61页 |
| 4.7 实验验证 | 第61-63页 |
| 4.8 本章小结 | 第63-64页 |
| 第五章 嵌入式多线程程序的数据竞态条件分析系统 | 第64-74页 |
| 5.1 概述 | 第64页 |
| 5.2 分析系统的搭建 | 第64-66页 |
| 5.2.1 ARM硬件平台仿真 | 第64-65页 |
| 5.2.2 数据竞态条件分析系统的设计框架 | 第65-66页 |
| 5.3 实验测试平台参数 | 第66-67页 |
| 5.4 实验设计与分析 | 第67-72页 |
| 5.5 本章小结 | 第72-74页 |
| 第六章 总结与展望 | 第74-76页 |
| 6.1 本文总结 | 第74-75页 |
| 6.2 未来工作 | 第75-76页 |
| 致谢 | 第76-78页 |
| 参考文献 | 第78-84页 |
| 附录A 硕士期间发表的论文专利与软著 | 第84-86页 |
| 附录B 硕士期间参与项目 | 第86页 |
