=Paper=
{{Paper
|id=Vol-1294/paper15
|storemode=property
|title=Modeling Channel Allocation via BRS: Case of WMNs
|pdfUrl=https://ceur-ws.org/Vol-1294/paper15.pdf
|volume=Vol-1294
|dblpUrl=https://dblp.org/rec/conf/icaase/BoucebsiBD14
}}
==Modeling Channel Allocation via BRS: Case of WMNs==
https://ceur-ws.org/Vol-1294/paper15.pdf
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: mV → Vn is a
reactive systems are simply a bigraph (a graph parent function, associating for each node its
hierarchical parent. link : XP → EY 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= VHVC. it represents all WMNs
nodes (hops and channels), Table 1 bellow, presents the correspondence
between WMNs components and their meaning
EWMN = EREC, it is a set of links (routers in BRS formalism.
and links between offered channels and
their alternatives),
ctrlWMN:VWMNK, 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 SiVH, 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 xiEC, such that :
link(Pj) = link(Pl)=xi with
Pj and Pl, the ports of Cj
and Ȼl respectively.
Router Ri Link eiER
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