贪婪节点对802.15.4无线传感器网络的影响的形式化建模

10802.15.4无线传感器网络中贪婪节点的形式化建模Youcef Hammal1、Jalel Ben-Othman2、Lynda Mokdad3和Abdelkrim Abdelli11LSI，计算机科学系，USTHB大学，阿尔及利亚2L2TI，加利利研究所，巴黎13大学，法国3LACL，巴黎东大学，法国摘要针对部分节点具有贪婪行为的无线传感器网络（WSN），对非时隙CSMA/CA协议进行了形式化描述。该协议要求传感器节点在发起传输之前等待一段时间，而贪婪节点可能会试图减少它们的等待时间，这可能会惩罚其他节点。来分析它们的影响在无线传感器网络运行模式下，我们使用模型检测器UPPAAL的时间自动机来捕获无线传感器网络中通信介质、理智节点和贪婪节点这使得可以使用分析工具来检查这些模型是否满足预期的属性。索引术语：IEEE 802.15.4; CSMA/CA;形式建模;时间自动机。1. 介绍无线传感器网络（WSN）通常由一组分布在地理区域上的传感器节点组成，用于收集有关物理现象的数据。将用于处理和分析的传感数据传送到控制站是基于节点以多跳方式的协作工作传统上，无线传感器网络面临的最大挑战是由于电源的限制而导致的能量节省。 因此，在WSN以及其他低速率无线个域网（LR-WPAN）中，通信应当遵守严格的时间约束。IEEE 802.15.4协议[4]正是克服这些问题的解决方案，这要归功于它的介质访问控制（MAC）子层。事实上，它采用载波侦听多路访问与冲突避免（CSMA/CA），以减少冲突的可能性，从而减少节点中的能量消耗。注意，基于竞争的MAC可以是时隙或非时隙CSMA/CA，这取决于网络操作行为：分别是信标启用模式或非信标启用模式。与[3]类似，本文旨在使用形式化的用于对与IEEE 802.15.4标准的MAC子层相关的非时隙CSMA/CA协议进行建模和分析的方法，其中，任何站都必须延迟被称为退避延迟的某个时间量，然后在其可以发送其分组之前将介质感测为空闲。这种算法旨在减少冲突并提高传输速率。然而，IEEE 802.15.4 MAC层基于在每个节点上本地执行的分布式算法，用于确定访问信道的时间段。由于在每个设备上执行信道访问，一些贪婪的节点可能会有自私的行为，而不遵守CSMA/CA规则。实际上，贪婪节点修改其IEEE 802.15.4 MAC层的一些参数，以便以牺牲其他节点为代价来增加其带宽。在一个或多个协议中简单更改多个协议参数，一组节点可能对整个网络性能具有破坏性的影响。这些变化甚至类似于拒绝服务（DoS）。因此，为了能够对具有受损节点的WSN进行严格的分析，在本研究中提出了一种正式的规范，以捕获理智和贪婪节点以及无线介质的行为，接收日期：2014年8月22日;修订日期：2014年9月8日接受日期：2014年9月21日* 通讯作者电子邮件：jalel. univ-paris13.fr，电话：+33（1）49 40 28 93这是一个开放获取的文章，根据知识共享署名（CC-BY-NC）许可证的条款，允许在任何媒体上无限制地使用，分发和复制，前提是正确引用原始作品。版权所有©韩国通信与信息科学研究所（KICS），2014http://www.ictexpress.org11http://www.ictexpress.org802.15.4无线传感器网络中贪婪节点的形式化建模NB=0，BE=macMinBE用来作为输入的时间自动机在模型检查工具（例如，UPPAAL[2]）。安全性和活性属性可以通过该工具进行检查，例如没有死锁和成功终止传输。在我们的方法中，贪婪节点可以通过不同的方式增加其对信道的访问。因此，它可以改变几个参数，例如减少退避延迟，在该退避延迟期间，信道必须在其可以被接入之前被感测为空闲，或者/和增加在尝试接入信道时可能需要CSMA/ CA算法退避的次数。2. CSMA/CA协议描述步骤（1）步骤（2）评估）。回退延迟是0和（2BE-1）回退周期之间的随机变量。 CCA表示在接入信道之前必须感测到信道空闲的时段（设置为8个符号）。数量 of backoffs（NB）是在尝试接入信道时调用算法进行回退的次数。在每次新的传输尝试之前将其重置为零。在每个节点中使用先前的参数来控制信道接入。BE允许生成节点在尝试之前必须等待的随机退避持续时间载波检测如果节点有数据要发送，则节点等待随机数量的退避周期，其中退避持续时间在0和（2BE - 1）个周期单位之间。被初始设置为值macMinBE = 3，并且每当退避试验（NB）的计数器增加时，可以增加到最大值aMaxBE = 5。如果信道在CCA期间被感测为空闲，则数据传输开始。如果信道被评估为忙，则NB和BE递增1。可以重复用于分组传输的退避试验，直到NB（退避试验的数量）超过macMaxCSMABackof = 4。步骤（3）步骤（4）N执行CCAY信道无所事事？N步骤（5）NB>3. 贪婪节点贪婪节点的目标是改善其信道访问相对于非妥协节点。因此，这增加了要发送的数据量，代价是可能遭受饥荒情况的未受损节点。例如，贪婪节点在接入信道之前观察到的平均时间可能小于macMaxCSMABackoffs？Y中止发送图1：非时隙CSMA/CA算法。MAC协议支持两种工作模式：主要用于对等拓扑的非信标启用模式和用于其他拓扑的信标启用模式。因此，IEEE 802.15.4定义了CSMA/CA机制的两个版本：（i）时隙CSMA/CA算法-在信标使能模式中使用，以及（ii）非时隙CSMA/CA算法-在非信标使能模式中使用。在这两种情况下，CSMA/CA算法都使用称为回退周期（BP）的基本时间单位，其等于20个符号（其中一个符号对应于发送4比特所需的时间）。非时隙CSMA/CA过程（在图1中给出）取决于以下参数：回退指数（BE）使得能够计算回退延迟，其是执行CCA（空闲信道）之前的时间CCA ， 并 且 退 避 试 验 的 数 量 NB 可 以 增 加 到 大 于macMaxCSMABackof = 4。显然，降低CCA增加了接入信道的机会。另一方面，这也可以增加比正常情况下观察到更多冲突的概率。实际上，将CCA减小到小于RTT的值将增加冲突发生的概率，因为由正常节点发送的信号可能在贪婪节点实现其CCA之后到达贪婪节点。然而，只有当同时访问信道的其他节点的数量很重要时，贪婪节点的冲突才可能增加。由于这些情况不太可能发生，因此在增加接入信道的概率方面的益处优先于经历冲突的风险。此外，考虑到贪婪的行为，碰撞的风险是次要的问题。4. 形式建模语言为了给协议指定一个正式的规范，我们使用模型检查器UPPAAL的建模语言[2]NB = NB + 1BE = min（BE+1，aMaxBE）选择非双时隙CSMA/CA随机（2BE > 1）单位回退周期的延迟12endSend[from]？i++，x：=0误差NB>=maxMacCSMABackoffse：间隔1i== NBR帧结束NB maxMacCSMABackoffs和BE==3回退延迟：=e，x：=0空闲x==FtrDurendSend[st]！x==FtrDuri++，x：=0碰撞x=FtrDuri NBR帧NB：=0，BE：=macMinBEx==CCA_DelayNB++，e：间隔2NB最大MacCSMA退避并且BE==4回退延迟：=e，x：=0e：间隔3NB maxMacCSMABackoffs和BE==5回退延迟：=e，x：=0后退i++，x：=0碰撞？NBRcol++不是wmIdleNB++，BE：=min（BE+1，aMaxBE）x =CCA_Delayx =回退延迟传输x=FtrDurwmIdle发送[st]！x：=0BE：=min（BE+1，aMaxBE）x==CCA_DelaywmIdle：=wmStatus不是wmIdlex==回退延迟wmIdle：=wmStatus，x：=0CCAx =CCA_Delay(a)（b）第（1）款图2：（a）无线介质自动机（b）感测节点的UPPAAL自动机其中系统被视为时间自动机[1]并行地演进，并且每一个都与系统组件中的至少一个相关。时间自动机是一个扩展了时钟变量的扁平有限状态机。它使用密集时间模型，其中时钟变量计算为实数。所有的时钟都同步运行。一个不定时自动机是一个元组A = Q，Q，→，; q0>其中：Q是位置的集合（描绘为图节点），是这个过程可以执行的交互的集合→Q × × Q是位置之间的边的集合，q0是初始位置。然而，组件的设计者可能会在组件与其环境之间可能发生的交互上向其自动机添加时序约束形式上，这种方法包括通过逻辑时钟上的布尔公式来表达时间约束。这些变量表示时间进程，但它们的值可以进行初始化和测试。一个时间自动机用三个映射扩展了一个不定时自动机，如下：第一个映射I给每个位置分配一个称为不变量的逗留条件，这个条件可能是真的。第二映射G向每个边缘分配定时保护，该定时保护应当为真以使边缘被采用。最后，映射Z将每个边沿与一组可能为空的时钟初始化相关联。UPPAAL建模语言由时间自动机组成，进一步扩展了离散常数和有界变量，这些变量在编程语言中使用：const int macMinBE：= 3，aMaxBE：= 5; const intmaxMacCSMABackoffs：= 5;自动机通过二进制同步通道（例如，chan c）。一条标有c的边用另一个标记为c的？如果启用了几个组合，则不确定地选择同步对。在广播同步中，一个发送者使用广播信道冲突！与一个任意数量的接收器冲突？任何可以在当前状态下同步的接收器都必须这样做。数组也可以用于时钟、通道和整数变量，例如chan String send [String s];系统的状态由所有自动机的位置、时钟约束和离散变量的值定义。每个自动机可以单独触发一个边，或者与另一个自动机同步，这导致一个新的状态。5. CSMA/CA规范我们的目标是建立一个无线传感器网络的节点通过共享介质进行通信。我们给出了这些组件的自动机模板：无线介质，正常和受损节点。5.1. 媒介的自动机介质的作用（见图2（a））是在节点之间传播数据包。任何节点的传输都可能干扰其他传输，从而导致冲突。 数据包发送的过程是通过介质之间的两个连续的相互作用来建模的而“以德为先”，就是“以德为先”。endSend[e]？）分别对E的传输的开始和成功终止建模。这两个事件之间的延迟将取决于分组传输的持续时间。这样的时间约束由位置上的不变量x≤ FtrDur来描述。在发送器节点自动机中（其中x是逻辑时钟）。当控制仍然在两者之间的位置时，任何干预传输都会引起冲突（见图2（a））。此外，一旦媒介自动机接收到WISend[e]事件，其状态wmStatus不会立即从空闲切换到繁忙，因为它必须等待wmStatus：=true传播e：idStx =RTD发送[e]？x>=RTDfrom：=e，x：=0wmStatus：碰撞！wmStatus：a：idSt发送[a]？802.15.4无线传感器网络中贪婪节点的形式化建模13http://www.ictexpress.orgRTT延迟。同时，介质被任何查询节点感知为空闲，使得这增加了冲突风险。碰撞！当另一个传输启动时，将引发事件（由endSend [a]？由任何站A触发）在当前传输结束之前（即，endSend[e]？事件尚未收到）。5.2. 健全节点自动机自动机模板（见图2（b））描绘了一个节点ST的传感功能。请注意，它的初始位置是空闲的，如果所有的数据包都已发送，则控制可以从该位置转到结束位置。否则，如果在相同分组的传输周期期间第一次进入测试位置，则控制与初始化为macMinBE值的退避指数BE一起转到测试位置。此后，自动机检查在当前分组的传输期间试验次数NB是否超过阈值maxMacCSMABackoffs。在前一种情况下，控制应转移到错误位置，然后返回到初始位置空闲。否则，控制移动到回退，在回退处，其停 留 等 于回 退 延 迟 。 这 样 的 时 间 约 束 由 位 置BackingOff上的不变量x ≤ BackoffDelay来描绘。根据BE值（由相关弧上的保护所示），从适当的时间间隔（间隔1、间隔2或间隔3）对该延迟进行采样。一旦经过了退避延迟，就执行CCA过程，其中在一定量内感测介质时间了如果感测到忙，则控制移动到测试位置，同时增加试验次数NB和退避指数BE对阈值aMaxBE取模。然而，如果介质在CCA延迟期间持续被感测为空闲，则自动机触发事件“发送[st]！到媒体自动化（对分组传输的开始建模），并且控制转移到传输位置，在传输位置，分组停留等于RTT的延迟。如果发生碰撞，是否有相关事件碰撞？被触发递增，冲突数量NBRcol。这使得控制移动到碰撞位置，并在传输延迟过去后移动到空闲位置。但是，如果endSend[st]！事件在CCA延迟过去之后被触发，则这将意味着成功终止，并且导致控制返回到空闲位置以发送下一个分组。下面是我们使用的一些参数的声明在节点自动机中（图2（b））：int[0; 140] interval1; int[0;300] interval2; int[0; 620]interval3;const int FtrDur：= 100，CCA Delay = 8;bool wmIdle，wmStatus = true; //通道的状态。5.3. 贪婪节点自动机除了正常节点的上述行为之外，受损节点可以使用关于其NB、CCA延迟和退避延迟的假值来增加其根据贪婪行为首先接入介质并发送其分组受损节点具有与正常节点相同的自动机（图2（b）），但由于其使用的延迟和退避次数不同，因此其行为方式不同。我们在下面给出假参数的定义（即，时间间隔和变量）：int[0; 150] interval1; int[0; 150]interval2; int[0; 310] interval3;const int CCA Delay = 4，maxMacCSMABackoffs：= 10;5.4. 全球模拟一 旦 定 义 了 模 板 ， 我 们 就 可 以 通 过 实 例 化CompomisedNode和SaneNode模板来构建整个系统，然后将生成的进程并行组合到一个进程WirelessMedium中，如下所示：node0=SaneNode（0）; node1=SaneNode（1）;. nodeC0=CompromisedNode（0）;.系统无线介质，节点0，节点1，...，nodeC0，.;6. 结论本文提出了一种基于时间自动机的无线传感器网络IEEE802.15.4非时隙CSMA/CA协议建模方法。我们打算在未来的工作中使用模型检查器对我们的模型进行检查预期的属性，并在自动机转换时使用传输事件的概率进行注释。引用[1] R. Alzheimer和D.迪尔时间自动机理论理论计算机科学，126：183-235，Elsevier，1994。[2]G. Behrmann，A.大卫和K.G.拉森A Wendon Uppaal，4thIntl.实时系统设计的形式化方法学派。LNCS 3185，Springer，2004年。[3]Y. Hammal，J. Ben-Othman，L. Mokdad和A.阿卜杜勒Formal Modeling and Verication of an Enhanced Variant oftheIEEE802.11CSMA/CAProtocol ， JournalofCommunications and Networks，16（4），2014年8月。[4]IEEE 802.15.4标准（2003）第15.4部分：用于低速率无线个域网（LR-WPAN）的无线介质访问控制（MAC）和物理层（PHY）规范，IEEE信息技术标准，IEEE-SA标准委员会，2003。