基于L-π演算的WSN路由协议形式化方法

引用本文

冯晓宁, 王卓, 张旭. 基于L-π演算的WSN路由协议形式化方法. 2015, 45(5): 1565-1571
FENG Xiao-ning, WANG Zhuo, ZHANG Xu. Formal method for routing protocol of WSN based on L-π calculus. Journal of Jilin University Engineering and Technology Edition, 2015, 45(5): 1565-1571 复制到剪切板

Permissions

基于L-π演算的WSN路由协议形式化方法

冯晓宁¹, 王卓², 张旭¹

1.哈尔滨工程大学计算机科学与技术学院,哈尔滨 150001

2.哈尔滨工程大学水下机器人技术国防科技重点实验室,哈尔滨150001

作者简介:冯晓宁(1976-),男,副教授.研究方向:建模与仿真,无线传感器网络,并行计算.E-mail:fengxiaoning@hrbeu.edu.cn

基金:国家自然科学基金项目(61100006,61272184); 黑龙江省自然科学基金项目(F201129)

摘要

针对无线传感器网络路由协议形式化描述与验证的问题,提出了一种形式化方法L-π演算。定义了L-π演算的语法,形式化描述无线传感器节点的广播与单播的通信行为。定义了相应的结构同余,描述了节点表达式的非顺序性。定义了相应的迁移规则,提供了路由协议形式化模型的动态推演功能。通过对无线传感器网络簇头选择协议的描述展现了L-π演算的能力。通过无线传感器网络簇头选择协议的验证实验说明了该方法能有效验证无线传感网络路由协议。

关键词: 计算机软件; 无线传感器网络; 路由协议; 形式化方法; L-π演算

中图分类号:TP393 文献标志码:A 文章编号:1671-5497(2015)05-1565-07

Formal method for routing protocol of WSN based on L-π calculus

FENG Xiao-ning¹, WANG Zhuo², ZHANG Xu¹

1.College of Computer Science and Technology, Harbin Engineering University, Harbin 150001,China

2.National Key Laboratory of Science and Technology on Autonomous Underwater Vehicle, Harbin Engineering University, Harbin 150001, China

Abstract

A process calculus called L-π calculus was proposed to solve the issue of formal specification and verification for Wireless Sensor Network (WSN) routing protocol. The calculus can capture the characteristics of WSN, including the limit transmission range and broadcast communication. The defined syntax of the L-π calculus describes the network from the perspective of node. Structural congruence defined in L-π describes the non-sequential of node expression. Transitional rules of L-π calculus in terms of labeled transition systems are also defined to provide the function of dynamic deduction. After the definition of L-π calculus, a leader election protocol is described to demonstrate the description ability of the calculus. Finally, the calculus is illustrated by developing and analyzing formal models of the leader election protocol for WSN.

Keyword: computer software; wireless sensor network; routing protocol; formal method; L-π calculus

Show Figures

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, 可形式化地定义为:

M::=0|M|M|!M|[P]_L

0表示处于非活动状态的节点; M|M表示两个节点的并行; !M表示若干个节点的并行执行; [P]_L表示节点执行的进程为P, 它的邻居节点列表为L。P为π 演算的进程表达式^[10], 它的形式如下:

P::= $\begin{matrix} \sum_{i \in I} \end{matrix}$ α _i.P_i|(P₁|P₂)|(vx)P|!P|[x=y]P|0

式中: $\begin{matrix} \sum_{i \in I} \end{matrix}$ α _i.P_i表示先选择执行一个动作α _i, 然后执行进程P_i; (P₁|P₂)表示两个进程P₁和P₂并行执行; (vx)P表示名字x是进程P的受囿名字; !P表示进程P的复制, 用来表示若干个进程P的并行执行; [x=y]P表示若匹配条件成立, 则执行进程P, 否则演化为空进程; 0表示一个空进程, 不具有任何行为。

定义2(L-π 演算动作) 设有无限名字集合N并且x, y, z∈ N, L-π 演算的动作集合可定义为:

α ::=< $\begin{matrix} \bar{bro} \end{matrix}$ x, L> |rec(x)|< $\begin{matrix} \bar{x} \end{matrix}$ y, L> |x(y)|τ

< $\begin{matrix} \bar{bro} \end{matrix}$ x, L> 和rec(x)分别代表广播发送与接收。无线传感器网络中, 节点不仅具有单播行为, 而且具有广播行为。例如, 在信息协商传感协议初始阶段, 节点需要广播ADV广告帧告知邻居节点有数据要转发, 收到该广告帧的节点需要对此作出响应。因此, 在π 演算的动作集合中加入了一对互补的动作< $\begin{matrix} \bar{bro} \end{matrix}$ x, L> 和rec(x)表示广播发送与接收, 并且在广播动作< $\begin{matrix} \bar{bro} \end{matrix}$ x, L> 中, 只有在邻居节点列表L内的节点才可以接收到消息; < $\begin{matrix} \bar{x} \end{matrix}$ y, L> 与x(y)是一对互补动作, 分别表示单播发送与接收动作, 并且在单播发送动作< $\begin{matrix} \bar{x} \end{matrix}$ y, L> 中, 只有在邻居节点列表L内的节点才可以收到消息; τ 表示节点的内部行为, 外界不可见。

1.2 L-π 演算的结构同余

结构同余反映了节点表达式的非顺序性, 给出了不同的节点表达式间的结构等价关系。

定义3(L-π 演算的结构同余) 设无限名字集合N(且x, y, z∈ N)表示节点内执行的进程, L表示节点的邻居列表, 用符号“ =” 表示两个节点结构同余关系, 定义的结构同余如下:

(1)[P]_L≡ [P]_L|0

该式定义了节点与非活动节点并行时结构等价。

(2) $\begin{matrix} [P_{1}]_{L_{1}} \end{matrix}$ | $\begin{matrix} [P_{2}]_{L_{2}} \end{matrix}$ ≡ $\begin{matrix} [P_{2}]_{L_{2}} \end{matrix}$ | $\begin{matrix} [P_{1}]_{L_{1}} \end{matrix}$

该式定义了两个节点并行时满足交换律, 表达式中节点不受顺序的影响, 即并行表达式中顺序不同的节点在结构上等价。

(3)([P₁ $\begin{matrix} ]_{L_{1}} \end{matrix}$ | $\begin{matrix} [P_{2}]_{L_{2}} \end{matrix}$ )| $\begin{matrix} [P_{3}]_{L_{3}} \end{matrix}$ ≡ [P₁ $\begin{matrix} ]_{L_{1}} \end{matrix}$ |( $\begin{matrix} [P_{2}]_{L_{2}} \end{matrix}$ | $\begin{matrix} [P_{3}]_{L_{3}} \end{matrix}$ )

该式定义了多个节点在并行复合时满足结合律。

(4)(vx)[P]_L≡ [P]_L, if x∉fn(P)

该式定义了节点存在受囿名字时的等价关系, fn(P)表示进程P的自由名字集合。

(5)(vx) $\begin{matrix} [P_{1}]_{L_{1}} \end{matrix}$ | $\begin{matrix} [P_{2}]_{L_{2}} \end{matrix}$ ≡ (vx)( $\begin{matrix} [P_{1}]_{L_{1}} \end{matrix}$ | $\begin{matrix} [P_{2}]_{L_{2}} \end{matrix}$ ), if x∉fn(P₂)

该式定义了节点并行表达式中存在受囿名字时的等价关系。

(6)(vx)(vy)[P]_L≡ (vy)(vx)[P]_L

该式定义了节点表达式存在多个受囿名字时, 节点表达式不受受囿名字的顺序的影响, 它们结构等价。

(7) $\begin{matrix} [P_{1}]_{L_{1}} \end{matrix}$ ≡ $\begin{matrix} [P_{2}]_{L_{2}} \end{matrix}$ , if[P₁ $\begin{matrix} ]_{L_{1}} \end{matrix}$ ≡ _α $\begin{matrix} [P_{2}]_{L_{2}} \end{matrix}$

该式定义了若两个节点表达式经过换名操作后结构等价, 那么两个节点表达式结构同余。

(8) $\begin{matrix} [P_{1}]_{L} \end{matrix}$ ≡ $\begin{matrix} [P_{2}]_{L} \end{matrix}$ , if P₁≡ P₂

该式定义了在邻居节点列表相同的情况下, 若两个节点内执行的进程结构同余, 那么两个节点也具有结构同余的关系。

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):

bn(α )∩ fn(N)=∅

该规则规定了如果节点M在动作α 的受囿名字不属于节点N的自由名字集合的情况下, 执行动作α 后演化为节点M', 那么并行执行的节点M|N可以在执行动作α 后演化为M'|N。在无线传感器网络中, 节点间的并行可能存在信息的交互, 也可能不存在。该规则通过条件bn(α )∩ fn(N)=∅限定了节点间不存在信息交互时并行节点间的行为, 下面的广播通信规则(MCOM)、单播通信规则(UNI-COM)以及封闭规则(UNI-CLOSE)定义了节点间存在交互时并行节点间的行为。

(3)广播规则(MCAST):

L≠ ∅

该规则规定了节点执行的进程若有广播动作前缀, 那么该节点会执行广播动作< $\begin{matrix} \bar{bro} \end{matrix}$ x, L> 然后演化为节点[P]_L。这里用L≠ ∅来表示执行广播节点的邻居节点列表非空。在无线传感器网络中, 若一个节点的邻居节点列表为空, 那么该节点成为孤立节点, 广播也就没有任何意义。

(4)接收规则(RECV):

该规则表示在任何条件下, [(rec(x).P]_L执行了rec(x)动作后变为节点[P]_L。在无线传感器网络中, 只要节点处在发送节点的发送范围内, 节点就可以执行接收动作, 因此在该规则中接收动作没有关联它的邻居节点列表。

(5)广播组合规则(MCOM):

该规则表示若节点M执行广播动作< $\begin{matrix} \bar{bro} \end{matrix}$ x, L> 后演化为节点M', 并且N_i存在于M的邻居节点列表中, 它可以执行rec(x)动作演化为节点N', 那么节点并行M|∏ N_i可以执行动作< $\begin{matrix} \bar{bro} \end{matrix}$ x, L> 后演化为节点M'|∏ N'_i{x/y}, 其中∏ N_i等价于N₁|N₂|…|N_n。

(6)单播发送规则(UNI-SEND):

L≠ ∅

该规则规定了节点M可以在任何条件下执行单播发送动作< $\begin{matrix} \bar{z} \end{matrix}$ x, L> , 并演化为节点M', 与广播规则类似, M的邻居节点列表L非空。

(7)单播接收规则(UNI-RECV):

该规则规定了节点M可以在任何条件下执行单播接收动作z(x), 并演化为节点M'。与广播接收规则类似, 若节点处在发送节点邻居列表中, 它便可以接收到发送节点单播发送的消息, 因此没有关联它的邻居列表。

(8)单播组合规则(UNI-COM):

该规则规定了若节点M执行单播动作< $\begin{matrix} \bar{z} \end{matrix}$ x, L> 演化为节点M', 并且节点N存在于M的邻居节点列表中, 它可以执行接收动作z(x)演化为节点N', 那么节点M|N执行动作τ 后演化为节点M'|N'{x/y}。

(9)开放规则(UNI-OPEN):

x≠ z

该规则规定了节点M可以将它的受囿名字x在通道z上单播发送出去, 那么x的作用范围将扩大到其他节点。

(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)。

	Figure Option View Download New Window
	图1 簇头选择协议中的消息流Fig.1 Message flow in leader election protocol

对应该过程的消息流图如图1所示, E表示簇头选择消息(election message)、A表示确认消息(ack message)、L表示簇头消息(leader message)。

2.2 簇头选择协议的形式化描述

为了描述上的方便, 将形式化描述中参数定义为下述7元组:

$\begin{matrix} \begin{matrix} \vec{a} = \\ {id, c h an, pc h an, init, elec, energy, maxenergy} \end{matrix} \end{matrix}$

id是节点的唯一标识; chan表示节点与子节点的通道名称; pchan表示节点与父节点的通道名称; init标识节点是否为发起节点, 1表示为发起节点, 反之为0; elec表示节点是否处在簇头选择过程, 1表示参加, 反之为0; energy表示节点当前的能量值; maxenergy表示节点已知的最大能量值。

根据簇头选择协议流程, 本文将网络中的节点分为普通节点(node)与发起节点(initNode)。node( $\begin{matrix} \vec{a} \end{matrix}$ )的进程描述为:

node( $\begin{matrix} \vec{a} \end{matrix}$ )=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的描述为:

$\begin{matrix} processElection (\vec{a}) = \bar{bro} election . awaitAck (\vec{a}) \end{matrix}$

(maxenergy)).node( $\begin{matrix} \vec{a} \end{matrix}$ )+[init=1] $\begin{matrix} \bar{bro} \end{matrix}$

(leader(energy)).node(id, chan, pchan, init, 0, energy, maxenergy)

processLeader( $\begin{matrix} \vec{a} \end{matrix}$ )=

[maxenergy==energy](

[elec=1] $\begin{matrix} \bar{bro} \end{matrix}$ (leader(maxenergy)).

node(id, chan, pchan, init, 0, energy, maxenergy)+

[elec=0]node(id, chan, pchan, init, 0, energy, maxenergy))+

[maxenergy> energy] $\begin{matrix} \bar{bro} \end{matrix}$ (leader(maxenergy)).

node(id, chan, pchan, init, 0, maxenergy, maxenergy)+

[maxenergy< energy] $\begin{matrix} \bar{bro} \end{matrix}$ (leader(energy)).

node(id, chan, pchan, init, 0, energy, energy)

整个簇头选择过程是由发起节点(initNode)触发的, 它的描述为:

至此, 簇头选择协议的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)]₍₂₎|

[node(5, 5, 2, 0, 0, 5, 5)]₍₅₎|[node(4, 4, 2, 0, 0, 4, 4)]₍₃₎|

[node(7, 7, 3, 0, 0, 7, 7)]₍₃₎

初始时刻节点并不知道其他节点的剩余能量, 故将节点已知的最大能量初始化为它的剩余能量; 由于发起节点没有父节点, 故其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-π 演算是有效的。

	Figure Option View Download New Window
	图2 MMC中加入的广播规则Fig.2 Broadcast rules in MMC

运行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中。

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-π 演算描述的无线传感器网络簇头选择协议, 得到了模型在不同的节点数的情况下到达终止状态经历的状态数一致的结果, 并且达到了目标状态, 说明了该方法能够有效地描述与验证无线传感器网络的路由协议。

该过程负责广播 election消息,然后进入等待确认消息的状态 awaitAck, awaitAck的描述为:

awaitAck(a→) =

chan( ack( Y)) .processAck( id, chan, pchan, init,

elec, energy, Y,) +[ init=0]pchan(¯ ack

在该状态中节点会非确定地选择下述三种情况执行:①若节点的 init为0,说明该节点为普通节点,那么它通过与父节点的通道单播发送( ack message)消息以及它已知的最大能量发送到父节点,并进入 node状态;②若节点的 init为1,说明节点为发起节点( initNode),此时它需要广播应成为簇头节点的 id到其邻居节点,并将 elec的值置为0,以标示退出选择过程,然后进入 node状态;节点还有可能收到子节点发送的( ack message)以及子节点已知的最大能量值,节点将参数 maxenergy用收到的最大能量值替换并进入对( ack message)消息确认的状态 processAck, processAck的描述为:

processAck(a→) =

[ maxenergy>=energy] awaitAck(a→) +

[ maxenergy<energy]

awaitAck( id, chan, pchan, init, elec, energy, energy)

在该状态中,若节点已知的最大能量大于它本身的能量,节点保存这个信息并返回( awaitAck)状态;否则,节点会用本身的能量值替换 maxenergy参数,然后返回( awaitAck)状态。

node进程中还有 processLeader过程,它的描述为:

initNode(a→) =bro¯ election.awaitAck(a→)

它负责广播发送 election消息,然后进入等待状态。

The authors have declared that no competing interests exist.

参考文献

View Option

[1]	孙利民, 李建中, 陈渝, 等. 无线传感器网络[M]. 北京: 清华大学出版社, 2009. [本文引用:1]
[2]	Godskesen J C. A calculus for mobile ad hoc networks[C]∥Coordination Models and Languages. Springer Berlin Heidelberg, 2007: 132-150. [本文引用:1]
[3]	Merro M. An observational theory for mobile ad hoc networks[J]. Electronic Notes in Theoretical Computer Science, 2007, 173: 275-293. [本文引用:1]
[4]	Mezzetti N, Sangiorgi D. Towards a calculus for wireless systems[J]. Electronic Notes in Theoretical Computer Science, 2006, 158: 331-353. [本文引用:1]
[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. [本文引用:1]
[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. [本文引用:1]
[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), 2011 IEEE 13th International Symposium on. IEEE, 2011: 157-162. [本文引用:1]
[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. [本文引用:1]
[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. [本文引用:1]
[10]	Milner R. 通信与移动系统[M]. 林惠民, 柳欣欣, 刘佳, 等译. 北京: 清华大学出版社, 2009: 88. [本文引用:1]
[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. [本文引用:1]
[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. [本文引用:1]

2009

0.0

. 2009, :- DOI:doi:10.3969/j.issn.1671-7597.2009.21.054

孙利民, 李建中, 陈渝

摘　要：无线传感器网络的问世和潜在应用前景,大有引发一场新技术革命的势头。无线传感器网络已成为IT领域的热点研究方向。通过对无线传感器网络的基本概念和结构的介绍,对拓扑控制、网络协议等关键技术进行列举。

... 将形式化方法引入到无线传感器网络路由协议的设计中,不仅可以严密、科学地完成协议性能和行为的校验、评判,进而保持网络协议的设计质量,而且可以提高协议的设计、实现、验证、测试的效率^[1] ...

2007

0.0

... 在网络行为的形式化描述方面,Godskesen^[2]提出了CMAN(Calculus for mobile Ad hoc networks),他将网络中节点的通信链路描述成双向通道,并将每个节点与一个数据结构相关联,该数据结构包含了节点的位置以及邻居节点的位置 ...

2007

0.0

... Merro等^[3,4]将节点的位置与传输范围作为#cod#x003c0 ...

2006

0.0

... Merro等^[3,4]将节点的位置与传输范围作为#cod#x003c0 ...

2010

0.0

... 在协议的形式化研究方面,美国石溪大学的Singh教授^[5]针对Ad Hoc网络提出了一种形式化方法描述Ad Hoc网络的通信行为,描述了AODV路由协议 ...

2009

0.0

... Orfanus教授^[6]对#cod#x003c0 ...

2011

0.0

... 在节点通信可靠性方面,Liu^[7]在Singh教授的研究理论中加入了概率信息,并分析了Ad Hoc网络中节点通信的可靠性问题 ...

2014

0.0

... Thong教授^[8]解决了无线传感器网络传输层协议的安全性的形式化验证问题,对#cod#x003c0 ...

2013

0.0

... 在能量方面,Gallina等^[9]从能量和网络连通性的关系形式化分析了Ad Hoc网络协议和性质 ...

2009

0.0

... 演算的进程表达式^[10],它的形式如下: ...

2004

0.0

... 演算形式化描述一种选取最大剩余能量的簇头选择协议^[11] ...

2005

0.0

... 1 实验环境实验环境为MMC^[12](Mobile model check)和SPIN(Simple promela interpreter)模型检测工具 ...