本文關(guān)鍵詞：無(wú)線傳感器網(wǎng)絡(luò)路由協(xié)議實(shí)現(xiàn)的靜態(tài)分析研究

  更多相關(guān)文章： 無(wú)線傳感器網(wǎng)絡(luò) 路由協(xié)議 靜態(tài)分析 WM2RP路由協(xié)議 量綱分析

【摘要】：無(wú)線傳感器網(wǎng)絡(luò)(wireless sensor networks,WSNs)由于其價(jià)格低廉、部署容易、可擴(kuò)展性強(qiáng)等優(yōu)點(diǎn),在環(huán)境監(jiān)測(cè)、軍事、航空等領(lǐng)域的應(yīng)用越來(lái)越廣泛,WSNs路由協(xié)議及其實(shí)現(xiàn)的正確性也越來(lái)越受到人們的重視。一直以來(lái)人們主要關(guān)注WSNs路由協(xié)議的設(shè)計(jì)、建模與驗(yàn)證,并取得了大量的研究成果。但是,WSNs路由協(xié)議實(shí)現(xiàn)分析的相關(guān)工作卻比較少。路由協(xié)議設(shè)計(jì)并實(shí)現(xiàn)后需要燒入傳感器節(jié)點(diǎn)中,即使協(xié)議設(shè)計(jì)沒(méi)有問(wèn)題,但由于協(xié)議實(shí)現(xiàn)代碼的不可靠性,并不能保證傳感器節(jié)點(diǎn)之間的通信按照協(xié)議規(guī)范進(jìn)行,因此對(duì)WSNs路由協(xié)議的實(shí)現(xiàn)進(jìn)行分析是十分必要的。WSNs節(jié)點(diǎn)一般都是基于特定傳感器的,協(xié)議的實(shí)現(xiàn)一般為嵌入式程序,而要對(duì)節(jié)點(diǎn)嵌入式程序進(jìn)行動(dòng)態(tài)分析比較困難,因此提出用靜態(tài)分析方法對(duì)WSNs路由協(xié)議實(shí)現(xiàn)進(jìn)行研究。首先,介紹了WSNs路由協(xié)議及其實(shí)現(xiàn)特點(diǎn);然后,提出了WSNs路由協(xié)議實(shí)現(xiàn)的靜態(tài)分析框架,又利用該方案分析了企業(yè)實(shí)際應(yīng)用的WM2RP路由協(xié)議實(shí)現(xiàn)代碼。具體來(lái)說(shuō),本文的主要貢獻(xiàn)有:(1)分析并歸納了WSNs路由協(xié)議及其實(shí)現(xiàn)代碼的特征,調(diào)研比較現(xiàn)有的程序靜態(tài)分析方法和工具。(2)提出了WSNs路由協(xié)議實(shí)現(xiàn)的靜態(tài)分析框架,該框架可以分析通用協(xié)議實(shí)現(xiàn)代碼中的內(nèi)存錯(cuò)誤,也能檢查協(xié)議實(shí)現(xiàn)是否滿足協(xié)議規(guī)范,同時(shí)還能分析協(xié)議實(shí)現(xiàn)代碼中的量綱問(wèn)題。開(kāi)發(fā)了基于KLEE的量綱分析工具,并實(shí)現(xiàn)了部分功能。(3)通過(guò)對(duì)企業(yè)實(shí)際的WM2RP協(xié)議文檔及協(xié)議實(shí)現(xiàn)代碼的分析,抽取了WM2RP協(xié)議的規(guī)范信息,并利用提出的框架對(duì)該協(xié)議實(shí)現(xiàn)進(jìn)行了分析。分析結(jié)果對(duì)于WM2RP路由協(xié)議的開(kāi)發(fā)者,有很好的參考意義。
【關(guān)鍵詞】：無(wú)線傳感器網(wǎng)絡(luò) 路由協(xié)議 靜態(tài)分析 WM2RP路由協(xié)議 量綱分析
【學(xué)位授予單位】：北京工業(yè)大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2015
【分類(lèi)號(hào)】：TP212.9;TN915.04
【目錄】：

• 摘要4-5
• Abstract5-8
• 第1章 緒論8-12
• 1.1 研究背景及意義8
• 1.2 國(guó)內(nèi)外研究現(xiàn)狀8-10
• 1.3 研究?jī)?nèi)容與目標(biāo)10-11
• 1.4 論文結(jié)構(gòu)11-12
• 第2章 相關(guān)背景及技術(shù)介紹12-24
• 2.1 WSNs概述12-13
• 2.2 WSNs路由協(xié)議13-15
• 2.2.1 WSNs路由協(xié)議概述13-14
• 2.2.2 WSNs路由協(xié)議的分類(lèi)14-15
• 2.3 WSNs路由協(xié)議實(shí)現(xiàn)15-18
• 2.3.1 WSNs路由協(xié)議實(shí)現(xiàn)概述15-17
• 2.3.2 WSNs路由協(xié)議實(shí)現(xiàn)的特點(diǎn)17
• 2.3.3 WSNs路由協(xié)議實(shí)現(xiàn)可能存在的問(wèn)題17-18
• 2.4 程序靜態(tài)分析18-19
• 2.5 量綱分析介紹19-23
• 2.5.1 量綱簡(jiǎn)介19-20
• 2.5.2 WSNs路由協(xié)議實(shí)現(xiàn)的量綱錯(cuò)誤舉例20-21
• 2.5.3 量綱分析工具介紹21-23
• 2.6 本章小結(jié)23-24
• 第3章 WSNs路由協(xié)議實(shí)現(xiàn)的靜態(tài)分析框架24-28
• 3.1 WSNs路由協(xié)議實(shí)現(xiàn)分析框架24-25
• 3.2 CBMC有界模型檢測(cè)工具介紹25-26
• 3.2.1 CBMC簡(jiǎn)介25-26
• 3.2.2 CBMC驗(yàn)證原理與驗(yàn)證性質(zhì)26
• 3.3 基于KLEE的量綱分析介紹26-27
• 3.3.1 KLEE簡(jiǎn)介26-27
• 3.3.2 基于KLEE的量綱分析27
• 3.4 本章小結(jié)27-28
• 第4章 WM2RP協(xié)議實(shí)現(xiàn)的靜態(tài)分析實(shí)例28-46
• 4.1 WM2RP協(xié)議介紹28-34
• 4.1.1 WM2RP協(xié)議簡(jiǎn)介28-29
• 4.1.2 WM2RP協(xié)議的工作時(shí)序圖29-30
• 4.1.3 WM2RP協(xié)議節(jié)點(diǎn)的狀態(tài)圖30-32
• 4.1.4 WM2RP協(xié)議的通信協(xié)議棧32
• 4.1.5 WM2RP協(xié)議的數(shù)據(jù)幀簡(jiǎn)介32-34
• 4.2 WM2RP協(xié)議實(shí)現(xiàn)介紹34-38
• 4.2.1 WM2RP協(xié)議實(shí)現(xiàn)環(huán)境簡(jiǎn)介34
• 4.2.2 WM2RP協(xié)議實(shí)現(xiàn)代碼分類(lèi)34-35
• 4.2.3 WM2RP協(xié)議核心代碼介紹35-37
• 4.2.4 WM2RP協(xié)議實(shí)現(xiàn)的主要模塊關(guān)系圖37-38
• 4.3 檢查WM2RP協(xié)議實(shí)現(xiàn)中的通用內(nèi)存問(wèn)題38-40
• 4.3.1 基于CBMC的WM2RP內(nèi)存問(wèn)題分析38-39
• 4.3.2 基于CBMC的WM2RP內(nèi)存分析結(jié)果統(tǒng)計(jì)39-40
• 4.4 WM2RP協(xié)議實(shí)現(xiàn)與協(xié)議規(guī)范性質(zhì)的分析40-44
• 4.4.1 網(wǎng)絡(luò)包發(fā)送的時(shí)序分析40-43
• 4.4.2 表節(jié)點(diǎn)等待應(yīng)答超時(shí)性質(zhì)分析43
• 4.4.3 表節(jié)點(diǎn)重發(fā)數(shù)據(jù)幀性質(zhì)分析43-44
• 4.5 WM2RP協(xié)議實(shí)現(xiàn)中的量綱問(wèn)題分析44-45
• 4.6 本章小結(jié)45-46
• 第5章 基于KLEE的量綱分析工具實(shí)現(xiàn)46-54
• 5.1 基于KLEE的量綱分析框架46-47
• 5.2 相關(guān)類(lèi)圖介紹47-49
• 5.3 量綱加法運(yùn)算處理49-50
• 5.4 量綱分析舉例50-51
• 5.5 本章小結(jié)51-54
• 結(jié)論54-56
• 參考文獻(xiàn)56-62
• 攻讀碩士學(xué)位期間所取得的研究成果62-64
• 致謝64

【參考文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前1條

1 李夢(mèng)君;李舟軍;陳火旺;;基于抽象解釋理論的程序驗(yàn)證技術(shù)[J];軟件學(xué)報(bào);2008年01期

，

本文編號(hào)：635711