基于π演算的WSN路由協(xié)議形式化驗(yàn)證的方法研究.pdf

1、集成了計(jì)算機(jī)技術(shù)、通信技術(shù)、半導(dǎo)體技術(shù)的無(wú)線傳感器網(wǎng)絡(luò)能夠根據(jù)用戶的需求對(duì)各種監(jiān)測(cè)對(duì)象進(jìn)行實(shí)時(shí)的信息采集、處理，具有非常廣泛的應(yīng)用前景，對(duì)擴(kuò)寬人類的認(rèn)知領(lǐng)域、改變?nèi)祟愓J(rèn)知方式有巨大的推動(dòng)作用。與傳統(tǒng)的網(wǎng)絡(luò)相比，無(wú)線傳感器網(wǎng)絡(luò)有一些獨(dú)有的特點(diǎn)，網(wǎng)絡(luò)的節(jié)點(diǎn)數(shù)量大、面向任務(wù)、大規(guī)模自組網(wǎng)、安全性較差、以數(shù)據(jù)為中心，能量受限等，上述這些問題使無(wú)線傳感器網(wǎng)絡(luò)的設(shè)計(jì)面臨著諸多問題。其中，通信協(xié)議的設(shè)計(jì)是無(wú)線傳感器網(wǎng)絡(luò)中的關(guān)鍵問題之一。形式化方法在無(wú)

2、線傳感器網(wǎng)絡(luò)路由協(xié)議的設(shè)計(jì)中不但可以提高協(xié)議的開發(fā)效率，而且有助于精確地完成性能的分析和性質(zhì)的驗(yàn)證，改善網(wǎng)絡(luò)協(xié)議的設(shè)計(jì)質(zhì)量。
　　本文根據(jù)無(wú)線傳感器節(jié)點(diǎn)通信范圍受限的特性，對(duì)π演算進(jìn)行擴(kuò)展，提出一種能夠描述與驗(yàn)證無(wú)線傳感器網(wǎng)絡(luò)路由協(xié)議的形式化方法，L-π演算。為了能夠在節(jié)點(diǎn)層次上描述無(wú)線傳感器網(wǎng)絡(luò)的通信行為，本文定義了L-π演算的表達(dá)式，在基本π演算的語(yǔ)法中加入了鄰居節(jié)點(diǎn)列表；定義了L-π演算的動(dòng)作集合，加入了廣播動(dòng)作描述節(jié)點(diǎn)的廣

3、播通信行為。其次，為了定義不同節(jié)點(diǎn)表達(dá)式間的等價(jià)關(guān)系，在節(jié)點(diǎn)層次上定義了結(jié)構(gòu)同余規(guī)則，定義了節(jié)點(diǎn)間結(jié)構(gòu)同余的轄域律，交換律，浮動(dòng)律；為了規(guī)定節(jié)點(diǎn)間的交互行為，定義了節(jié)點(diǎn)間的轉(zhuǎn)換規(guī)則。重新論證了節(jié)點(diǎn)間的強(qiáng)模擬、基于結(jié)構(gòu)同余的強(qiáng)模擬以及弱模擬理論，利用互模擬理論分析與驗(yàn)證了無(wú)線傳感器網(wǎng)絡(luò)的性質(zhì)。最后，利用L-π演算描述了無(wú)線傳感器網(wǎng)絡(luò)路由協(xié)議中的信息傳感協(xié)議和簇頭選擇協(xié)議，通過實(shí)驗(yàn)驗(yàn)證了利用L-π描述的上述協(xié)議的正確性，分析了實(shí)驗(yàn)的優(yōu)點(diǎn)與不