基于統(tǒng)計(jì)模型檢測的無線傳感器網(wǎng)絡(luò)協(xié)議建模與分析.pdf

1、隨著無線傳感器技術(shù)的發(fā)展，無線傳感器網(wǎng)絡(luò)(Wireless Sensor Network，WSN)得到極大的關(guān)注。WSN有著廣泛的應(yīng)用場景，在一些危險、不易到達(dá)以及不易生存等情景下，利用無線傳感器（Wireless Sensor）代替人去監(jiān)測、控制目標(biāo)成為自然而然的選擇。這些傳感器之間的通信就必須使用WSN，為了使無線傳感器能達(dá)成監(jiān)測、控制目標(biāo)的目的，WSN協(xié)議必須確保功能的正確性；同時無線傳感器往往資源有限、能量受限，WSN協(xié)議也要考

2、慮性能與功耗問題。為了確保功能正確性，人們通常使用測試與仿真、定理證明以及模型檢測（Model Checking）技術(shù)。測試與仿真無法對系統(tǒng)進(jìn)行全面檢測，定理證明需要過多人工干預(yù)，模型檢測技術(shù)是一種可以自動對系統(tǒng)模型進(jìn)行全面分析的檢測手段，故本文使用模型檢測技術(shù)進(jìn)行建模分析。
　　本文使用統(tǒng)計(jì)模型檢測技術(shù)（Statistical Model Checking，SMC）。傳統(tǒng)的模型檢測技術(shù)由于狀態(tài)空間爆炸問題難以對復(fù)雜系統(tǒng)模型進(jìn)行定

3、量分析，SMC技術(shù)利用統(tǒng)計(jì)學(xué)與仿真手段避免了對整個系統(tǒng)模型狀態(tài)空間的搜索，不會遇到狀態(tài)空間爆炸問題，為性能與功耗的分析提供了新方法。Minimum Cost Forward(MCF)協(xié)議是 WSN網(wǎng)絡(luò)層一種重要的協(xié)議，該協(xié)議使用了基于代價的方法形成最小代價轉(zhuǎn)發(fā)路徑。在此過程中無需存儲路由表，數(shù)據(jù)按照最小代價路徑進(jìn)行傳輸，適用于能量與資源受限的WSN。針對MCF協(xié)議進(jìn)行建模與分析。首先重新建立了MCF協(xié)議的時間自動機(jī)(Timed Auto

4、mata，TA）模型，用時間計(jì)算樹邏輯（Timed Computation Tree Logic，TCTL）語言描訴了協(xié)議的安全性、活性，在模型檢測器UPPAAL上進(jìn)行了驗(yàn)證；然后根據(jù)本文建立的TA模型，用代價時間自動機(jī)(Priced Timed Automata，PTA）對鏈路錯誤以及節(jié)點(diǎn)失效兩種情形進(jìn)行了建模，并用統(tǒng)計(jì)模型檢測的方法分析其定量屬性；除此之外，利用SMC技術(shù)對協(xié)議在無損通信時的功耗進(jìn)行了分析。經(jīng)過分析，發(fā)現(xiàn)在理想情形下