基于有界模型检验的传感网软件验证方法研究
| 摘要 | 第4-5页 |
| Abstract | 第5页 |
| 目录 | 第6-7页 |
| 第一章 绪论 | 第7-11页 |
| 1.1 课题研究背景和意义 | 第7-8页 |
| 1.2 国内外研究现状 | 第8-9页 |
| 1.3 论文内容以及结构安排 | 第9-11页 |
| 第二章 相关工作 | 第11-21页 |
| 2.1 传感网基本概念 | 第11页 |
| 2.2 传感网软件验证 | 第11-18页 |
| 2.2.1 软件验证技术 | 第11-12页 |
| 2.2.2 基于模型检验的软件验证技术的分类 | 第12-13页 |
| 2.2.3 TinyOS 系统与 NesC 语言 | 第13-18页 |
| 2.3 模型检验技术 | 第18-20页 |
| 2.3.1 模型检验基本原理 | 第18-19页 |
| 2.3.2 时态逻辑和其它逻辑 | 第19页 |
| 2.3.3 状态空间爆炸以及相关技术 | 第19-20页 |
| 2.4 本章小结 | 第20-21页 |
| 第三章 基于有界模型检验的传感网软件代码验证方法 | 第21-41页 |
| 3.1 引言 | 第21-26页 |
| 3.1.1 传感网软件的代码分析技术 | 第21-22页 |
| 3.1.2 C 语言的验证处理方法 | 第22-26页 |
| 3.2 基于模型检验的传感网软件代码分析 | 第26-30页 |
| 3.2.1 传感网软件模型静态结构分析 | 第26-29页 |
| 3.2.2 传感网软件模型动态行为分析 | 第29-30页 |
| 3.3 基于有界模型检验的转换规则 | 第30-32页 |
| 3.4 传感网软件代码验证分析 | 第32-39页 |
| 3.4.1 验证工具以及工作原理 | 第32-33页 |
| 3.4.2 基于 CBMC 的 C 程序验证 | 第33-35页 |
| 3.4.3 验证分析 | 第35-39页 |
| 3.5 本章小结 | 第39-41页 |
| 第四章 基于模型检验的传感网软件验证优化 | 第41-50页 |
| 4.1 引言 | 第41页 |
| 4.2 基于改进的 POR 的验证优化算法 | 第41-43页 |
| 4.3 基于改进的 POR 的验证优化算法 | 第43-45页 |
| 4.4 验证分析 | 第45-48页 |
| 4.4.1 验证工具介绍 | 第45-47页 |
| 4.4.2 验证结果分析 | 第47-48页 |
| 4.5 本章小结 | 第48-50页 |
| 第五章 总结与展望 | 第50-52页 |
| 5.1 工作总结 | 第50-51页 |
| 5.2 进一步研究展望 | 第51-52页 |
| 参考文献 | 第52-55页 |
| 附录1 攻读硕士学位期间申请的专利 | 第55-56页 |
| 附录2 攻读硕士学位期间参加的科研项目 | 第56-57页 |
| 致谢 | 第57页 |
