| 摘要 | 第1-6页 |
| Abstract | 第6-10页 |
| 插图目录 | 第10-11页 |
| 第一章 绪论 | 第11-18页 |
| ·研究背景 | 第11-13页 |
| ·研究现状 | 第13-15页 |
| ·本文工作 | 第15-16页 |
| ·本文布局 | 第16-18页 |
| 第二章 无线传感网络协议及形式化分析方法 | 第18-30页 |
| ·无线传感网络及其协议 | 第18-23页 |
| ·协议分析方法 | 第23-25页 |
| ·时间自动机、基于统计的模型检验及模型检验工具UPPAAL | 第25-28页 |
| ·WSN协议建模与验证相关工作 | 第28-29页 |
| ·本章小结 | 第29-30页 |
| 第三章 基于随机时间自动机的无线传感网络协议建模与分析框架 | 第30-36页 |
| ·WSN协议建模 | 第30-33页 |
| ·工作流程时间自动机建模 | 第30-31页 |
| ·复杂环境与动态行为建模 | 第31-33页 |
| ·WSN协议验证与分析 | 第33-35页 |
| ·用传统模型检验进行正确性验证 | 第33页 |
| ·用基于统计的模型检验进行性能评估 | 第33-35页 |
| ·本章小结 | 第35-36页 |
| 第四章 基于随机时间自动机的WSN协议建模实例研究 | 第36-43页 |
| ·TPSN建模 | 第36-40页 |
| ·FTSP建模 | 第40-41页 |
| ·本章小结 | 第41-43页 |
| 第五章 基于统计模型检验技术的WSN协议分析与评估实例研究 | 第43-50页 |
| ·TPSN评估 | 第43-46页 |
| ·TPSN正确性评估 | 第43-44页 |
| ·TPSN性能评估 | 第44-46页 |
| ·FTSP评估 | 第46-48页 |
| ·FTSP正确性评估 | 第46-47页 |
| ·FTSP性能评估 | 第47-48页 |
| ·本章小结 | 第48-50页 |
| 第六章 无线传感网络协议描述语言WPDL和辅助建模工具AMT | 第50-56页 |
| ·WSN协议描述语言WPDL | 第50-52页 |
| ·时间自动机模型与XML结构 | 第52-53页 |
| ·AMT工具及实例 | 第53-54页 |
| ·本章小结 | 第54-56页 |
| 第七章 总结与展望 | 第56-58页 |
| ·总结 | 第56-57页 |
| ·下一步工作 | 第57-58页 |
| 参考文献 | 第58-64页 |
| 攻读硕士学位期间的研究成果 | 第64-65页 |
| 致谢 | 第65-66页 |
