无线网状网络的双图反应系统建模

沙特国王大学学报无线Mesh网络的共享双图反应系统建模Rachida Boucebsi女士，Faiza Belala*LIRE实验室，康斯坦丁第二大学-Abdelhamid Mehri，Nouvelle ville Ali Mendjeli BP：67 A，康斯坦丁，阿尔及利亚阿提奇莱因福奥文章历史记录：接收日期：2018年2018年10月19日修订2018年10月30日接受在线发售2018年保留字：WMNS多路径路由双向反应式系统形式验证模型检查器A B S T R A C T近年来，各种类型的无线网络和移动通信技术已经出现;特别是无线网状网络（WMN）显著地提高了移动通信的容量。本文的目的是提出一种新的建模方法，WMN的理论方面的新见解。我们依靠正式的方法来展示如何定义一个精确的语义WMN和如何正式分析其路由协议。我们结合Maude语言的逻辑反射和双向反应系统（BRS）的层次结构，为WMN提供了一个可执行的形式化模型该模型称为Bis-WMN，它既规定了WMN拓扑结构，也规定了在路由过程中可以观察到的任何行为。然后用Maude的LTL模型检查器检查了一些固有特性。©2018作者制作和主办：Elsevier B.V.代表沙特国王大学这是一CC BY-NC-ND许可下的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。1. 介绍在过去的几十年中，已经做出了很大的努力来解决一些主要的传统（有线或无线）网络的挑战，随着互联网用户数量的增加，大量的网络资源等，这样的网络的性能不能满足用户在成本和吞吐量方面的要求。因此，出现了一类新的网络，称为无线网状网络（WMN），并且由于其灵活性、易于部署和最小化的成本而构成了对通信的令人愉快的支持。此外，它们还为具有各种服务质量要求的各种应用提供了通信手段，例如延迟，吞吐量，可靠性，机密性等。由于Mesh路由器（MR）的独立组织和多跳通信能力，WMN被部署在广泛的应用场景中，包括城市、郊区和农村的互联网接入，应急响应通信，*通讯作者。电 子 邮 件 地 址 ： rachida. univ-constantine2.dz （ R.Boucebsi ） ， faiza.belala@univ-constantine2.dz（F. Belala）。沙特国王大学负责同行审查公共安全、楼宇自动化和智能交通系统。WMN拓扑，如图所示。 1的无线接入点由多个基站无线接入点MR和移动客户端节点组成。路由器构成多跳无线骨干网，通过多跳通信，MR可以以比传统路由器低得多的传输功率达到相同的覆盖范围在骨干网内，路由器的子集可以充当包括若干接入网络的网关，如经由高速有线链路在普通互联网网络中观察到的因此，WMN部署可以覆盖广泛的网络区域。几种无线技术支持这种类型的通信，IEEE802.11（用于无线局域网WLAN）、IEEE802.15.4（用于无线个域网WPAN）和IEEE802.16（用于无线城域网WMAN）。为了提高WMN的灵活性，MR通常配备有在相同或不同的无线接入 技 术 （ IEEE 802.11a/b/g 频 带 ） 上 操 作 的 多 个 网 络 接 口 卡（Network Interface Card，NIC）。此外，无线Mesh路由器可以使用不同的信道并行通信，因此，WMN可以是一个多接口多信道无线Mesh网络（MIMC-WMN）。实际上，在相同信道上的同时传输可能引起冲突并导致吞吐量下降，因此，WMN面临的主要挑战是干扰，干扰是直接影响在相同区域中以及在相似或融合信道上发生的通信的不期望的现象，从而减少了传输速率。https://doi.org/10.1016/j.jksuci.2018.10.0161319-1578/©2018作者。制作和主办：Elsevier B.V.代表沙特国王大学这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。制作和主办：Elsevier可在ScienceDirect上获得目录列表沙特国王大学学报杂志首页：www.sciencedirect.com1072R. Boucebsi，F.Belala/沙特国王大学学报Fig. 1. WMN架构。网络容量。因此，使用多个信道和多个无线电可以减轻但不能消除WMN中的干扰（Li等人， 2008年）。现有的一些关于WMN容量改进的研究仅仅集中在使用定向天线、多输入/输出和/或多无线电多信道上。其他作品解决干扰问题，考虑在同一时间，路由和通道分配，因为他们是依赖。实际上，单独地管理路由和信道分配在信道分配阶段期间不考虑业务信息。同样地，路由协议对信道状态的访问有限（Pathak和Dutta，2011; Malik等人，2015年）。然而，同时应用路由选择和信道分配是NP完全的，遵循这一趋势的方法简化了它们的目标，并试图连续地应用它们，即一个接一个地应用（Capone等人， 2010年）。基于同样的想法，我们已经提出了一种基于AODV的路由协议（Boucebsi和Belala，2015 b; Boucebsi和Belala，2017），命名为MPR-CAP 4 WMN（WMN的多路径路由和信道分配协议），处理WMN功能。它保持该网络的连通性，并在部分重叠信道（POC）的上 下 文 中 最 小 化 它 们 的 干 扰 （ Mishra 等 人 ，2005 ） 的IEEE802.11a标准。在本文中，我们继续正式分析该协议，以补充基于模拟的方法。我们提出了一个基于BRS共享的模型来支持对协议行为的有效分析此外，MPR-CAP 4 WMN规范，然后原型和Maude系统下执行。Maude重写引擎对实现BRS的反应规则是非常有用的BRS（Biographical Reactive Systems，BRS）（Milner，2008）为并发和移动系统模型提供了一个自然的语义框架。BRS在各种应用领域中的广泛使用促使该理论的创始人以几种方式对其进行扩展，例如：绑定双图（Damgaard和Birkedal，2006），定向双图（Grohmann和Miculan，2007），随机BRS（SBRS）（Krivine等人，2008）和分享的Bigraphs（Sevegnani，2012）。后者是Milners双图的一个新的推广，其中两个或多个父节点可以共享同一个子节点。因此，局部性概念被更新。因此，位置图定义被改变，父映射由二元关系而不是函数表示。这种双图扩展足以允许WMN拓扑的建模。这个拓扑中的每个元素（节点）可能有零个或多个父节点（可能包含它）。本文的其余部分组织如下：在第2节中，讨论了与我们的方法相关的一些工作然后，我们给出一个第三章是对生物反应理论的简要概述。在第4节中，我们定义了基于BRS的模型Bis-WMN，用于指定WMN的结构和行为方面。第5节展示了如何利用我们的模型来执行和形式化分析所提出的路由协议MPR-CAP4 WMN。最后，一些结论性意见和正在进行的工作总结了文件。2. 相关工作在本节中，我们涉及两类工作，那些处理信道分配（CA）和路由协议，以提高WMN的能力，和其他采用形式化的方法来分析路由协议在WMN（第2.2节）。2.1. CA和路由方法在文献中，各种方法试图提高WMN的能力集中在一些关键问题，如干扰和连接。通过提出图2所示的分类，我们强调了这些解决方案的优点和局限性。我们确定了三个主要的方法类。第一类是致力于CA过程，同时提高WMN的能力。这些基于CA的方法旨在减轻干扰，保持连通性，然后最大化网络容量。在这方面，我们指出：(1) 干扰感知方法（Subbaiah和Naidu etVenkata，2015）通过计算共享每个信道的节点数量(2) 药物感知方法（Martignon等人，2015）选择具有较少业务负载的信道。(3) 连 通 性 感 知 方 法 （ Chaudhry 等 人 ， 2012; Devare 和Wankhade，2014），其考虑了信道连接性问题。在第二类方法中，我们只建立基于路由的解决方案。在相应的路由协议中定义了各种度量来选择最佳路径，考虑了许多因素，如网络拓扑结构，链路质量和干扰。这种类型的度量被称为通道未知路由度量（包括跳数、ETX、ETT、InvETx、MTM）。尽管这些方法多种多样，但提出的解决方案仍然有限。显然，基于以前的工作限制，出现了第三类方法结合CA过程和路由算法。属于此类的协议构建于R. Boucebsi，F.Belala/沙特国王大学学报1073图二. CA和路由方法。在 路 径 选 择 期 间 考 虑 信 道 状 态 的 信 道 感 知 路 由 度 量 （ iAWARE（Subramanian等人， 2006）、SBR（Boushaba等人，2016））。在这种情况下，路由过程可以是联合单播路由和信道分配JURCA（ Gammar 等 人 ， 2016 ） ， 或 联 合 多 播 路 由 和 信 道分 配 JMRCA（Chakraborty，2015）。这种类型的方法也不能方便地支持干扰因子。2.2. 正式办法本节涉及一些工作，在文献中，试图将正式模型应用于WMN路由规范和分析。Fehnker等人（2012）提出了一种基于进程代数的模型，称为AWN，用于指定WMN路由协议，并为AODV内核建立了 形 式 化 模 型 。 这 个 结 果 （ AWN ） 也 被 van Glabbeek 等 人（2013）用来证明用于确定最新路径的序列号不能保证协议中不存在循环。其他作品研究了AODV路由协议在WMN的模型检测分析，因此在Fehnker等人。（2012）提出了一个同样基于AWN的AODV模型，并使用UPPAAL模型检验器进行了检验。另一方面，Hoefner和Kamali（2013）的作者使用统计模型检查SMC-UPPAAL描述了AODV 定 量 分 析 及 其 基 于 同 样 的 思 想 ， Hoefner 和 Edenhofer（2012）的作者提出了一种基于AWN的形式化模型来分析反应式AODVv2协议（DYMO）。在Ad-Hoc网络的上下文中，Billington和Yuan（2009），Espensen等人（5062）报告了一些结果，以使用着色Petri网对各种版本的AODVv 2进行Huang和Zhou（2012）也使用这种形式来验证WMN（黑洞攻击）中的安全性。我们将提到，所有这些方法既不解决信道分配，也不解决WMN多无线电上下文中的多路径路由。我们相信多径和多信道的联合使用可以显著提高WMN的吞吐量和性能，我们已经在Boucebsi和Belala（2017）中提出了AODV协议MPR-CAP4WMN的适当扩展，提供了这些功能。在本文中，我们提供了一个明智的组合的双图反应系统，能够代表在WMN网络的局部性和连通性，和Maude语言，一个很好的候选人执行，模拟和模型检查的底层 协 议 。我 们 注 意 到 ， 在Sevegnani （ 2012 ） ， Muffy 和 Michele（2014），Muffy等人（2014）中，作者专注于实际使用双图，并分享对真实世界场景的有效建模和分析因 此 ， 他 们 分 别 使 用 PSBRS （ Priority Stochastic BRS withSharing）和BRS with Sharing对IEEE 802.11 CSMA/CA RTS/CTS协议和家庭无线网络进行通过这项工作，他们能够证明具有共享的BRS允许重叠位置（即拓扑）的类似地，我们使用BRS与共享来指定，这一次，WMN拓扑和路由协议。3. 双图反应系统BRS理论最初由Milner（2008）引入，用于对分布式移动代码进行建模。BRS由一个配备了一组反应规则的偶图组成，这些规则允许定义给定系统如何随时间演变。双图（见图） 3）使用两个单独的图结构（位置图和链接图）来表示处理系统的连接性和局部性方面的图形模型。位置图指定了通过特定节点层次结构分布的系统实体而链接图捕获节点之间的连接它由一个超图组成，超图使用边（超边）抽象可能的实体每条边（见图3）至少连接两个节点。Places图由一个树的森林组成，称为根，描述系统如图1所示的节点（系统逻辑/物理部件）。 3可以嵌套或/和嵌套在其他图三. 二图解剖学。1074R. Boucebsi，F.Belala/沙特国王大学学报！. Σ1/4fgSDd1/4fgDBD拓扑SR结每个节点的特征在于一个控制;一个类型标识符与一个arity相结合，以定义相关端口的数量。 一个双图可以有一个或多个表示保持其他双图（或区域）的能力的位置。一个偶图通过接口中的内部和/或外部名称与其他偶图（外部环境）进行交互。双图也可以通过文本术语语言来描述，由于几个可用的操作，可以构思更复杂的双图。另一方面，为了避免不可接受的双图构造，可以将排序规则添加到双图定义中;施加一些形成规则（约束或属性）。在BRS中，反应规则R具有如下形式：B0表示在某个偶图上下文中偶图B到B0的重新配置。4. 一种基于BRS的WMN最近出现了一种对米尔纳的双图的新扩展这导致了新的定义的地方图。它基于非循环二元关系，而不是原始定义中的非循环函数。因此，不再需要额外的链接、节点副本或特殊控件来覆盖系统节点的特定特征和交叉点。在本节中，我们将解释如何采用具有共享和排序规则的双图来正式建模WMN的结构和行为方面。因此，在高抽象级别上，WMN被认为是在根内分组的一组节点和链路。WMN演进由反应规则定义。我们强调，每个WMN元素在BRS理论中具有特定的语义。因此，所设想的双图不仅指定WMN的图形表示，而且还指定其预期的数学模型。定义1.用于WMN的基于BRS的模型是一对：Bis-WMN =（B-WMN，R-WMN），其中，B-WMN是表示系统（WMN）基础结构或拓扑的偶图。● R-WMN是一组指定系统行为的反应规则(inMPR-CAP4 WMN协议的条款（Boucebsi和表1WMN元素语义的双图。根节点控制排序Arity干扰通道频带渠道B{0}信道CPC{1}下一页时隙时间插槽B不{1}下一页槽S拓扑无线电网络ISnIRn网络一W{1，2，3，4，5}{1}下一页跳跳H{2，3}个字符流动流动O{0}届会议届会议D{1}、{2}路径路径FM{1}下一页干扰路径S干扰A我{0}干扰E连接信号信号xyzS{1}、{2}范围RTG{1}下一页RI很好控制Cp的节点（排序为C/CP）表示信道频率;p是表示信道位置的参数在的渠道乐队最后，的排序B信道与信道频带相关联 所有c-sort节点最初都分组在Channel节点内。在系统演化过程中，信道可以在时隙节点内迁移以表示其使用时间。c-sort节点有一个端口（Arity = 1），它们可以通过f-name连接到Topology根中的一个（一个或多个与- wise类似，Slot-time节点有一个端口，使其能够通过电子名称链接到Network-node。我们注意到c-排序节点是原子的（不能托管其他节点），而t-排序和b-排序节点是活动的（受到反应的影响）。对干扰根的构造的这些约束由表2中所示的U干扰1/4fU1;U7;U9;U10;U13;U16;U17g表示。(2)第二个根拓扑用于定义一组路由器上使用的排序集为H;In;In正在键入节点Belala，2017））。在下面的小节中，我们详细介绍了我们提出的模型的每个部分。路由器参数n用于指定邻居的数量。确切地说，In是一个发送方接口，表24.1. B-WMN：一种WMN基础设施根据我们的形式化方法，我们定义拓扑的WMN作为一个二图B-WMN有三个独立的根，分别命名为，干扰，拓扑和连接。连通性根表示路由器的位置，允许定义路由器的连接和邻居。干扰定义了在使用的信道之间可能产生的干扰。拓扑根指定观察网络中的路由演变。所以，每个根都包含一组不同的节点。表1示出了用于在具有共享语法的双图中抽象WMN的最重要元素的对应规则集我们使用这个抽象相关联的一个正式的语义的WMN拓扑结构组成的几个固定的路由器和移动通道。(1) 定义了干扰根来模拟CA进程。它可以通过三种类型的H干扰来表示，分别为信道频带节点、信道节点和时隙节点。分别在t时隙B、S时隙中控制快播时隙和发送时隙，编队规则。U1所有acgm-节点都是原子节点U2一个w节点的所有子节点都有sortahiU3一个h节点的所有子节点都有sort aU4一个d节点的所有子节点都有sortdmU5一个i节点的所有子节点都有sort hU6 s节点的所有子节点都有排序gU7一个tb节点的所有子节点都有c在a节点中，一个端口总是通过r链路链接到a节点，另一个端口可以通过其他链路链接到一个或多个a节点U9在w-node中，端口始终链接到t-nodeU10在h节点中，一个端口总是链接到m节点，另一个端口总是链接到c节点U11在d-node中，一个端口通过一个r-name链接到两个a-node，第二个端口可以通过另一个r-nameU12在m-node中，端口链接到f-namesU13在c-node中，端口链接到a-name或b-nameU14在s-node中，一个端口总是通过r-name链接到两个a-node，第二个端口可以通过u-name链接到两个g-nodeU15在g节点中，端口总是链接到s节点U16在t节点中，端口总是链接到e名称U17所有nhisdt节点都是活动的U18一个d节点有两个r节点名●R. Boucebsi，F.Belala/沙特国王大学学报1075RFG.Σ1/4fgUUUU-ðÞ---Gn是一个接收器。路径F;路径Sg的排序用于区分设想的路径，第一路径和第二路径。排序w;h;o和d标识节点：分别在两个路由器之间打开的网络、跳、流和传输会话。中列出了用于区分流内干扰和流间干扰的i½ f干扰A;干扰Eg.结构上的拓扑根是表示通过U拓扑：表2的U1;U2;U3;U4;U5;U8;U9;U10;U11;U12;U18。（3）连通性根通过提供路由器的位置信息来支持前两种根在根定义 中 使 用 的 排 序 集 合 由 与 路 由 器 信 号 节 点 相 关 联 的sl/4Signalxyz和用于传输范围节点的t RT;RIx、y和z参数分别指定每个无线电具有在由两个给定级别限定的传输范围内减小的传输功率;路由器高功率传输范围和低功率干扰范围类型感谢T排序元素。因此，信号节点和范围节点被认为是提高路由器的灵敏度。对连通性根（偶图）的约束由U 连通性14 fU1;U6;U14;U15g定义，也由表2给出。我们注意到使用的排序纪律提供了一个分类的控制施加一组属性，必须满足在B-WMN建设。此排序规则定义为：RB WMN; jB WMN; UB 其中：● VB-WMN 1/4V干扰V拓扑其中：VInterference¼ f频段;通道;时隙g无线电;网络;跳;流;会话;路径;干扰gVConnectivity¼ fSignal;Rangeg● EB-WMN 1/4E干扰E拓扑E连通性是具有以下类型的链路的有限集合：● B-WMN：V B-WMN！ k是将种类（控制）与所有B-WMN节点相关联的映射，其中，K B-WMNk;b; c; t; a; w; h; o; d; m; i; s; gg。● PGB-WMN 1/4PG干扰kPG拓扑kPG连通性，是位置图。● LGB-WMN 1/4LG干扰kLG拓扑kLG连通性，是链接图。B-WMN节点表示由VB-WMN 并且由于集合EB-WMN而具有在它们之间交互的能力。在这种情况下，链接可以是以下类型：（1）e：将网络节点与插槽节点类型链接。(2)是表示路由器i的超弧。(3)v：是不同路由器的两个接口无线电I R = I S之间的虚拟链路。(4)Q：定义一个在 邻 居 之 间 发 送 随 机 消 息 （ 5 ） p ： 定 义 在 邻 居 之 间 发 送 的RREP(6)1：是在无线电设备之间建立的链路，其可以在路径内设想（内部）跳。（7）a：是跳节点和第一路径之间（8）b：是跳节点和第二路径之间的弧（9）f：将信道c节点与Hop节点链接(10)是将信号节点与RT=RI节点（传输和干扰范围）链接的超弧。我们注意到，边e和r最初是在拓扑根中创建的，而其他边是在拓扑根的演化过程中创建的。图图4呈现了具有其三个根的WMN的说明性示例：干扰k拓扑k连接。在Topology根中，我们考虑表示为R链路的三个路由器R1、R2、R3每一个(1)HB-WMN是一个非空的排序集合（参见表1）。(2)jB-WMN，是指定所有B-WMN控制的签名，如表1 .一、（三）UB-WMN1/4fU1;U2;U3;U4;U5;U6;U7;U8;U9;U10;U11;U12;U13;U14;U15;U16;U17;U18是保证构造具有有意义结构的双图的形成规则集。表2总结了所有这些规则。WMN基础结构的正式定义如下。定义2. WMN基础设施由B-WMN双图定义，B-WMN双图是三个给定根的并置，B-WMN =干扰k拓扑k连接，其中：B-WMN ;B-WMN;B-WMN;B-WMN;PG B-WMN; LG B-WMN：3;/！n;/n，其中：有两个接口（IS用于发送，IR用于接收）。如果路由器r是源节点或目的地节点，则r链路附接到会话节点，如对于r1和r3的情况。网络节点保存所有路由器的无线电。此外，还对干扰现象进行了监测通过干扰A和干扰E节点，其中前者表示在一条路径上产生的内部干扰，而后者是在两个流之间发生的内部干扰。两条路径可以在路由过程期间在会话节点内创建关于干扰根;识别两种类型的节点以定义时间（用于广播阶段的时隙B和用于发送的时隙S当在相同的时隙下并且在相同的地理位置中分配会聚信道（c节点）时，可能发生干扰。见图4。 B-WMN拓扑示例。1076R. Boucebsi，F.Belala/沙特国王大学学报区最初，信道被分组在信道节点（信道频带）内。连通性根提供有关分布在给定地理区域的路由器及其信号的重要信息。因此，我们找到Signal节点及其内部的RT/RI节点，它们分别是特定路由器的传输和干扰范围。根上的站点表示可能添加的节点的抽象，遵守形成规则Ui，i =1，.，18.4.2. MPR-CAP 4 WMN协议除了能够对WMN的基础设施进行建模之外，BRS还允许WMN状态演化的正式规范，这要归功于它们的反应规则。我们在这一步的主要贡献，是提出了一套参数化的反应规则R-WMN，定义了WMN的路由协议，处理流内和流间的干扰。我们定义了四类反应规则（见表3）;每一类处理我们提出的MPR-CA 4 WMN算法的一个步骤（Boucebsi和Belala，2017）。我们注意到，每个规则都有不同的参数，例如，n：表示给定节点的邻居数量。x和y指定路由器在网络中的位置。z：是信号节点内的子节点的数量。P表示信道序列顺序（在信道频带中）。4.2.1. A类：反应规则此类别的反应规则（参见表3）适用于连接位于相同传输区域（RT）或干扰区域（RI）的路由器。例如，如果两个路由器r1和r2位于相同的传输区域中，则图5所示的规则R1每个路由器可以链接三种类型的节点：发送无线电（Is）、接收无线电（Ir）和信号。在规则左侧（redex），两个路由器都没有连接，信号节点是完全独立的，并且两个路由器的接口（无线电）之间缺少链路。偶图reactum表示路由器r1和r2如何通过在路由器接口之间创建v链路来连接，在信号之间共享RT在此步骤结束时，将构建路由表，即每个路由器将能够识别其传输或干扰区域中的邻居。这个阶段是非常重要的，不仅为contacting路由器，而且为估计的干扰generated根据邻居数的每个路由器。4.2.2. B类：多路径路由的反应规则在这一类的12个反应规则中，我们只提出了三个规则，如表3所示。它们影响拓扑根，根据其功能，可以分为：表3反应规则建模MPR-CAP4 WMN行为。R. Boucebsi，F.Belala/沙特国王大学学报1077(1) 广播规则（R3;R4;R5）。当源向路由器发送路由请求时，路由过程开始。这些后者中的每一个都将该请求转发给其邻居。(2) RREP到达目的地触发第一路径的构造，这是通过沿着所选择的路径（属于该路径的节点是低干扰的）从目的地向源发送RREP响应规则R6、R7、R8、R9、R10和R11负责这项任务。(3) 规则R12;R13;R14;R15允许第二路径，同时考虑干扰，即通过从第一路径节点中选择较少数量的相邻路由器和最远的一个来保持对流间干扰的关注。例如，表3中的规则R3负责广播消息Rbn.该网络包含两个路由器r1和r2，其中r1是源（到会话节点的链路），r2是它的邻居。bor（r1的Is和r 2的Ir使用链接v 1绑定）。站点d0;d1;d2;d3抽象其他节点的存在发送消息Rbn在reactum偶图中表示，同时用q1替换链路v 1。4.2.3. C类：信道分配反应规则第三个反应规则类别（见表3）定义CA行为。R16为目的节点（路由器）分配一个信道，标志着这一阶段的开始.然后，R17继续此操作，直到到达源节点（路由器），并在R18op-ates。最后，R19保证了第二条路径的节点的信道分配。我们注意到，所有这些变化都是在干扰根内进行的。图6描述了当创建最后一个跳跃节点时CA过程的触发。r1的接收接口（Ir）在跳节点内，以及两个路由器r2和r3（属于不同路径）的发送接口（Is）在跳节点内。因此，目的地分别通过r2和r3从两个路径（路径1和路径2）接收流。干扰根包含准备分配的所有通道（通道节点内）。双图reactum定义了通道C在Ir（目的地的）和Is（r2和r3的）通过创建链接f。C节点由时隙S节点托管以指示其占用。4.2.4. D类：干涉分析的反应规则最后一类反应规则涉及干涉现象的验证，它包含9条规则.为了简化，我们只给出图五. 连接反应规则（R1）。见图6。 CA触发（R16）。1078R. Boucebsi，F.Belala/沙特国王大学学报见图7。 流内干扰检测（R20）。表3中示出的两个规则负责解决流内干扰和流间干扰。图图7示出了规则R20，其通知在相同路径的两个跳（跳1和跳2）之间发生流内干扰，因为它们使用两个干扰信道（干扰根内的时隙s中的c节点）。干扰检测是由托管两个所考虑的跳的干扰A5. 执行Bis-WMN模型双向反应系统构成了一个很好的手段来模拟WMN的结构和行为方面。然而，在这方面，表4将Bis-WMN元素映射到Maude语言概念。围绕BRS的现有工具是有限的，并且专用于某些应用领域。在我们之前的工作中（Boucebsi和Belala，2015 b; Boucebsi和Belala ， 2015 a; Boucebsi 和 Belala ， 2016 ） ， 我 们 已 经 使 用BigMC （ Perrone 和 Hildebrandt ， 2012 ） 和 BigraphER（Sevegnani，2012）工具执行和分析了我们基于bigraph的模型的初步版本。虽然这些工具很有趣，但我们面临着一些限制。例如，BigMC不提供表示共享的双图的能力，而Bigra- phER不支持形式验证。因此，复杂的属性很难表达和验证。此外，每当属性发生变化时，所提出的模型都需要进行调整，从而产生不太通用的解决方案。另一方面，一种高级形式化规范语言Maude（Clavel等，2007）基于等式和重写逻辑，提供了仿真和若干验证技术，例如模型检查、定理证明、不变量搜索等。 在这项工作中，我们选择使用LTL模型检查工具（Eker et al.， 2003），实现了对MPR-CAP 4 WMN协议固有特性的分析。为此，我们根据一组映射规则（表4）将WMN的基于共享的BRS模型转换为Maude模块。因此，我们定义了两个基本模块，给出了结构和行为方面之间的明确区分：MPR-CAP4 WMN语法模块和MPR-CAP 4WMN动态模块。通过前者，我们恢复排序和运算符声明来定义双图的签名。而在第二个模块中，我们定义了一组重写规则，实现前面定义的反应规则来指定MPR-CAP 4 WMN协议的行为。图8示出了规则语法示例;见图8。 来源Rumble Broadcasting Maude重写规则。R. Boucebsi，F.Belala/沙特国王大学学报1079表5与干涉和布线相关的属性。物业介绍干涉性质如果在协议期间，则满足此属性执行时，流内干扰发生在共享相同流路径的中间路由器之间，并且不能被处理。Inter-Interference报告无法处理内部流在竞争相同或收敛信道的邻居路由器之间发生的干扰。路由属性目的地-RREQ接收转发到目的节点的接收能力Rendezvous数据包。源-RREP-接收到目的地节点的能力，通过RREP分组应答所述源节点请求。双路径构造检查构造两个路径源节点和目的节点之间的独特路径。rule负责将Rename数据包从源节点广播到其邻居节点。在本节中，我们将展示如何利用这些Maude模块来检查与干扰检测（内部或内部）和路由过程相关的一些属性（总结见表5（更多解释见表5）。这两类属性，erties必须使用LTL逻辑在第三Maude模块（MPR-CAP 4 WMN-PREDS）表示。模型检验技术是针对系统行为的模型及其初始状态。因此，模型检查过程是通过WMN模型检查模块来实现的。表5中给出的第一个和最后一个性质规定如下：1. 内部干扰属性（见图9）是一种安全属性，确保不会发生任何不良事件。因此，它检查在AC过程期间是否发生了流内干扰并且无法解决。2. 双路径结构特性（见图） 10）是一个活跃的道具，规定好的事情最终会发生。因此，它证明了在一个节点和一个目的节点之间构造了两条不同的路径两个LTL属性模型检验的结果如图所示。 十一岁6. 结论干扰是影响WMN性能的重要因素之一。在本文中，我们一直有兴趣解决这个问题，采用BRS作为一个语义框架模型WMN的结构和行为方面。特别是，我们已经定义了一个正式的模型Bis-WMN，基于见图9。 内部干扰属性。见图10。 双路径结构特性。见图11。属性模型检查结果。1080R. Boucebsi，F.Belala/沙特国王大学学报具有共享功能的BRS及其排序功能。关于结构方面，我们定义了三个独立的根，分别代表网络拓扑、路由器连通性和信道干扰。而行为方面是由一组通用的反应规则来描述WMN的重新配置。然后，我们展示了如何结合BRS和Maude语言来执行和评估多路径路由信道分配协议的WMN（MPR-CAP4 WMN）。一组固有属性已被定义和模型检查使用Maude LTL工具。在我们正在进行的工作中，我们计划完善和丰富我们提出的模型Bis-WMN，以处理路由器的负载，例如，路由环路和隐藏节点。引用Billington，J.，袁角，越-地2009.对动态移动自组网按需路由协议DYMO进行了建模和分析. 在：Jensen，K.，Billington，J.，Koutny，M.（编）， Transactions on PetriNets and Other Models of Concurrency III（ToPNoC），LNCS. 施普林格，pp. 98比126Boucebsi，Rachida，Belala，Faiza，2015 a. 走向渠道基于SBRS共享的WMN分配方案模型，第二届过程语言Meta模型国际研讨会（MeMo 2015），法国格勒诺布尔。Boucebsi ， Rachida ， Belala ， Faiza ， 2015 b. Towards BRS based model forWirelessMesh Networks，2015年国际协议工程会议（ICPE）和国际分布式系统新技术会议（NTDS）。IEEE，pp. 1比6Boucebsi ， Rachida ， Belala ， Faiza ， 2016. Towards Modeling and SimulationWirelessMesh Networks，软件工程高级方面国际会议（ICAASE'16）。君士坦丁第二大学，君士坦丁，阿尔及利亚。Boucebsi，Rachida，Belala，Faiza，2017. MPR-CAP 4 WMN：一种结合信道分配和多路径路由的WMN路由算法。技术报告。阿尔及利亚康斯坦丁第二大学LIRE实验室。Boushaba，Mustapha，Haidan，Abdelhakim，Gendreau，Michel，2016.无线网状网络中的源基路由。 IEEE系统 J. 10（1），262-270。Capone，Antonio，Carello，Giuliana，Filippini，Ilarisabello，2010. 无线网状网路中的路由与频道分配：最佳化模型与演算法。J. 特设网络 8（6），545-563。Chakraborty，Dibakar，2015. i-QCA：多信道无线网状网中服务质量组播路由智能框架。 J. 特设网络33，221-232.Chaudhry，Aizaz U.，Ahmad，Nazia，Roshdy Hm，Hafez，2012.多无线电多信道无线网状网络中使用基于功率控制的拓扑控制通过改进信道分配来提高吞吐量和公平性。EURASIPJ. 无线通信网络 2012（1），155.Clavel，M.，Duran，F.，Eker，S.，Lincoln，P.，Marti-Oliet，N.，Meseguer，J.，Talcott，C.L.，2007年关于莫德的一切。一个高性能的逻辑框架。 Lect. Notes计算科学，4350. 斯 普林格。Damgaard，Troels Christoffer，Birkedal，Lars，2006. 公理化绑定双图。Nordic J. Comput. 13（1/2），58.Devare，M.A.S.，Wankhade，MP，2014.无线网状网中使用自动接收机及bfs-ca分析之频道分配。Int. J. Adv. Eng. 纳米技术（TM）1，1-6.Eker，Steven，Meseguer，Jos，Sridharanarayanan，Ambarish，2003. Maude LTL模型检测器及其实现，软件模型检测国际SPIN研讨会。施普林格柏林海德堡Espensen，K.，Kjeldsen，M.，克里斯滕森湖，5062.移动ad-hoc网络DYMO路由协议的建模和初步验证。In：van Hee，K.M.，瓦尔克，R. （编），应用和理论的Petri网（Petri网5062号施普林格，pp. 152- 170Fehnker，Ansgar，van Glabbeek，Robert，Hoefner，Peter，McIver，Annabelle，Portmann，Marius，Tan，Wee Lum，2012.一种无线Mesh进程代数第 22 届 欧 洲 编 程 研 讨 会 （ 22nd European Symposium on Programming ）Springer，Berlin，Heidelberg，pp. 第295-315页。Fehnker，Ansgar，van Glabbeek，Robert，Hoefner，Peter，McIver，Annabelle，Portmann，Marius，Tan，Wee Lum，2012.使用UPPAAL自动分析AODV，第18届国际会议工具和算法的建设和分析系统（TACAS 2012），pp. 173-187，塔林，爱沙尼亚.Gammar，Sonia Mettali et Ghannay，Sana，2016. Jrcap：一种用于多无线电多信道IEEE 802.11 s网状网络的联合路由和信道分配协议。J. Netw.系统管理，24;1：140-160.Grohmann，Davide，Miculan，Marino，2007.有向双图。电子笔记理论Comput. Sci.