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

馮曉寧，王 卓，張 旭

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

0 引 言

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

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

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

1 L－π演算

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

1.1 L－π演算的語法

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

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

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

1.2 L－π演算的結構同余

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

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

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

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

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

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

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

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

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

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

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

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

1.3 L－π演算的遷移規則

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

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

（1）結構規則（STRUCT）：

該規則規定了若節點M 與N 結構同余、節點M 執行動作α后變為M′并且節點M′與N′結構同余，那么節點N 執行動作α可以演化為節點N′。

（2）并行規則（PAR）：

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

（3）廣播規則（MCAST）：

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

（4）接收規則（RECV）：

該規則表示在任何條件下，［（rec（x）.P］L執行了rec（x）動作后變為節點［P］L。在無線傳感器網絡中，只要節點處在發送節點的發送范圍內，節點就可以執行接收動作，因此在該規則中接收動作沒有關聯它的鄰居節點列表。

（5）廣播組合規則（MCOM）：

（6）單播發送規則（UNI－SEND）：

（7）單播接收規則（UNI－RECV）：

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

（8）單播組合規則（UNI－COM）：

（9）開放規則（UNI－OPEN）：

（9）封閉規則（UNI－CLOSE）：

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

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

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

2.1 協議流程介紹

該協議的流程下：

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

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

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

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

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

2.2 簇頭選擇協議的形式化描述

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

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

根據簇頭選擇協議流程，本文將網絡中的節點分為普通節點 （node）與發起節點（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）

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

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

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

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

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

它負責廣播發送election 消息，然后進入等待狀態。

至此，簇頭選擇協議的L－π 演算描述完成。若有圖1所示的網絡拓撲結構，那么簇頭選擇協議在該網絡中對應的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）

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

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

3.1 實驗環境

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

3.2 實驗方法

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

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

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

3.3 協議驗證

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

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

表1 MMC和SPIN 得到的狀態數對比Table 1 State comparison in MMC and SPIN

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

4 結束語

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

［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.通信與移動系統［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.