- 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.
Wireless Mesh Networks (WMNs) are a very pleasant communication support due to their flexibility, deployment ease and reduced costs. In addition, they are a means of communication for a variety of applications; offering multiple service quality requirements in terms of delay, throughput, reliability and confidentiality. This kind of network does not suffer from typical problems, often encountered in other wireless networks; such as energy consumption for sensor networks and node mobility for MANET networks. However, as they are multi-hop wireless networks, they invoke other problems, particularly those related to radio interference. This affects WMNs performance and causes flow’s degradation and overload nodes. To address these problems, some existing works adopt the use of multiple radio interfaces and multiple channels on one hand. and duplicate paths between the source and the destination nodes to spread data traffic across multiple paths, on the other hand.
One of the most important issues in multi-radio WMN design is the channel assignment problem, i.e., how to bind each radio interface to a channel while maintaining network connectivity. Two neighboring nodes cannot communicate unless their radios share the same channel. However, the reuse of the same channel in a neighborhood must be limited, because simultaneous transmissions on the same channel may cause collisions and leads to throughput degradation. Indeed, in an interference range; all links using the same channel cannot transmit at the same time and should not share the channel capacity.
In literature, it has been proved that the problem of Channel Assignment (CA) needs to be addressed jointly with routing problem, i.e., find a set of rates for each network link, in order to achieve a given objective. Unfortunately, coupling the CA problem and routing problem is NP-complete. A naïve solution consists of considering the two problems separately. First, a routing protocol aiming to maximize network capacity, without depending on any particular traffic, must be considered, then, a CA algorithm decorating the given paths while preserving network connectivity is adopted [1].
Many efforts have been made to improve the capacity of WMNs, especially in technical wireless transmissions. Traditional analysis approaches for routing protocols, are based on simulation and test bed experiments. Although these methods are important and valuable for protocol evaluation, they still remain limited; they are very expensive in terms of time consuming and not exhaustive. Therefore, no general guarantee can be given about protocol behavior for a wide range of unpredictable scenarios of deployment.
Formal methods have a great potential to help in solving this problem. They may provide valuable design tools and contribute to evaluation and verification of routing protocols.
Using formal methods in the WMNs context is relatively new, but they can have a great benefit and may help in this regard.
Among research work in this trend, we may cite:
Fehnker and al [
Further works have been interested by the
model-checking analysis of AODV routing
protocol, but in the context of WMN, thus in [
In the context of Ad-Hoc networks, some results
are reported in [
The remainder of this paper is organized as follows: Section 2 presents briefly WMNs and their architecture. In Section 3, we introduce some concepts of BRS. Section 4 illustrates our formal modeling approach of CA in WMNs. Conclusion and directions for future work are presented in the last Section.
Wireless Mesh networks (in short WMNs) form a two-tier architecture based on multi-hop technology (Figure 1). The WMN consists of wireless access point (router) and mobile client nodes. Routers are organized independently to form a mesh backbone networks (Backbone). They maintain connectivity, perform routing and form the wireless backbone. They are equipped, generally with several radio interfaces for networking and an interface for connecting with devices and networks. A mesh router equipped with a bridge “Getaway” may include several access networks, such as the internet network functionality, also interconnecting them. The deployment of WMNs, can cover a wide area of the network. They are used to connect multiple LANs wireless, it requires only availability of routers, one in the reach of the other.
Several wireless technologies support this type of communication, e.g. IEEE802.11 (for Wireless Local Area Networks, WLAN), IEEE802.15.4 (for Wireless Personal Area Networks WPAN) and IEEE802.16 (for Wireless Metropolitan Area Networks, WMAN). In what follows, we focus on the IEEE802.11a standard providing a multitude of channels.
The major challenge of the WMNs is the interference issue that directly affects the communications occurring in the same area and on the similar or converged channels. To tackle this problem, we provide, in this paper, a BRS based modeling approach, taking the CA in WMNs as a central key for minimizing the interference. type) equipped with reaction rules. A bigraph results from two merged graphs “places graph” and “links graph”. Places graph specifies the nodes hierarchy while the links graph represents the connections between these nodes.
The places graph contains a set of trees; where in each tree, a root of nodes, sites and arcs are defined. By the same way, links graph contains 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).
Bigraphical Reactive systems theory (BRS) was
developed by Robin Milner in 2004 [
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 (or tensor product operation) and parallel product. In addition, there is a transformation operation on bigraphs which ensures the system evolution by means of applying reaction rules. A reaction rule is a pair of bigraphs, source (Redex) and destination (Reactum) bigraphs. The source bigraph models the system current state. By against, the destination is the bigraph modeling the next state of the system partner after the execution of the rule.
In this section we highlight how the BRS are 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.
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; each router has two interfaces which represent the means of communication to a router via channels. Channels represent the mobile components in the bigraph; their assignment is subject to environment changes.
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, 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:
VWMN= VHVC. it represents all WMNs nodes (hops and channels), EWMN = EREC, it is a set of links (routers 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)} prntWMN is the function associating for each node its hierarchical parent, prntWMN(Ci)=H, prntWMN(Ȼi)=P and prntWMN(Si)=T linkWMN is a link map that shows the data flow from inner face XWMN or ports P to outer face YWMN or arcs E.
For instance, a bigraph of Figure 4 is presented algebraically as: B= ₵6(x) ǁ C1│ C2│ C3│ C4│ C5│ C6(x) │ C7 ǁ S1(e1,e2).d0 │ S2(e2,e3).d1 The places graph (Figure 5) in this case, represents hierarchical nesting of nodes. While links graph (Figure 6) shows relations between these ones. We have defined a suitable bigraph to model the topology of a given WMN. In addition, BRS formalism is expressive enough to be adopted for representing WMN dynamics; in terms of reaction rules that give possible ways in which a set of channels might be reassigned to routers in order to minimize interference. Hence, we are interested by a set of reaction rules definition These rules define the reconfiguration operation that affects both bigraph linkage and localization.
Let two given paths, resulting from a routing
protocol application (AODVM [
The first reaction rule (Figure 8) describes bigraph changes when a simple assignment is the case. Each site (in the hope) hosts the 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) ǁ C2│ C3│ C4│ C5│ C6(x)│ C7 ǁ S1(e1,e2).C1│ S2(e2,e3).d1 ₵6(x)
C6│C7 ǁ S5 (e5, e6). C5 │ S6 (e6, e7). 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. Algebraic notation of this rule, illustrated through our running example is: ₵6(x) ǁ C6(x) │ S6(e6,e7).d1 S6(e6,e7). C6(x)
C7 ǁ S5(e5,e6). C5 │ ₵6(x) ǁ C7 ǁ S5(e5,e6). C5 │ The application of this reaction rule type is avoided and replacing by another type of reaction rules allowing to replace channels causing interference by their analogues (lying in root P) in the CA process. The bigraph changes in this case affect both links and places graphs. A simple example of this rule application is identified in Figure 10 and noted algebraicly as follows: ₵6(x) ǁ C7 ǁ S5 (e5, e6). C5 │ S6 (e6, e7). C6(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). The major concern of Wireless Mesh Network is to improve the flow and to preserve the bandwidth, while minimizing the interference. Using multi-channel in multi-radio WMNs is a novel approach enhancing their throughput and performances significantly.
This paper have addressed the formal modeling
of multi-radio WMN networks using the BRS
formalism. It has particularly shown how the
proposed bigraphical model provides a flexible
theoretical framework, where WMN topology can
be naturally defined. A nice consequence of this
axiomatization is that the Channel Affectation
process in this network, has been formalized
thanks to some reaction rules.
In perspective, we plan to formally verify some
relevant properties of our proposed bigraphical
model by existing tools, such as BigMc [