基于L－π演算的WSN 路由協(xié)議形式化方法

馮曉寧，王 卓，張 旭

（1.哈爾濱工程大學 計算機科學與技術學院，哈爾濱150001；2.哈爾濱工程大學 水下機器人技術國防科技重點實驗室，哈爾濱150001）

0 引 言

由于無線傳感器網絡具有節(jié)點數量大、密度高，計算能力和能量受限等特點，使得無線傳感器網絡的設計面臨著很多挑戰(zhàn)，其中網絡協(xié)議的設計是無線傳感器網絡設計中的關鍵問題之一。將形式化方法引入到無線傳感器網絡路由協(xié)議的設計中，不僅可以嚴密、科學地完成協(xié)議性能和行為的校驗、評判，進而保持網絡協(xié)議的設計質量，而且可以提高協(xié)議的設計、實現(xiàn)、驗證、測試的效率［1］。

目前，形式化方法在無線網絡的不同方面的研究已經取得了進展。在網絡行為的形式化描述方面，Godskesen［2］提 出 了CMAN（Calculus for mobile Ad hoc networks），他將網絡中節(jié)點的通信鏈路描述成雙向通道，并將每個節(jié)點與一個數據結構相關聯(lián)，該數據結構包含了節(jié)點的位置以及鄰居節(jié)點的位置；Merro等［3－4］將節(jié)點的位置與傳輸范圍作為π演算語法的一部分對Ad Hoc網絡進行了形式化的描述。在協(xié)議的形式化研究方面，美國石溪大學的Singh 教授［5］針對Ad Hoc網絡提出了一種形式化方法描述Ad Hoc網絡的通信行為，描述了AODV 路由協(xié)議；Orfanus教授［6］對π演算進行了概率、地理位置擴展，并描述了WSN 的簇頭選擇路由協(xié)議。在節(jié)點通信可靠性方面，Liu［7］在Singh教授的研究理論中加入了概率信息，并分析了Ad Hoc網絡中節(jié)點通信的可靠性問題。2013年，無線網絡的安全性與能量的形式化有了相關的研究。Thong 教授［8］解決了無線傳感器網絡傳輸層協(xié)議的安全性的形式化驗證問題，對π演算進行時間和概率擴展，提出了概率時間演算用于描述與驗證協(xié)議的安全性。最后，基于PAT 過程分析工具提出一種自動的驗證方法驗證了DTSN（Distributed transport for sensor networks）協(xié)議。在能量方面，Gallina等［9］從能量和網絡連通性的關系形式化分析了Ad Hoc網絡協(xié)議和性質。首先根據Ad Hoc網絡的節(jié)點廣播范圍受限和移動性的特點擴展π演算，將節(jié)點的通信行為與傳輸半徑相關聯(lián)，提出了E－BUM 演算。通過調節(jié)節(jié)點通信半徑的大小來表現(xiàn)能量控制。最后利用E－BUM 證明網絡的連通性質，用于減少通信的干擾并分析能量管理策略。

現(xiàn)有的形式化方法從不同角度形式化分析與驗證了無線網絡的性質，但是沒有一套推理規(guī)則指導網絡路由協(xié)議的形式化推導。因此，本文根據無線傳感器網絡節(jié)點通信范圍受限的特點，提出一種形式化方法用于描述與驗證無線傳感器網絡路由協(xié)議。

1 L－π演算

π演算是由Robin Milner等人創(chuàng)建的一種進程代數，用于描述結構跟隨計算而變化的并發(fā)進程計算模型。它語義嚴格并提供了很強的理論分析支持。但是，π演算不能充分地描述無線傳感器網絡節(jié)點通信范圍受限的特點，例如在SPIN協(xié)議初始階段，只有鄰居節(jié)點才可以收到發(fā)送節(jié)點的ADV 廣告幀。因此，本文擴展了π 演算的表達式，提出了一種新的形式化方法：L－π 演算，并從節(jié)點的層次上定義了L－π演算的語法、結構同余和遷移規(guī)則。

1.1 L－π演算的語法

定義1（L－π演算表達式） 用大寫字母M 表示無線傳感器網絡節(jié)點，P、Q、R 表示節(jié)點內執(zhí)行的進程，L 表示節(jié)點的鄰居列表，對任意節(jié)點M，可形式化地定義為：

0表示處于非活動狀態(tài)的節(jié)點；M｜M 表示兩個節(jié)點的并行；！M 表示若干個節(jié)點的并行執(zhí)行；［P］L表示節(jié)點執(zhí)行的進程為P，它的鄰居節(jié)點列表為L。P 為π 演算的進程表達式［10］，它的形式如下：

定義2（L－π演算動作） 設有無限名字集合N 并且x，y，z∈N，L－π演算的動作集合可定義為：

1.2 L－π演算的結構同余

結構同余反映了節(jié)點表達式的非順序性，給出了不同的節(jié)點表達式間的結構等價關系。

定義3（L－π演算的結構同余） 設無限名字集合N（且x，y，z∈N）表示節(jié)點內執(zhí)行的進程，L 表示節(jié)點的鄰居列表，用符號“＝”表示兩個節(jié)點結構同余關系，定義的結構同余如下：

（1）［P］L≡［P］L｜0

該式定義了節(jié)點與非活動節(jié)點并行時結構等價。

該式定義了兩個節(jié)點并行時滿足交換律，表達式中節(jié)點不受順序的影響，即并行表達式中順序不同的節(jié)點在結構上等價。

該式定義了多個節(jié)點在并行復合時滿足結合律。

該式定義了節(jié)點存在受囿名字時的等價關系，fn（P）表示進程P 的自由名字集合。

該式定義了節(jié)點并行表達式中存在受囿名字時的等價關系。

（6）（vx）（vy）［P］L≡（vy）（vx）［P］L

該式定義了節(jié)點表達式存在多個受囿名字時，節(jié)點表達式不受受囿名字的順序的影響，它們結構等價。

該式定義了若兩個節(jié)點表達式經過換名操作后結構等價，那么兩個節(jié)點表達式結構同余。

該式定義了在鄰居節(jié)點列表相同的情況下，若兩個節(jié)點內執(zhí)行的進程結構同余，那么兩個節(jié)點也具有結構同余的關系。

1.3 L－π演算的遷移規(guī)則

遷移規(guī)則定義了節(jié)點的基本行為的演化規(guī)則，可以從基于行為的“靜態(tài)”描述進行行為的動態(tài)推演，為L－π形式化驗證無線傳感器路由協(xié)議提供了推理依據。

定義4（L－π 演算的遷移規(guī)則） 令M、N 表示網絡中的節(jié)點，P、Q、R 表示節(jié)點內執(zhí)行的進程，x，y，z表示進程中的名字，α表示L－π演算中的動作，L－π演算的遷移規(guī)則如下：

（1）結構規(guī)則（STRUCT）：

該規(guī)則規(guī)定了若節(jié)點M 與N 結構同余、節(jié)點M 執(zhí)行動作α后變?yōu)镸′并且節(jié)點M′與N′結構同余，那么節(jié)點N 執(zhí)行動作α可以演化為節(jié)點N′。

（2）并行規(guī)則（PAR）：

該規(guī)則規(guī)定了如果節(jié)點M 在動作α 的受囿名字不屬于節(jié)點N 的自由名字集合的情況下，執(zhí)行動作α后演化為節(jié)點M′，那么并行執(zhí)行的節(jié)點M｜N 可以在執(zhí)行動作α 后演化為M′｜N。在無線傳感器網絡中，節(jié)點間的并行可能存在信息的交互，也可能不存在。該規(guī)則通過條件bn（α）∩fn（N）＝? 限定了節(jié)點間不存在信息交互時并行節(jié)點間的行為，下面的廣播通信規(guī)則（MCOM）、單播通信規(guī)則（UNI－COM）以及封閉規(guī)則（UNI－CLOSE）定義了節(jié)點間存在交互時并行節(jié)點間的行為。

（3）廣播規(guī)則（MCAST）：

該規(guī)則規(guī)定了節(jié)點執(zhí)行的進程若有廣播動作前綴，那么該節(jié)點會執(zhí)行廣播動作然后演化為節(jié)點［P］L。這里用來表示執(zhí)行廣播節(jié)點的鄰居節(jié)點列表非空。在無線傳感器網絡中，若一個節(jié)點的鄰居節(jié)點列表為空，那么該節(jié)點成為孤立節(jié)點，廣播也就沒有任何意義。

（4）接收規(guī)則（RECV）：

該規(guī)則表示在任何條件下，［（rec（x）.P］L執(zhí)行了rec（x）動作后變?yōu)楣?jié)點［P］L。在無線傳感器網絡中，只要節(jié)點處在發(fā)送節(jié)點的發(fā)送范圍內，節(jié)點就可以執(zhí)行接收動作，因此在該規(guī)則中接收動作沒有關聯(lián)它的鄰居節(jié)點列表。

（5）廣播組合規(guī)則（MCOM）：

（6）單播發(fā)送規(guī)則（UNI－SEND）：

（7）單播接收規(guī)則（UNI－RECV）：

該規(guī)則規(guī)定了節(jié)點M 可以在任何條件下執(zhí)行單播接收動作z（x），并演化為節(jié)點M′。與廣播接收規(guī)則類似，若節(jié)點處在發(fā)送節(jié)點鄰居列表中，它便可以接收到發(fā)送節(jié)點單播發(fā)送的消息，因此沒有關聯(lián)它的鄰居列表。

（8）單播組合規(guī)則（UNI－COM）：

（9）開放規(guī)則（UNI－OPEN）：

（9）封閉規(guī)則（UNI－CLOSE）：

該規(guī)則規(guī)定若節(jié)點M 在通道z 上單播發(fā)送它的受囿名字，節(jié)點N 存在于節(jié)點M 的鄰居列表中并且可以在通道z 上執(zhí)行接收動作，那么當節(jié)點M 與N 并行時，節(jié)點M 的受囿名字的作用范圍會擴大到節(jié)點N。

2 基于L－π演算無線傳感器網絡路由協(xié)議描述

分層協(xié)議是無線傳感器網絡中一類重要的協(xié)議，它解決了平面路由協(xié)議中的網絡功耗分布不均、擴展性弱的問題。在分層協(xié)議中最重要的就是簇頭選擇過程，它為簇的形成階段以及后續(xù)的數據傳輸階段奠定了基礎。本文利用L－π演算形式化描述一種選取最大剩余能量的簇頭選擇協(xié)議［11］。

2.1 協(xié)議流程介紹

該協(xié)議的流程下：

（1）簇頭選擇發(fā)起節(jié)點（initNode）發(fā)起簇頭選擇過程，廣播選擇簇頭消息（election message）消息到鄰居節(jié)點，隨后等待來自鄰居節(jié)點的確認消息（ack message）。

（2）鄰居節(jié)點收到election message消息后記錄該消息的發(fā)送者并將其作為父節(jié)點，重復步驟（1）的動作。最后，收到簇頭選擇消息的節(jié)點會構成一個以簇頭發(fā)起節(jié)點為根的樹。

（3）收到election message消息的節(jié)點將其剩余能量作為確認消息發(fā)送到父節(jié)點，最終匯聚到發(fā)起節(jié)點。最后由發(fā)起節(jié)點廣播最大剩余能量的節(jié)點作為簇頭的消息（leader message）。

圖1 簇頭選擇協(xié)議中的消息流Fig.1 Message flow in leader election protocol

對應該過程的消息流圖如圖1所示，E 表示簇頭選擇消息（election message）、A 表示確認消息（ack message）、L 表 示 簇 頭 消 息（leader message）。

2.2 簇頭選擇協(xié)議的形式化描述

為了描述上的方便，將形式化描述中參數定義為下述7元組：

id 是節(jié)點的唯一標識；chan 表示節(jié)點與子節(jié)點的通道名稱；pchan 表示節(jié)點與父節(jié)點的通道名稱；init標識節(jié)點是否為發(fā)起節(jié)點，1表示為發(fā)起節(jié)點，反之為0；elec 表示節(jié)點是否處在簇頭選擇過程，1表示參加，反之為0；energy 表示節(jié)點當前的能量值；maxenergy 表示節(jié)點已知的最大能量值。

根據簇頭選擇協(xié)議流程，本文將網絡中的節(jié)點分為普通節(jié)點 （node）與發(fā)起節(jié)點（initNode）。node的進程描述為：node＝rec（X）.［X ＝election］processElection（id，chan，pchan，init，1，energy，maxenergy）＋rec（leader（X））.processLeader（id，chan，pchan，init，elec，energy，X）

普通節(jié)點（node）或者等待父節(jié)點發(fā)起簇頭選擇的消息，然后將參數elec 置為1，并執(zhí)行簇頭選擇過程processElection，或者等待父節(jié)點發(fā)送的當選簇頭的廣播消息，然后執(zhí)行processLeader過程。processElection 的描述為：

在該狀態(tài)中節(jié)點會非確定地選擇下述三種情況執(zhí)行：①若節(jié)點的init為0，說明該節(jié)點為普通節(jié)點，那么它通過與父節(jié)點的通道單播發(fā)送（ack message）消息以及它已知的最大能量發(fā)送到父節(jié)點，并進入node 狀態(tài)；②若節(jié)點的init 為1，說明節(jié)點為發(fā)起節(jié)點（initNode），此時它需要廣播應成為簇頭節(jié)點的id 到其鄰居節(jié)點，并將elec 的值置為0，以標示退出選擇過程，然后進入node狀態(tài)；節(jié)點還有可能收到子節(jié)點發(fā)送的（ack message）以及子節(jié)點已知的最大能量值，節(jié)點將參數maxenergy 用收到的最大能量值替換并進入 對 （ack message）消 息 確 認 的 狀 態(tài)processAck，processAck 的描述為：

在該狀態(tài)中，若節(jié)點已知的最大能量大于它本身的能量，節(jié)點保存這個信息并返回（awaitAck）狀態(tài)；否則，節(jié)點會用本身的能量值替換maxenergy 參數，然后返回（awaitAck）狀態(tài)。

node 進程中還有processLeader 過程，它的描述為：

整個簇頭選擇過程是由發(fā)起節(jié)點（initNode）觸發(fā)的，它的描述為：

它負責廣播發(fā)送election 消息，然后進入等待狀態(tài)。

至此，簇頭選擇協(xié)議的L－π 演算描述完成。若有圖1所示的網絡拓撲結構，那么簇頭選擇協(xié)議在該網絡中對應的L－π描述為：

M ＝ ［initNode（1，1，null，1，0，1，1）］（2，3）｜［node（2，2，1，0，0，2，2）］（1，4，5）｜［node（3，3，1，0，0，3，3）］（1，6，7）｜［node（4，4，2，0，0，4，4）］（2）｜［node（5，5，2，0，0，5，5）］（5）｜［node（4，4，2，0，0，4，4）］（3）｜［node（7，7，3，0，0，7，7）］（3）

初始時刻節(jié)點并不知道其他節(jié)點的剩余能量，故將節(jié)點已知的最大能量初始化為它的剩余能量；由于發(fā)起節(jié)點沒有父節(jié)點，故其pchan 的值為null。

3 基于L－π演算的無線傳感器網絡路由協(xié)議驗證

3.1 實驗環(huán)境

實驗環(huán)境為MMC［12］（Mobile model check）和SPIN（Simple promela interpreter）模型檢測工具。MMC 是用于對π 演算建模進行驗證的工具，它的運行環(huán)境為Linux，以兩個文件（一個規(guī)則庫文件和一個待檢測模型文件）作為輸入，通過命令查詢得到模型運行到終止狀態(tài)經過的狀態(tài)數；SPIN 是一個協(xié)議分析的輔助工具，利用它可以得出模型在到達終止狀態(tài)經歷的狀態(tài)數和對應該過程的消息序列圖MSC（Message sequence chart）。

3.2 實驗方法

首先獲得模型在MMC 軟件與SPIN 軟件運行下達到終止狀態(tài)經歷的狀態(tài)數，然后對比兩種環(huán)境下狀態(tài)數是否一致，最后查看模型的MSC圖判斷消息是否到達目標節(jié)點。若上述兩個條件均滿足，那么就可以驗證L－π演算是有效的。

運行MMC需要在規(guī)則庫中加入L－π演算的廣播動作，該文件用Prolog語言編寫，如圖2 所示。單播規(guī)則與廣播規(guī)則類似，在此不再敘述。規(guī)則中謂詞basic（P，L）表示節(jié)點，P、L 分別代表進程和鄰居節(jié)點列表；pref（P，Q）表示P、Q 是前綴關系；trans（M，A，N）表示節(jié)點M 經過執(zhí)行動作A 演化為節(jié)點N；contain（L，N）表示節(jié)點N 在集合L中。

圖2 MMC中加入的廣播規(guī)則Fig.2 Broadcast rules in MMC

3.3 協(xié)議驗證

驗證的無線傳感器路由協(xié)議為第2 節(jié)中用L－π演算描述的簇頭選擇協(xié)議，采用的網絡拓撲結構為圖1所示的樹形拓撲結構，分別驗證了網絡中節(jié)點數為5、6、7、8時模型達到終止狀態(tài)經歷的狀態(tài)數。

表1列出了在不同節(jié)點數的情況下，模型在MMC中到達終止狀態(tài)經歷的狀態(tài)數，同時列出了該協(xié)議在SPIN 工具中達到終止狀態(tài)經歷的狀態(tài)數。由表中數據可知，隨著節(jié)點數的增加，模型經歷的狀態(tài)數也增加；在不同的模型檢測環(huán)境中，當網絡拓撲結構、節(jié)點數相同時，得到的狀態(tài)數一致。

表1 MMC和SPIN 得到的狀態(tài)數對比Table 1 State comparison in MMC and SPIN

同時，給出了網絡中節(jié)點數為7時簇頭選擇協(xié)議在SPIN 工具中運行，運行結果表明用L－π演算形式化描述的簇頭選擇路由協(xié)議正確，L－π演算有效。

4 結束語

本文提出了一種描述無線傳感器網絡路由協(xié)議的形式化方法L－π演算，該方法在π演算中加入了鄰居列表的結構，描述了無線傳感器網絡節(jié)點通信范圍受限的特性，在π演算的動作集合中加入了廣播動作，描述了節(jié)點的廣播通信行為；從節(jié)點的層次上定義的結構同余描述了不同節(jié)點表達式間的等價關系；定義的遷移規(guī)則可以動態(tài)地推演節(jié)點的行為，并用L－π演算形式化描述了無線傳感器網絡節(jié)點的通信行為。最后，通過在不同的模型檢測工具中驗證L－π演算描述的無線傳感器網絡簇頭選擇協(xié)議，得到了模型在不同的節(jié)點數的情況下到達終止狀態(tài)經歷的狀態(tài)數一致的結果，并且達到了目標狀態(tài)，說明了該方法能夠有效地描述與驗證無線傳感器網絡的路由協(xié)議。

［1］孫利民，李建中，陳渝，等.無線傳感器網絡［M］.北京：清華大學出版社，2009.

［2］Godskesen J C.A calculus for mobile ad hoc networks［C］∥Coordination Models and Languages.Springer Berlin Heidelberg，2007：132－150.

［3］Merro M.An observational theory for mobile ad hoc networks［J］.Electronic Notes in Theoretical Computer Science，2007，173：275－293.

［4］Mezzetti N，Sangiorgi D.Towards a calculus for wireless systems［J］.Electronic Notes in Theoretical Computer Science，2006，158：331－353.

［5］Singh A，Ramakrishnan C R，Smolka S A.A process calculus for mobile ad hoc networks［J］.Science of Computer Programming，2010，75（6）：440－469.

［6］Orfanus D，Heimfarth T，Wagner F R.Process algebra to model Self－Organizing behavior in wireless sensor networks［C］∥Ultra Modern Telecommunications ＆Workshops，2009.ICUMT＇09.International Conference on，IEEE，2009：1－6.

［7］Liu S，Zhao Y，Zhu H，et al.A calculus for mobile Ad Hoc networks from a group probabilistic Perspective［C］∥High－Assurance Systems Engineering（HASE），2011IEEE 13th International Symposium on.IEEE，2011：157－162.

［8］Thong V T，Buttyán L，Dvir A.On formal and automatic security verification of WSN transport protocols［J］.International Scholarly Research Notices，2014：891467.

［9］Gallina L，Rossi S.A process calculus for energy‐aware multicast communications of mobile ad hoc networks［J］.Wireless Communications and Mobile Computing，2013，13（3）：296－312.

［10］Milner R.通信與移動系統(tǒng)［M］.林惠民，柳欣欣，劉佳，等譯.北京：清華大學出版社，2009：88.

［11］Vasudevan S，Kurose J，Towsley D.Design and analysis of a leader election algorithm for mobile ad hoc networks［C］∥Network Protocols，2004，ICNP，2004，Proceedings of the 12th IEEE International Conference on.IEEE，2004：350－360.

［12］Yang P，Dong Y，Ramakrishnan C R，et al.A Provably correct Compiler for Efficient Model Checking of Mobile Processes［M］.Practical Aspects of Declarative Languages.Springer Berlin Heidelberg，2005：113－127.