基于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.