| 摘要 | 第1-8页 |
| Abstract | 第8-12页 |
| 第一章 绪论 | 第12-20页 |
| ·背景和动机 | 第12-14页 |
| ·无线网络形式化研究现状 | 第14-17页 |
| ·本文的主要工作 | 第17-20页 |
| 第二章 基础理论和方法 | 第20-34页 |
| ·形式语义 | 第20-23页 |
| ·程序统一理论 | 第23-26页 |
| ·Rely/Guarantee方法 | 第26-28页 |
| ·形式化描述语言Z | 第28-30页 |
| ·重写逻辑和Maude工具 | 第30-32页 |
| ·本章小结 | 第32-34页 |
| 第三章 无线系统演算的代数语义 | 第34-72页 |
| ·无线系统演算 | 第35-40页 |
| ·卫兵选择 | 第40-43页 |
| ·代数规则 | 第43-48页 |
| ·首规范型 | 第48-55页 |
| ·从代数语义计算操作语义的导出规则 | 第55-65页 |
| ·基于Maude工具的语义与导出规则自动实现 | 第65-70页 |
| ·语法实现 | 第65-66页 |
| ·代数语义和首规范型实现 | 第66-68页 |
| ·导出规则和操作语义的实现 | 第68-70页 |
| ·本章小结 | 第70-72页 |
| 第四章 无线系统演算的指称语义 | 第72-92页 |
| ·语义模型 | 第73-77页 |
| ·发送节点 | 第77-80页 |
| ·接收节点 | 第80-83页 |
| ·卫兵选择 | 第83-84页 |
| ·并行组合 | 第84-88页 |
| ·代数性质 | 第88-90页 |
| ·本章小结 | 第90-92页 |
| 第五章 无线网络AODV路由协议建模与分析 | 第92-124页 |
| ·AODV路由协议 | 第93-95页 |
| ·建模分析 | 第95-101页 |
| ·路由请求发起操作 | 第101-109页 |
| ·路由请求过程 | 第109-115页 |
| ·性质分析 | 第115-121页 |
| ·网络拓扑结构 | 第121-122页 |
| ·本章小结 | 第122-124页 |
| 第六章 无线网络AODV路由协议验证 | 第124-152页 |
| ·共享变量并行程序的Rely/Guarantee推理规则 | 第125-129页 |
| ·基于共享变量并行程序的AODV模型 | 第129-142页 |
| ·模型基本变量 | 第129-132页 |
| ·路由请求过程 | 第132-135页 |
| ·路由请求 | 第135-139页 |
| ·路由回复 | 第139-142页 |
| ·AODV路由协议性质验证 | 第142-150页 |
| ·本章小结 | 第150-152页 |
| 第七章 总结与展望 | 第152-158页 |
| ·本文工作总结 | 第152-155页 |
| ·后续工作展望 | 第155-158页 |
| 参考文献 | 第158-170页 |
| 致谢 | 第170-173页 |
| 攻读博士学位期间发表论文和科研情况 | 第173-174页 |