无线传感器网络路由协议实现的静态分析研究

发布时间：2017-08-07 17:02

  本文关键词：无线传感器网络路由协议实现的静态分析研究

  更多相关文章： 无线传感器网络 路由协议 静态分析 WM2RP路由协议 量纲分析

【摘要】：无线传感器网络(wireless sensor networks,WSNs)由于其价格低廉、部署容易、可扩展性强等优点,在环境监测、军事、航空等领域的应用越来越广泛,WSNs路由协议及其实现的正确性也越来越受到人们的重视。一直以来人们主要关注WSNs路由协议的设计、建模与验证,并取得了大量的研究成果。但是,WSNs路由协议实现分析的相关工作却比较少。路由协议设计并实现后需要烧入传感器节点中,即使协议设计没有问题,但由于协议实现代码的不可靠性,并不能保证传感器节点之间的通信按照协议规范进行,因此对WSNs路由协议的实现进行分析是十分必要的。WSNs节点一般都是基于特定传感器的,协议的实现一般为嵌入式程序,而要对节点嵌入式程序进行动态分析比较困难,因此提出用静态分析方法对WSNs路由协议实现进行研究。首先,介绍了WSNs路由协议及其实现特点;然后,提出了WSNs路由协议实现的静态分析框架,又利用该方案分析了企业实际应用的WM2RP路由协议实现代码。具体来说,本文的主要贡献有:(1)分析并归纳了WSNs路由协议及其实现代码的特征,调研比较现有的程序静态分析方法和工具。(2)提出了WSNs路由协议实现的静态分析框架,该框架可以分析通用协议实现代码中的内存错误,也能检查协议实现是否满足协议规范,同时还能分析协议实现代码中的量纲问题。开发了基于KLEE的量纲分析工具,并实现了部分功能。(3)通过对企业实际的WM2RP协议文档及协议实现代码的分析,抽取了WM2RP协议的规范信息,并利用提出的框架对该协议实现进行了分析。分析结果对于WM2RP路由协议的开发者,有很好的参考意义。
【关键词】：无线传感器网络 路由协议 静态分析 WM2RP路由协议 量纲分析
【学位授予单位】：北京工业大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP212.9;TN915.04
【目录】：

• 摘要4-5
• Abstract5-8
• 第1章 绪论8-12
• 1.1 研究背景及意义8
• 1.2 国内外研究现状8-10
• 1.3 研究内容与目标10-11
• 1.4 论文结构11-12
• 第2章 相关背景及技术介绍12-24
• 2.1 WSNs概述12-13
• 2.2 WSNs路由协议13-15
• 2.2.1 WSNs路由协议概述13-14
• 2.2.2 WSNs路由协议的分类14-15
• 2.3 WSNs路由协议实现15-18
• 2.3.1 WSNs路由协议实现概述15-17
• 2.3.2 WSNs路由协议实现的特点17
• 2.3.3 WSNs路由协议实现可能存在的问题17-18
• 2.4 程序静态分析18-19
• 2.5 量纲分析介绍19-23
• 2.5.1 量纲简介19-20
• 2.5.2 WSNs路由协议实现的量纲错误举例20-21
• 2.5.3 量纲分析工具介绍21-23
• 2.6 本章小结23-24
• 第3章 WSNs路由协议实现的静态分析框架24-28
• 3.1 WSNs路由协议实现分析框架24-25
• 3.2 CBMC有界模型检测工具介绍25-26
• 3.2.1 CBMC简介25-26
• 3.2.2 CBMC验证原理与验证性质26
• 3.3 基于KLEE的量纲分析介绍26-27
• 3.3.1 KLEE简介26-27
• 3.3.2 基于KLEE的量纲分析27
• 3.4 本章小结27-28
• 第4章 WM2RP协议实现的静态分析实例28-46
• 4.1 WM2RP协议介绍28-34
• 4.1.1 WM2RP协议简介28-29
• 4.1.2 WM2RP协议的工作时序图29-30
• 4.1.3 WM2RP协议节点的状态图30-32
• 4.1.4 WM2RP协议的通信协议栈32
• 4.1.5 WM2RP协议的数据帧简介32-34
• 4.2 WM2RP协议实现介绍34-38
• 4.2.1 WM2RP协议实现环境简介34
• 4.2.2 WM2RP协议实现代码分类34-35
• 4.2.3 WM2RP协议核心代码介绍35-37
• 4.2.4 WM2RP协议实现的主要模块关系图37-38
• 4.3 检查WM2RP协议实现中的通用内存问题38-40
• 4.3.1 基于CBMC的WM2RP内存问题分析38-39
• 4.3.2 基于CBMC的WM2RP内存分析结果统计39-40
• 4.4 WM2RP协议实现与协议规范性质的分析40-44
• 4.4.1 网络包发送的时序分析40-43
• 4.4.2 表节点等待应答超时性质分析43
• 4.4.3 表节点重发数据帧性质分析43-44
• 4.5 WM2RP协议实现中的量纲问题分析44-45
• 4.6 本章小结45-46
• 第5章 基于KLEE的量纲分析工具实现46-54
• 5.1 基于KLEE的量纲分析框架46-47
• 5.2 相关类图介绍47-49
• 5.3 量纲加法运算处理49-50
• 5.4 量纲分析举例50-51
• 5.5 本章小结51-54
• 结论54-56
• 参考文献56-62
• 攻读硕士学位期间所取得的研究成果62-64
• 致谢64

【参考文献】

中国期刊全文数据库 前1条

1 李梦君;李舟军;陈火旺;;基于抽象解释理论的程序验证技术[J];软件学报;2008年01期

，

本文编号：635711