无线传感器网络中基于APMC的MAC协议分析与性能评估

理论计算机科学电子笔记185（2007）33-46www.elsevier.com/locate/entcs基于APMCMichaüelCadilhac1 ThomasH′erault2RichardLasaigne3SylvainPeyronnet1，3S′ebastienTixeuil2摘要在本文中，我们提出了一个无线传感器网络的MAC（媒体访问控制）协议的分析。该协议的目的是通过构建时分媒体接入（TDMA）调度来管理无线媒体接入。APMC（Approximate Probability Model）是一种使用基于近似的验证技术来分析复杂概率系统行为的工具。使用APMC，我们近似计算了所研究的MAC协议的几个属性的概率，从而给出了一些关于它的性能的见解。关键词：无线传感器网络，近似验证1引言无线传感器网络是使用大量嵌入了处理器、传感器、执行器和无线电通信能力的机器的网络。这些网络通常用于环境监测和资产跟踪。单个节点通常以自组织方式部署，因此它们必须组织起来形成多跳无线通信网络[18]。这种自组织无线网络中的主要问题是对通信介质的访问，因为相邻节点之间的同时无线传输导致混淆交换的消息的冲突。冲突管理和避免是无线网络协议中的基本问题，介质访问控制（MAC）协议是解决这个问题的分布式解决方案在文献[4]中，Busch，Magdon-Ismail，Sivrikaya和Yener提出了一种用于传感器网络的MAC协议。该协议提供了许多有趣的属性：1个EPITA研究&开发实验室（{cadilhac| peyronnet}@ lrde.epita.fr）2 巴黎大学Xi，INRIA Grand-Large（{herault| tixeuil}@ lri.fr）3法国国家科学研究中心巴黎第七大学逻辑设备部（lassaign@logique.jussieu.fr）1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.02734M. Cadilhac等人/理论计算机科学电子笔记185（2007）33保证了分配给每个节点的带宽，它是完全分布式的，并且不需要全局时钟的存在。为了分析分布式协议的正确性和性能，可以采用多种方法。其中之一是概率模型检验，这是一类用于验证概率系统的定量属性的算法方法。 这些方法中的大多数都是基于系统的数学模型的构建和在一些时态语言中的规范的表达。这个模型代表了系统所有可能的组态，以及这些状态之间可能发生的转换的概率。评估要检查的时间属性的满意概率的问题，被减少到状态空间上的线性方程组的系统的分辨率。然而，由于在建模步骤中的状态空间爆炸现象，转移矩阵的表示可以是如此之大，验证变得棘手。为了克服这一现象，符号和数值方法已被引入PRISM等工具中[14]。 在过去的几年里，出现了一种完全不同的模型检测技术：近似概率模型检测。使用这种技术，我们可以近似计算模型满足规范的概率[10]。使用这种方法，计算时间不一定会降低，但内存消耗变得非常低（或在某些情况下保持不变）。实际上，该方法的空间复杂度与模型的大小我们在本文中提出的结果是双重的：我们为无线传感器网络建立了一个复杂的无竞争MAC协议模型[4]，并使用该模型进行了各种实验因此，我们使用近似概率模型检测的传感器网络协议的验证和分析的兴趣本文的结构如下。在第3节中，我们回顾了近似概率验证的框架然后，我们简要地描述了[4]的MAC协议（第4节）和它的建模（第5节）。最后，第6节给出了使用APMC对我们的模型进行的几个实验的结果2相关工作现在为传感器[26]和小型设备[5]设想的网络需要节能、可扩展性、对瞬时故障的容忍性以及对拓扑变化的适应性。传感器网络基本上存在两种MAC算法[24]：(i) 基于竞争的协议：节点竞争共享信道，导致概率协调，例如ALOHA [2]和载波侦听多路访问（CSMA [13]）。CSMA协议已被广泛研究和扩展，并且是广泛使用的标准（例如IEEE 802.11 [1]）的核心(ii) 调度协议：节点协作以规划通信，从而不发生冲突。该方案可以基于在调制解调 器 中 广 泛 使 用 的 频 率 （ FDMA ， 频 分 多 址 ） 、 码 （ CDMA ） 或 时 间（TDMA）。M. Cadilhac等人/理论计算机科学电子笔记185（2007）3335无线通信系统[20]。实质上，通过在虚拟子信道中调度通信来避免冲突，所述虚拟由于虚拟子信道不相互干扰，因此该组中的MAC协议基本上是无冲突的。时分多址（TDMA）是一种合理的技术管理无线媒体接入，但可扩展性和容错性的优先事项并没有被大多数以前的研究强调。最近对传感器网络典型的无线电传输特性的分析[9]表明，与随机冲突避免协议相比，TDMA可能并不总是显著提高带宽，但公平性和节能考虑仍然是重要的动机。在具有可预测的通信模式的应用中，传感器甚至可以在TDMA时隙期间关闭无线电接收器，在TDMA时隙中不期望消息在专门为传感器网络设计的TDMA协议中，[11，12]在理论和实践上都进行了研究（以获得定量测量），而[4]中提出的相当复杂的协议仅通过手工研究，特别是没有提供定量分析。近似概率模型检验方法领域的研究相当年轻，除了我们的方法之外，在[25]中，描述了一种基于Monte-Carlo模拟和统计假设检验来验证离散事件系统属性的过程。在[22]中，提出了一种用于黑箱概率系统的模型检查的统计方法。这些方法通过使用统计假设检验而不是随机近似方案，与我们的方法有很大的最近，在[8]中，给出了表示为LTL公式的安全特性的概率模型检验的随机化算法在另一种方法[19]中，随机测试和抽象解释都用于C程序的验证。只有少数尝试已经在验证通信协议使用近似为基础的模型检查。例如，APMC已经在[7，6]中用于此目的。使用概率模型检验对通信协议进行形式化验证已经做我们可以提到PRISM团队的工作（例如，见[15，16]）。3近似概率验证和APMC在本节中，我们回顾了近似概率验证的框架，并快速介绍了工具APMC（近似概率模型验证）。APMC基于随机算法，通过使用系统执行路径的采样来近似时间规范36M. Cadilhac等人/理论计算机科学电子笔记185（2007）33通用近似算法GAA输入：图、k、θ、δ输出：Probk的近似值[]N：=1n（2）/2ε2;A：δ对于i= 1到N，做A：=A+随机路径（图，k，k）返回Y=A/N3.1型号和规格APMC的近似方法可以处理任何支持执行路径生成的概率系统。输入语言与PRISM相同，并允许以模块化的方式描述离散时间或连续时间马尔可夫链。该语言可以表达时态逻辑公式的满足概率。设M是一个离散时间马尔可夫链，s是一个初始状态，时态逻辑公式我们用Path（s）表示第一个状态为s的执行路径的集合。集合Path（s）上的概率测度Prob是经典定义的，我们用Prob[k]表示满足公式k的路径集合的测度。设Pathk（s）是从s开始的所有长度为k >0的路径的集合，Probk[k]是Pathk（s）中满足k的使用APMC的近似方法，我们可以近似，以任何程度的精度，时间公式的满意概率。在下一小节中，为了清楚起见，我们只考虑有界时间属性（即有限路径的属性），并描述一个近似Probk[k]的随机算法。3.2近似验证为了用随机算法来估计有界属性k的概率p，我们生成路径k（s）的随机路径，并计算一个估计p=Probk[k]的随机变量X。我们说一个估计X是ε-好的意思是如果算法的输出值在[p−ε，p+ε]中。定义3.1p的随机近似方案（RAS）是一个随机的算法Athattakes asai puttoa rees entationof thethesystem，a. property∈，两个实数ε，δ>0并产生值X，使得：Pr X∈[p−ε，p+ε] ≥1−δ。如果A的运行时间是k，1和log（1）的多项式，则称A为ε δ是完全多项式的。概率Pr是在算法的随机选择上采用的。在多个样本多项式之后，近似是ε-好的，置信度为（1−δ）在1和log（1）。主要优点是，为了设计路径生成器，我们ε δ只需要使用简洁的表示来模拟系统的行为它的名字叫《易经》。APMC的通用近似算法如下。其中，函数Random Path为：M. Cadilhac等人/理论计算机科学电子笔记185（2007）3337随机路径输入：图，k，k输出：对长度为k的路径π进行采样，并检查π上的公式(i) 生成一个长度为k的随机路径π（图中）(ii) 如果 在π上为真，则返回1，否则返回0在[17]中，证明了GAA是计算p=Probk[k]的完全多项式RAS，只要k是有界时间性质且0