本文關(guān)鍵詞：基于統(tǒng)計模型檢測的無線傳感器網(wǎng)絡(luò)協(xié)議建模與分析，由筆耕文化傳播整理發(fā)布。

【摘要】：隨著無線傳感器技術(shù)的發(fā)展,無線傳感器網(wǎng)絡(luò)(Wireless Sensor Network,WSN)得到極大的關(guān)注。WSN有著廣泛的應(yīng)用場景,在一些危險、不易到達以及不易生存等情景下,利用無線傳感器(Wireless Sensor)代替人去監(jiān)測、控制目標(biāo)成為自然而然的選擇。這些傳感器之間的通信就必須使用WSN,為了使無線傳感器能達成監(jiān)測、控制目標(biāo)的目的,WSN協(xié)議必須確保功能的正確性；同時無線傳感器往往資源有限、能量受限,WSN協(xié)議也要考慮性能與功耗問題。為了確保功能正確性,人們通常使用測試與仿真、定理證明以及模型檢測(Model Checking)技術(shù)。測試與仿真無法對系統(tǒng)進行全面檢測,定理證明需要過多人工干預(yù),模型檢測技術(shù)是一種可以自動對系統(tǒng)模型進行全面分析的檢測手段,故本文使用模型檢測技術(shù)進行建模分析。為了對性能與功耗進行分析,本文使用統(tǒng)計模型檢測技術(shù)(Statistical Model Checking,SMC)。傳統(tǒng)的模型檢測技術(shù)由于狀態(tài)空間爆炸問題難以對復(fù)雜系統(tǒng)模型進行定量分析,SMC技術(shù)利用統(tǒng)計學(xué)與仿真手段避免了對整個系統(tǒng)模型狀態(tài)空間的搜索,不會遇到狀態(tài)空間爆炸問題,為性能與功耗的分析提供了新方法。Minimum Cost Forward(MCF)協(xié)議是WSN網(wǎng)絡(luò)層一種重要的協(xié)議,該協(xié)議使用了基于代價的方法形成最小代價轉(zhuǎn)發(fā)路徑。在此過程中無需存儲路由表,數(shù)據(jù)按照最小代價路徑進行傳輸,適用于能量與資源受限的WSN。本文針對MCF協(xié)議進行建模與分析。首先重新建立了MCF協(xié)議的時間自動機(Timed Automata, TA)模型,用時間計算樹邏輯(Timed Computation Tree Logic,TCTL)語言描訴了協(xié)議的安全性、活性,在模型檢測器UPPAAL上進行了驗證；然后根據(jù)本文建立的TA模型,用代價時間自動機(Priced Timed Automata,PTA)對鏈路錯誤以及節(jié)點失效兩種情形進行了建模,并用統(tǒng)計模型檢測的方法分析其定量屬性；除此之外,本文還利用SMC技術(shù)對協(xié)議在無損通信時的功耗進行了分析。經(jīng)過分析,發(fā)現(xiàn)在理想情形下,MCF協(xié)議可以完成WSN的路由,但是不能均衡地消耗WSN中的能量,同時在進行有損通信時,MCF協(xié)議無法有效進行數(shù)據(jù)傳輸。
【關(guān)鍵詞】：無線傳感器網(wǎng)絡(luò) 時間自動機 代價時間自動機 模型檢測 統(tǒng)計模型檢測
【學(xué)位授予單位】：鄭州大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TP212.9;TN929.5
【目錄】：

• 摘要4-5
• Abstract5-11
• 1 緒論11-18
• 1.1 研究背景11-12
• 1.2 研究現(xiàn)狀12-14
• 1.3 相關(guān)工作14-16
• 1.4 論文概述16-18
• 2 預(yù)備知識18-30
• 2.1 數(shù)學(xué)知識18-19
• 2.1.1 參數(shù)估計18-19
• 2.1.2 假設(shè)檢驗19
• 2.2 時間自動機19-20
• 2.3 時間分支計算樹邏輯20-21
• 2.4 基于時間自動機的模型檢查21-22
• 2.5 代價時間自動機及其網(wǎng)絡(luò)22-25
• 2.6 概率權(quán)重時間分支計算樹邏輯25-26
• 2.7 統(tǒng)計模型檢測26-27
• 2.8 Minimum Cost Forward協(xié)議27-29
• 2.9 本章小結(jié)29-30
• 3 MCF協(xié)議建模30-39
• 3.1 MCF協(xié)議的TA模型30-35
• 3.2 MCF協(xié)議的PTA模型35-38
• 3.2.1 MCF協(xié)議在鏈路錯誤情形下的PTA模型35-37
• 3.2.2 MCF協(xié)議在節(jié)點失效情形下的PTA模型37-38
• 3.3 本章小結(jié)38-39
• 4 MCF協(xié)議分析39-50
• 4.1 MCF協(xié)議的時間自動機模型分析40-41
• 4.2 MCF協(xié)議的性能分析41-47
• 4.3 MCF協(xié)議能耗分析47-49
• 4.4 本章小結(jié)49-50
• 5 總結(jié)與展望50-51
• 5.1 總結(jié)50
• 5.2 展望50-51
• 參考文獻51-55
• 個人簡歷、在學(xué)期間參加的科研項目及發(fā)表的論文55-56
• 個人簡歷55
• 在學(xué)期間參加的科研項目55
• 在學(xué)期間發(fā)表的學(xué)術(shù)論文55-56
• 致謝56

【參考文獻】

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

1 史新宏,蔡伯根,穆建成;智能交通系統(tǒng)的發(fā)展[J];北方交通大學(xué)學(xué)報;2002年01期

2 巫細波;楊再高;;智慧城市理念與未來城市發(fā)展[J];城市發(fā)展研究;2010年11期

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前1條

1 李倩;采用概率模型檢測技術(shù)對無線傳感網(wǎng)絡(luò)聚簇協(xié)議的分析[D];山東大學(xué);2012年

  本文關(guān)鍵詞：基于統(tǒng)計模型檢測的無線傳感器網(wǎng)絡(luò)協(xié)議建模與分析，，由筆耕文化傳播整理發(fā)布。

本文編號：353556