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

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

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

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