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

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

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

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

【參考文獻(xiàn)】

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

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

，

本文編號：635711