ICAASE'2014 Modeling Channel Allocation via BRS: Case of WMNs Modeling Channel Allocation via BRS: Case of WMNs Rachida Boucebsi Faiza Belala Lakhdar Derdouri LIRE Laboratory, University of LIRE Laboratory, University of LIRE Laboratory, University of Constantine II Constantine II Constantine II Constantine, Algeria. Constantine, Algeria. Constantine, Algeria. rachidaboucebsi@gmail.com, faiza.belala@univ- derdouril@yahoo.fr, constantine2.dz, Abstract – Wireless Mesh Networks (WMNs), is an emerging wireless technology which attracts more and more attention of service providers and enterprises. The main advantage of this new class of network is to offer a flexible and economical way to expand internet access. Their major concern is to improve the flow and to preserve the bandwidth, while minimizing the interference. Using multi-channel in multi-radio WMNs can enhance their throughput and performances significantly. The main purpose of this paper is to propose a formal modeling approach, based on bigraphs for maintaining channels assignment in order to minimize interference in WMNs. Bigraphical Reactive Systems are adopted as a semantic framework for their graphical aspect and rigorous basis. Particularly, they are capable of representing both locality and connectivity of routers and channels in WMNs, during their reconfiguration process. Keywords – WMNs, Channels Assignment, Formal methods, Bigraphs. nodes to spread data traffic across multiple paths, on the other hand. 1. INTRODUCTION Wireless Mesh Networks (WMNs) are a very 1.1. Context pleasant communication support due to their flexibility, deployment ease and reduced costs. One of the most important issues in multi-radio In addition, they are a means of communication WMN design is the channel assignment for a variety of applications; offering multiple problem, i.e., how to bind each radio interface to service quality requirements in terms of delay, a channel while maintaining network throughput, reliability and confidentiality. This connectivity. Two neighboring nodes cannot kind of network does not suffer from typical communicate unless their radios share the same problems, often encountered in other wireless channel. However, the reuse of the same networks; such as energy consumption for channel in a neighborhood must be limited, sensor networks and node mobility for MANET because simultaneous transmissions on the networks. However, as they are multi-hop same channel may cause collisions and leads to wireless networks, they invoke other problems, throughput degradation. Indeed, in an particularly those related to radio interference. interference range; all links using the same This affects WMNs performance and causes channel cannot transmit at the same time and flow’s degradation and overload nodes. To should not share the channel capacity. address these problems, some existing works adopt the use of multiple radio interfaces and In literature, it has been proved that the problem multiple channels on one hand. and duplicate of Channel Assignment (CA) needs to be paths between the source and the destination addressed jointly with routing problem, i.e., find a set of rates for each network link, in order to International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 133 ICAASE'2014 Modeling Channel Allocation via BRS: Case of WMNs achieve a given objective. Unfortunately, formalism has also been used by Huang et al coupling the CA problem and routing problem is [9], this time to verify the safety of WMNs, NP-complete. A naïve solution consists of solving some attack kinds: "Black hole attack". considering the two problems separately. First, a routing protocol aiming to maximize network In the same thought, our contribution is to capacity, without depending on any particular provide a more elegant formalism in order to traffic, must be considered, then, a CA algorithm specify and analyze WMNs topology and their decorating the given paths while preserving inherent behaviors. We are interested in this network connectivity is adopted [1]. paper by the CA problem in a routing protocol. Bigraphical Reactive Systems (BRS, in short) are adopted as a semantic framework for their 1.2. Related work graphical aspect and rigorous basis. Particularly, they are capable of representing both locality Many efforts have been made to improve the and connectivity of routers and channels in capacity of WMNs, especially in technical WMNs, during their reconfiguration process, so, wireless transmissions. Traditional analysis both static and dynamic aspects of WMNs may approaches for routing protocols, are based on be specified by an unique formalism. simulation and test bed experiments. Although these methods are important and valuable for protocol evaluation, they still remain limited; they 1.3. Paper organization are very expensive in terms of time consuming and not exhaustive. Therefore, no general The remainder of this paper is organized as guarantee can be given about protocol behavior follows: Section 2 presents briefly WMNs and for a wide range of unpredictable scenarios of their architecture. In Section 3, we introduce deployment. some concepts of BRS. Section 4 illustrates our Formal methods have a great potential to help in formal modeling approach of CA in WMNs. solving this problem. They may provide valuable Conclusion and directions for future work are design tools and contribute to evaluation and presented in the last Section. verification of routing protocols. Using formal methods in the WMNs context is 2. WIRELESS MESH NETWORK OVERVIEW relatively new, but they can have a great benefit Wireless Mesh networks (in short WMNs) form a and may help in this regard. two-tier architecture based on multi-hop Among research work in this trend, we may cite: technology (Figure 1). The WMN consists of Fehnker and al [2] propose process algebra, wireless access point (router) and mobile client called AWN for specifying WMNs routing nodes. Routers are organized independently to protocols and puts up a formal model for the form a mesh backbone networks (Backbone). AODV kernel. This result (AWN) was also used They maintain connectivity, perform routing and in [3] to prove that the sequence number cannot form the wireless backbone. They are equipped, guarantee the non-existence of loops in generally with several radio interfaces for protocols. networking and an interface for connecting with devices and networks. A mesh router equipped Further works have been interested by the with a bridge “Getaway” may include several model-checking analysis of AODV routing access networks, such as the internet network protocol, but in the context of WMN, thus in [4], functionality, also interconnecting them. an AODV model was implemented with UPPAAL model-checker tool, based on AWN The deployment of WMNs, can cover a wide specifications. Also, authors of [5] described the area of the network. They are used to connect AODV quantitative analysis and its variants multiple LANs wireless, it requires only using techniques of statistical model-checking: availability of routers, one in the reach of the SMC_UPPAAL other. By the same way, authors of [6] have proposed Several wireless technologies support this type an AWN-based formal model to analyze the of communication, e.g. IEEE802.11 (for Wireless AODVv2 protocol (DYMO), which is a reactive Local Area Networks, WLAN), IEEE802.15.4 (for one, dedicated to WMNs. Wireless Personal Area Networks WPAN) and IEEE802.16 (for Wireless Metropolitan Area In the context of Ad-Hoc networks, some results Networks, WMAN). In what follows, we focus on are reported in [7, 8] to model various versions of AODVv2 using Colored Petri Nets. This International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 134 ICAASE'2014 Modeling Channel Allocation via BRS: Case of WMNs the IEEE802.11a standard providing a multitude type) equipped with reaction rules. A bigraph of channels. results from two merged graphs “places graph” The major challenge of the WMNs is the and “links graph”. Places graph specifies the interference issue that directly affects the nodes hierarchy while the links graph represents communications occurring in the same area and the connections between these nodes. on the similar or converged channels. To tackle this problem, we provide, in this paper, a BRS The places graph contains a set of trees; where based modeling approach, taking the CA in in each tree, a root of nodes, sites and arcs are WMNs as a central key for minimizing the defined. By the same way, links graph contains interference. nodes and edges, where each edge connects two or more node ports. A bigraph may contain: roots, nodes, sites, edges, ports, inner and outer names (see Figure 3). Figure 1: Architecture of WMNs 3. BRS PRESENTATION Figure 3: Bigraph Components Formally a bigraph is defined as: Bigraphical Reactive systems theory (BRS) was developed by Robin Milner in 2004 [10]. They Definition 1 [11]: G= (V, E, ctrl, prnt, link): (m, have been used to model and analyze the X) → (n, Y). Where, V and E are sets of nodes distributed mobile code. BRS focus on two and links respectively. Ctrl: V → K, represents views, connectivity and locality. The bigraphical the sorting of nodes. Prnt: mV → Vn is a reactive systems are simply a bigraph (a graph parent function, associating for each node its hierarchical parent. link : XP → EY is a transformation showing the data flow from internal names X or ports P to external names Y or arcs E. A places graph take the form of GP= (V, ctrl, prnt): m→n. while link graph is GL= (V, E, ctrl, link): X→Y. m is the sites’ number (emplacement in the graph that may host other bigraphs), X is a set of inner names. n is the number of roots (elements of bigraph able to be integrated into other bigraphs) and Y is a set of outer names. Several operations may be applied to conceive more elaborated bigraphs: vertical composition (called also composition), horizontal composition Figure 2: Link graph and Place graph of a (or tensor product operation) and parallel Bigraph product. In addition, there is a transformation operation on bigraphs which ensures the system evolution by means of applying reaction rules. A International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 135 ICAASE'2014 Modeling Channel Allocation via BRS: Case of WMNs reaction rule is a pair of bigraphs, source  prntWMN is the function associating for each (Redex) and destination (Reactum) bigraphs. node its hierarchical parent, prntWMN(Ci)=H, The source bigraph models the system current prntWMN(Ȼi)=P and prntWMN(Si)=T state. By against, the destination is the bigraph  linkWMN is a link map that shows the data modeling the next state of the system partner flow from inner face XWMN or ports P to after the execution of the rule. outer face YWMN or arcs E. For instance, a bigraph of Figure 4 is presented algebraically as: 4. MODELING WMNs WITH BIGRAPHS B= ₵6(x) ǁ C1│ C2│ C3│ C4│ C5│ C6(x) │ C7 ǁ In this section we highlight how the BRS are S1(e1,e2).d0 │ S2(e2,e3).d1 able to define both static and dynamic aspects of WMSs. The routers and channels localities may be defined by Places and links graphs, and the reactions rules model the channels allocation to a given set of links forming a path between a source router and a destination one. 4.1. Topology Modeling A generic mapping from WMNs to bigraph, covering basic constructs, is given in order to formalize a network topology. In our case, it consists essentially of a plurality of fixed routers; Figure 4: Topology bigraph example each router has two interfaces which represent the means of communication to a router via The places graph (Figure 5) in this case, channels. Channels represent the mobile represents hierarchical nesting of nodes. While components in the bigraph; their assignment is links graph (Figure 6) shows relations between subject to environment changes. these ones. So, places graph is constituted by three roots P, H and T. An initial bigraph is represented in Figure 4; “T” root defines a WMN topology having routers as e-links between nodes “S”. These later correspond to hopes that may contain channels nodes “C” instead their sites. “H” root encloses channels offered for each hop. In “P” root, we may find also channels, Figure 5: Places graph candidate for replacing those in the “H” root that may have interference problem. We give the following formal definition of the involved bigraph. Definition 2 : Each a WMN is defined by a bigraph BWMN = (VWMN, EWMN, ctrlWMN, prntWMN, linkWMN): (m, XWMN) → (3, ), where: Figure 6: Links graph  VWMN= VHVC. it represents all WMNs nodes (hops and channels), Table 1 bellow, presents the correspondence between WMNs components and their meaning  EWMN = EREC, it is a set of links (routers in BRS formalism. and links between offered channels and their alternatives),  ctrlWMN:VWMNK, gives the sorting of nodes,i.e., K={Ci:(1 atomic), Ȼi:(1,atomic), Si: (2,composite)} International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 136 ICAASE'2014 Modeling Channel Allocation via BRS: Case of WMNs Table 1: Mapping WMNs concepts in BRS 4.2. Modeling the CA Process WMNs elements Semantics in terms of We have defined a suitable bigraph to model BRS the topology of a given WMN. In addition, BRS formalism is expressive enough to be adopted Roots: for representing WMN dynamics; in terms of reaction rules that give possible ways in which a  Topology  T set of channels might be reassigned to routers in order to minimize interference. Hence, we are  Channels’ set  H interested by a set of reaction rules definition  Alternative  P These rules define the reconfiguration operation channels’ set that affects both bigraph linkage and localization. Hope Si Node SiVH, such that : Let two given paths, resulting from a routing protocol application (AODVM [12] for our case), prntWMN(Si)=T The first path associated topology is defined by the initial bigraph configuration of Figure 4, it Offered channels Nodes Ci VC, such that : shows the bigraph of a path having two hopes, Ci for each hope while there is a single channel (C6) that poses prntWMN(Ci)=H the interference problem. However, in Figure 7 Offered replacing Nodes Ȼi VC, such that : the second path denoting two interference channels Ȼi for emplacement (C4, C7) is so specified. Its each hope with prntWMN(Ȼi)=P corresponding algebraic term is as follows: possible interference B= ₵4(x2) │ ₵7(X1) ǁ C1│ C2│ C3│ C4(x2)│ C5│ C6│ C7(X1) ǁ S1(e1,e2).d0 │ S2(e2,e3).d1 Interference Xi Link xiEC, such that : link(Pj) = link(Pl)=xi with Pj and Pl, the ports of Cj and Ȼl respectively. Router Ri Link eiER Ports:  Channel Ci  Pi of node Ci need to be replaced  Pj of node Ȼi Figure 7: The second path specification  Channel Ȼi can replace Ci Having these two possible initial bigraph configurations, the CA process will be applied by  Participant  Pl of node Si means of some reaction rules to maintain this router in this functionality. hope The first reaction rule (Figure 8) describes Channel Deployment of a node Ci bigraph changes when a simple assignment is assignment belonging to root H inside the case. Each site (in the hope) hosts the a node Sj of the root P appropriate channel. The simple channel assignment reaction rule is presented algebraically as: ₵6(x) ǁ C1│ C2│ C3│ C4│ C5│ C6(x)│ C7 ǁ S1(e1,e2).d0 │ S2(e2,e3).d1 ₵6(x) ǁ International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 137 ICAASE'2014 Modeling Channel Allocation via BRS: Case of WMNs C2│ C3│ C4│ C5│ C6(x)│ C7 ǁ S1(e1,e2).C1│ C6│C7 ǁ S5 (e5, e6). C5 │ S6 (e6, e7). S2(e2,e3).d1 ₵6(x) The main contribution of this approach is twofold. Firstly, we show how Bigraphical Reactive Systems (BRS) are adopted as a semantic framework for the WMNs topology specification. Then, we enhance, in a formal way, the processing capacity of the routers belonging to one path in the WMN routing, thus avoiding the problem of wasted resources (Rational allocation of channels). Figure 8: Channel assignment reaction rule This rule type may be applied recursively to directly affect channels to their appropriate router ports. If one situation indicating the presence of interference arises, as it appears in Figure 9, another type of channel assignment rule must be applied to remedy the problem. Indeed, the assignment of the channel C6 to the port of the router e6 causes interference because it is bound to a replacing channel ₵6. Figure 9: Reaction rule causing interference Algebraic notation of this rule, illustrated through our running example is: 5. CONCLUSION ₵6(x) ǁ C6(x) │ C7 ǁ S5(e5,e6). C5 │ The major concern of Wireless Mesh Network is S6(e6,e7).d1 ₵6(x) ǁ C7 ǁ S5(e5,e6). C5 │ to improve the flow and to preserve the S6(e6,e7). C6(x) bandwidth, while minimizing the interference. The application of this reaction rule type is Using multi-channel in multi-radio WMNs is a novel approach enhancing their throughput and avoided and replacing by another type of performances significantly. reaction rules allowing to replace channels causing interference by their analogues (lying in This paper have addressed the formal modeling root P) in the CA process. The bigraph changes of multi-radio WMN networks using the BRS in this case affect both links and places graphs. formalism. It has particularly shown how the A simple example of this rule application is proposed bigraphical model provides a flexible theoretical framework, where WMN topology can identified in Figure 10 and noted algebraicly as be naturally defined. A nice consequence of this follows: axiomatization is that the Channel Affectation ₵6(x) ǁ C7 ǁ S5 (e5, e6). C5 │ S6 (e6, e7). C6(x) process in this network, has been formalized thanks to some reaction rules. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 138 ICAASE'2014 Modeling Channel Allocation via BRS: Case of WMNs In perspective, we plan to formally verify some [5] Peter Hoefner and Maryam Kamali. “Quantitative relevant properties of our proposed bigraphical Analysis of AODV and its Variants on Dynamic Topologies using Statistical Model model by existing tools, such as BigMc [13]. Checking”.11th International Conference on Formal Modeling and Analysis of Timed Systems (Formats '13), pp. 15, Buenos Aires, Argentina, August. 2013 [6] Peter Hoefner and Sarah Edenhofer. “Towards a Rigorous Analysis of AODVv2 (DYMO)”. 2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012), pp. 1-6, Austin, Texas, October. 2012 [7] J. Billington and C. Yuan, “On modeling and analyzing the dynamic MANET on-demand (DYMO) routing protocol,” in Transactions on Petri Nets and Other Models of Concurrency III (ToPNoC), ser. LNCS, K. Jensen, J. Billington, and M. Koutny, Eds. Springer, pp. 98–126. 2009. [8] K. Espensen, M. Kjeldsen, and L. Kristensen, “Modeling and initial validation of the DYMO routing protocol for mobile ad-hoc networks,” in Applications and Theory of Petri Nets (Petri NETS’08), ser. LNCS, K. M. van Hee and R. Valk, Eds., vol. 5062. Springer, pp. 152–170. 2008. [9] Hejiao Huang, Qiang Zhou. Petri-net-based Figure 10: Interference solving reaction rule Modeling and Resolving of Black Hole Attack in WMN. IEEE 36th International Conference on Computer Software and Applications Workshops. 2012. 6. REFERENCES [10] Jensen, O.H. and Milner, R. 2004. Bigraphs and [1] Rachida Boucebsi, Lakhdar Derdouri and Faiza mobiles processes (revised). Technical Report Belala. " Affectation des Canaux dans Routage 580, University of Cambridge, ISSN: 1476-2986. Multi-Chemins: Cas des Réseaux Mesh ». 3rd edition of the Student Day ESI'14 (Jeesi 14), [11] R. Milner, “Bigraphs and their algebra”. Proc. of Algiers, Algeria, May 2014. the LIX Colloquium on Emerging Trends in [2] Ansgar Fehnker, Robert van Glabbeek, Peter Concurrency Theory, Electronic Notes in Hoefner, Annabelle McIver, Marius Portmann and Theoretical Computer Science Elsevier, V. 209, Wee Lum Tan. “A Process Algebra for Wireless 5-19. 2008 Mesh Networks”. 22nd European Symposium on Programming (ESOP 2012), pp. 295-315, Tallinn, [12] Ye, Z., Krishnamurthy, S.V., Tripathi, S.K.: A Estonia, March. 2012 Framework for Reliable Routing in Mobile Ad Hoc Networks. IEEE INFOCOM 2003 [3] Robert van Glabbeek, Peter Hoefner, Wee Lum Tan and Marius Portmann. “Sequence Numbers [13] Perrone, G. and Hildebrandt, T. 2012. A Model Do Not Guarantee Loop Freedom - AODV Can Checker for Bigraphs. In proceedings of the 27th Yield Routing Loops”. 16th ACM International ACM Sym. in Applied Computing ACM-SAC'12. Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems, pp. 1-10, Barcelona, Spain, November. 2013 [4] Ansgar Fehnker, Robert van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan. “Automated Analysis of AODV using UPPAAL”. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), pp. 173-187, Tallinn, Estonia, March. 2012 International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 139