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

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

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

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

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