Abdoulaye Tall
email: abdoulaye.tall@orange.com

Zwi Altman
email: zwi.altman@orange.com

Eitan Altman
email: eitan.altman@sophia.inria.fr

Self-optimizing load balancing with backhaul-constrained radio access networks

Keywords: SON, Self-Organizing Networks, Load Balancing, Backhaul, backhaul-constrained load balancing, LTE

Self-Organizing Network (SON) technology aims at autonomously deploying, optimizing and repairing the Radio Access Networks (RAN). SON algorithms typically use Key Performance Indicators (KPIs) from the RAN. It is shown that in certain cases, it is essential to take into account the impact of the backhaul state in the design of the SON algorithm. We revisit the Base Station (BS) load definition taking into account the backhaul state. We provide an analytical formula for the load along with a simple estimator for both elastic and guaranteed bit-rate (GBR) traffic.

We incorporate the proposed load estimator in a self-optimized Load Balancing (LB) algorithm. Simulation results for a backhaul constrained heterogeneous network illustrate how the correct load definition can guarantee a proper operation of the SON algorithm.

I. INTRODUCTION

The SON concept has been introduced by 3GPP [START_REF] Gpp | Evolved Universal Terrestrial Radio Access Network (E-UTRAN); Self-configuring and self-optimizing network (SON) use cases and solutions[END_REF] as a means to manage complexity, to reduce cost of operation, and to enhance performance and profitability of mobile networks. Self organizing networks aim at autonomously configuring newly deployed network nodes (self-configuration), at tuning parameters to improve Key Performance Indicators (KPIs) (self-optimization) and at diagnosing and repairing faulty network nodes (self-healing). Research on SON has mainly focused on the RAN with the assumption of infinite backhaul capacity. However, finite backhaul capacity may impact the RAN performance in general and the operation of SON functions in particular. This paper investigates self-optimizing LB algorithm in the case of finite backhaul capacity, and proposes solutions to guarantee correct operation of the algorithm.

Different SON algorithms for LB have been proposed in the literature (e.g. [START_REF] Khan | Centralized self-optimization of pilot powers for load balancing in LTE[END_REF], [START_REF] Combes | Self-organization in wireless networks: a flow-level perspective[END_REF], [START_REF] Nasri | Handover adaptation for dynamic load balancing in 3GPP Long Term Evolution systems[END_REF], [START_REF] Rodriguez | Load balancing in a realistic urban scenario for LTE networks[END_REF]). The SON function monitors KPIs in the BSs and adjusts its parameters in order to steer those KPIs to desired values. In previous works, the KPIs are limited to the RAN, thus excluding finite backhaul capacity.

Network operators carefully dimension the backhaul to avoid capacity bottlenecks and to ensure end-to-end performance, while avoiding over dimensioning due to both equipment and deployment costs. In existing networks, and particularly for low power nodes such as small cells but not only, performance issues due to finite backhaul capacity can be encountered in Asymmetric Digital Subscriber Line (ADSL) [START_REF]Backhaul technologies for small cells[END_REF], or in wireless backhaul. In 5G networks, the high rate requirements for bandwidth intensive services [START_REF] Osseiran | Scenarios for 5G mobile and wireless communications: the vision of the METIS project[END_REF] may cause saturation even in optical backhaul, unless very costly investment in the transport network are made.

The impact of the backhaul has been considered in non-3GPP networks e.g. in LB problems in Wireless Local Area Networks (WLANs) [START_REF] Bejerano | Fairness and load balancing in wireless lans using association control[END_REF] where the authors propose load balancing algorithms but for a static scenario in which the number of users and their channel conditions are considered fixed. The backhaul limitations have been studied for LTE but only when it is used to exchange information between BSs e.g. in Coordinated Multi-Point (CoMP) [START_REF] Lee | Coordinated multipoint transmission and reception in LTE-advanced: deployment scenarios and operational challenges[END_REF]. The backhaul impact has also been studied in Radio Resource Management (RRM) mechanisms such as scheduling in [START_REF] Ghimire | Impact of limited backhaul capacity on user scheduling in heterogeneous networks[END_REF] but with a static user association mechanism. This paper analyses the impact of limited backhaul capacity on 3GPP LB SON taking into account the system dynamics. Numerical simulations show how a LB algorithm can fail when neglecting the limited backhaul. The contributions of the paper are the following:

• A global load definition for a BS taking into account the traffic demand and the capacity of both the backhaul and RAN.

• A simple and measurable estimator for the global load.

• Simulation results that show the limits of state-of-the-art load balancing algorithms in backhaul-constrained settings and the way these limits can be overcome using the global load indicator.

The rest of the paper is organized as follows. A classical definition of the load and a LB algorithm are recalled in Section II. The corrected load balancing algorithm is presented in Section III along with the modified load definition which takes into account the backhaul state. Section IV describes the numerical results which highlight the importance of using the correct load estimator to avoid significant performance deterioration. Section V concludes the paper.

II. LB FOR INFINITE-BACKHAUL

Consider the downlink of a mobile network such as the Long Term Evolution (LTE). We suppose that the backhaul has an infinite capacity or at least greater than the capacity of the BS. Two equivalent definitions can be used for the load of the BS: The first is the occupation rate of its resources. The second is the ratio between the traffic demand and the cell capacity which is valid for both elastic or GBR traffic.

In the case of a BS serving elastic traffic, users arrive randomly according to a Poisson process of intensity λ(r) (in users/s/m 2 ) at position r, download a file of random size σ with mean E(σ) (in Mbits) and leave the network when their download is complete. The load is written as [START_REF] Bonald | Wireless Downlink Data Channels: User Performance and Cell Dimensioning[END_REF]

ρ e = min 1, A λ(r)E(σ) R(r) dr , (1)
where A is the area of the considered cell, and R(r) (in Mbps) is the peak data rate (i.e. when the user is alone in the cell) at position r averaged over fading.

If the BS also serves GBR traffic with fixed amount of resources allocated to the users, the priority is given to the GBR users. We consider that GBR traffic varies slowly with respect to elastic traffic (which is bursty) and is considered constant in [START_REF] Khan | Centralized self-optimization of pilot powers for load balancing in LTE[END_REF]. The load is redefined as

ρ = min 1, ρ GBR + A λ(r)E(σ) R(r) dr , (2)
where R(r) is the peak data rate achievable at position r when using only the resources left after scheduling all GBR users, and ρ GBR is the proportion of resources occupied by the GBR traffic at the radio access (in this case

R(r) = (1 -ρ GBR )R(r)).
It is noted that this definition of the load does not depend on the scheduling algorithm which only impacts the user performance.

In practice, the load is estimated by the proportion of time-frequency resources that are occupied by the scheduler over a certain time period. We denote by K the total number of resource blocks available at a LTE BS, by K t the number of resource blocks used at time slot t, and by T the total number of time slots over which the load is estimated. The load estimator is then given as

ρ = T t=1 K t K • T . (3)
LB consists in updating certain RRM or system parameters in order to balance the load across BSs in the network.

We consider here a LB algorithm proposed in [START_REF] Combes | Self-organization in wireless networks: a flow-level perspective[END_REF] that tunes the pilot powers of BSs in order to adjust the coverage of cells according to their loads. This algorithm has been developed for distributed and reactive operation, although it can be adapted for a centralized SON operation. The algorithm is presented in the form of a Stochastic Approximation (SA) update equation as follows:

P s [t + 1] = P s [t] + (ρ 0 [t] -ρ s [t]). (4)
P s is the pilot power of BS s, ρ s [t] -its load at time t, ρ 0 [t] -the load of the reference cell at time t, and -a constant step size. The reference BS can be chosen to be the most loaded cell in the considered area.

The authors in [START_REF] Combes | Self-organization in wireless networks: a flow-level perspective[END_REF] have shown that as → 0 and t → +∞, P s in (4) converges in probability to a set of pilot powers for which the loads of all the BSs are balanced on the average. Their proof relies on the elastic traffic scenario but the algorithm remains valid for GBR traffic as well. This LB algorithm has been extended in [START_REF] Tall | Self organizing strategies for enhanced ICIC (eICIC)[END_REF] to heterogeneous network scenario where each macro cell is surrounded by a number of small cells. The pilot powers are replaced with the Cell Individual Offset (CIO) of the small cells and the reference cell is chosen as the nearest macro cell. The CIO is used together with the Reference Signal Received Power (RSRP) to define the attachment rule for the User Equipment (UE)

s * = argmax s CIO s h u s P s , (5)
where s * is the chosen serving cell, CIO s -the CIO of cell s and h u s -the pathloss from BS s to UE u.

III. LB WITH LIMITED-BACKHAUL

In order to take into account the impact of backhaul capacity on LB algorithms, the BS load definition should be modified to include the backhaul occupancy. Indeed, when the backhaul is saturated while the BS capacity remains sufficient, KPIs such as outage probability or File Transfer Time (FTT) may drastically deteriorate. In this case, the buffer of the BS may be empty since the radio link traffic flows faster than the backhaul traffic feeding the buffer.

The load (1) for elastic traffic is rewritten taking into account the state of the backhaul as follows

ρ e,g = min 1, A λ(r)E(σ) min(C BH , R(r)) dr (6)
where C BH is the capacity of the backhaul reserved for the RAN traffic. The subscript g stands for global, taking into account both BS and backhaul, as opposed to local.

The rationale behind Equation ( 6) is that the limited backhaul capacity may limit the peak data rate of a UE when alone in the cell. Hence Equation ( 1) should be modified by replacing R(r) with min(C BH , R(r)). This modification is validated through simulation results in Section IV where we compare the adjusted load formula (in dashed lines in Figs. 3 and4) with the actual load observed in the simulated system (plain lines in the Figures).

The load definition in ( 6) is modified if GBR traffic is also considered as follows

ρ g = min 1, ρ GBR,g + A λ(r)E(σ) min( CBH , R(r)) dr . (7)
CBH is the remaining backhaul capacity after backhaul resources have been allocated to GBR traffic. If we denote by D GBR the total traffic demand of GBR users then CBH = max(0, C BH -D GBR ). ρ GBR,g = max( DGBR C BH , ρ GBR ) is the global load of GBR traffic.

Load estimator

In practice, a simple load estimator can be derived, based on scheduler measurements. Consider first only elastic traffic and assume that all the resources are occupied even if only one user is present. Then the load can be estimated by the proportion of time that at least one user is present in the cell:

ρ e = T t=1 1 {xe(t)>0} T (8)
where x e (t) is the number of users at time slot t.

If we consider a mixed traffic scenario with priority given to GBR traffic, we get a general load estimator ρg that reads

ρg = 1 T T t=1 1 {xe(t)>0} + 1 {xe(t)=0} max(γ(t), ρ BH (t)) (9)
where γ(t) is the proportion of resources used by the GBR traffic at time slot t in the RAN, and ρ BH (t) is the occupancy of the backhaul at time slot t.

The LB algorithm is then rewritten as follows

P s [t + 1] = P s [t] + (ρ g,0 [t] -ρg,s [t]) (10)
where ρg,s and ρg,0 are the global loads of cell s and the reference cell 0 respectively evaluated using Eq. ( 9). It is noted that the convergence proof of ( 10) is the same as in [START_REF] Combes | Self-organization in wireless networks: a flow-level perspective[END_REF].

IV. NUMERICAL RESULTS

Consider a LTE network comprising a trisector macro BS surrounded by 6 interfering macro BSs. We select one sector and place in it 4 small cells (see Fig. 1). We consider only elastic traffic and evaluate the performance for the selected macro sector and the small cells inside its coverage area.

Two layers of traffic are superposed: the first one has a uniform arrival rate of λ users/s in the entire area (grey area in Fig. 1). The second one has a uniform arrival rate of λ h users/s in the initial area covered by the small cells (with all CIOs set to 0dB), namely the small cells are deployed to serve the users in the hotspot areas. I which also summarizes the simulation parameters.

We simulate the system during 3 hours and compare side-by-side the performance obtained using Algorithms (4) and [START_REF] Ghimire | Impact of limited backhaul capacity on user scheduling in heterogeneous networks[END_REF] denoted respectively as Local SON and Global SON. We present the results for the macro sector and for two of the small cells. We plot the analytical and the estimated loads (with T = 60s) in dashed and plain lines respectively, using the different definitions (see Figs. 3 and4). We also plot the CIOs (Fig. 2) set by the algorithms over time and the corresponding FTTs (Fig. 5).

The local SON balances the BSs' scheduler loads (see Fig. 3(a)) while it is unable to balance the real loads (see Fig. 3(b)). In particular, small cell 1 increases excessively its coverage area (see red curve in Fig. 2(a)) which causes its FTT to explode (red curve in Fig. 5(a)).

On the other hand, the Global SON balances the real loads (see Fig. It is noted that the size of small cell 2 is initially small because of its proximity to the macro cell. So the increase in its CIO does not increase too much its size, thus its performance remains good even with local SON as shown in Fig. 5(a). The overall user performance in terms of mean user throughput (MUT) and cell-edge throughput (CET) (see Fig. 6) also shows the superior performance of Global SON. At the beginning of the simulation period, the MUT is driven by the macro users which are more numerous. With the activation of the LB algorithms, the macro cell is progressively offloaded by the small cells, thus the MUT improves for both the local SON and the Global SON.

When the real loads are balanced, the global SON stops increasing the small cells coverage thus ensuring that the MUT remains good. The local SON on the other hand continues to increase the small cells coverage in order to

Fig. 1 .

 1 Fig. 1. Network Layout

4

 4

  (b)) by limiting the increase in small cells' CIOs (see Fig.2(b)). As a consequence, the small cells' FTT remain low while the macro cell's FTT is decreased (see Fig.5(b)).

Fig. 2 .

 2 Fig. 2. Cell Individual Offsets

Fig. 3 .Fig. 4 .Fig. 6 .

 346 Fig. 3. Local loads using Eq. (2) (dashed lines) and Eq. (3) (plain lines)

TABLE I

 I

				.	NETWORK AND TRAFFIC PARAMETERS
					Network parameters
				Number of cells	1 macro sector, 4 small cells
				Number of interfering macros	6 × 3 sectors
				Macro Cell layout	hexagonal trisector
				Small Cell layout	omni
				Intersite distance	500 m
				Bandwidth	20MHz
					Channel characteristics
				Thermal noise	-174 dBm/Hz
				Macro Path loss (d in km)	128 + 36.4 log 10 (d) dB
				small cell Path loss (d in km)	140.7 + 36.7 log 10 (d) dB
					Traffic characteristics
				Traffic spatial distribution	uniform
				(λ, λ h )	(8,4) users/s
				Service type	FTP
				Average file size	4 Mbits
		12
	Cell Individual Offsets (dB)	2 4 6 8 10		Macro sector Small cell 1 Small cell 2
		0 0	50	100	150
				Time (min)


Mendes Oulamara
email: mendes.oulamara@ens.fr

Arnaud J Venet
email: arnaud.venet@west.cmu.edu

Dimensional Ellipsoids Extrapolation Computer

Aided Verification

Daniel Kroening

Corina S Păsăreanu

Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation

Keywords: static analysis, semidefinite programming, ellipsoids, conic extrapolation

Introduction

Ellipsoids have been widely used to overapproximate convex sets. For instance, in Control Theory they naturally arise as sublevel sets of quadratic Lyapunov functions. They are chosen to minimize some criterion, such as the volume. In 1 Abstract Interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], they have been used to compute bounds on the output of linear digital filters [START_REF] Feret | Static Analysis of Digital Filters[END_REF][START_REF] Feret | Numerical abstract domains for digital filters[END_REF]. Roux et al. [START_REF] Roux | A generic ellipsoid abstract domain for linear time invariant systems[END_REF][START_REF] Roux | Computing quadratic invariants with min-and max-policy iterations: a practical comparison[END_REF] further extended that approach by borrowing techniques from Semidefinite Programming (SDP). However, all those works try to recover an ellipsoid that is known to exist as the Lyapunov invariant of some control system from the numerical algorithm implementing that system. The analysis algorithms are tailored for the particular type of numerical code considered. Ellipsoids are interesting in and of themselves because they provide a space-efficient yet expressive representation of convex sets in higher dimensions (quadratic compared to exponential for polyhedra). In this paper, we devise an Abstract Interpretation framework [START_REF] Cousot | Abstract interpretation frameworks[END_REF] to automatically compute an overapproximation of the values of the numerical variables in a program by an ellipsoid.

We focus our attention on the case when the program variables grow linearly with respect to the enclosing loop counters. We call this approximation an 'ellipsoidal cone'. Our work also relates to the gauge domain [START_REF] Venet | The gauge domain: scalable analysis of linear inequality invariants[END_REF], which discovers simple linear relations between loop counters and the numerical variables of a program. Even though the definitions of the abstract operations are general, this model arises more naturally when the analyzed system naturally tends to exhibit quadratic invariants, for instance in the analysis of switched linear systems. Section 2 defines the basic ellipsoidal operations and their verification, and Sect. 4 extends this to the conic extrapolation. The soundness of our analysis relies on the verification of Linear Matrix Inequalities (LMI), which we describe in Sect. 3 before delving into the description of ellipsoidal cones. Finally Sect. [START_REF] Feret | Numerical abstract domains for digital filters[END_REF] presents experiments and discusses applications to switched linear systems.

Ellipsoidal Operations

Ellipsoids are the building blocks of our conic extrapolation. We define how to compute the result of basic operations (union, affine transformation. . . ). Since there is generally no minimal ellipsoid in the sense of inclusion, we choose the heuristic of minimizing the volume. Other choices, such as minimizing the so called 'condition number' or preserving the shape, are compared in [START_REF] Roux | A generic ellipsoid abstract domain for linear time invariant systems[END_REF].

We mainly rely on SDP optimization methods [START_REF] Ben-Tal | Lectures on modern convex optimization: analysis, algorithms, and engineering applications[END_REF][START_REF]Semidefinite Optimization and Convex Algebraic Geometry[END_REF][START_REF] Vandenberghe | Semidefinite Programming[END_REF] both to find a covering ellipsoid and test the soundness of our result. However, we do not rely on the correctness of the SDP solver. For each operation whose arguments and results are expressed in function of matrices (A i ) 1≤i≤r , we define a linear matrix inequality (LMI) of the form r i=0 α i A i 0, where A 0 means "A is semidefinite positive", such that proving the soundness of the result is equivalent to showing that the LMI is satisfied for some reals (α i ). We find (α i ) candidates using an SDP solver and then verify the inequality with a sound procedure described in Sect. 3.

Definition 1 (Ellipsoid). Ell(Q, c) = {x ∈ R n |(x -c) T Q(x -c) ≤ 1} is the definition of an ellipsoid where c ∈ R n and Q is a definite positive n × n matrix.
For practical use, we also define the function

F : (Q, c) → Q -Qc -c T Q c T Qc -1 .

A Test of Inclusion

Let Ell(Q, c) and Ell(Q * , c * ) be two ellipsoids, using the function F of Definition 1 we have the following duality result (proven in [START_REF] Yildirim | On the minimum volume covering ellipsoid of ellipsoids[END_REF]):

Theorem 1. max x∈Ell(Q,c) (x -c * ) T Q * (x -c * ) -1 = min λ,β∈R {β s.t. λ ≥ 0 and βE n+1 + λF (Q, c) F (Q * , c * )} Where E n+1 is an (n+1)×(n+1) matrix, with (E n+1 ) i,j = 1 if i = j = n+1, else (E n+1 ) i,j = 0. Hence Ell(Q, c) ⊂ Ell(Q * , c * ) if and only if the minimizing value β * is nonpositive.
For given Ell(Q, c), Ell(Q * , c * ) and candidates λ and β computed by the SDP solver, the right hand term provides the LMI to check.

Computation of the Union

Let (Ell(Q i , c i )) 1≤i≤p be p ellipsoids, we want to find an ellipsoid Ell(Q * , c * ) which is of nearly minimal volume containing them. To do so, we can solve the following SDP problem. It is decomposed into a first part ensuring the inclusion, proven in [START_REF] Yildirim | On the minimum volume covering ellipsoid of ellipsoids[END_REF], and a second part describing the volume minimization criterion, proven in [3, example 18d].

The unknowns of the SDP problem are X an n × n symmetric matrix, z ∈ R n a vector, ∆ a lower triangular matrix and real numbers t, (τ i ) 1≤i≤p (u i ) 1≤i≤2 l+1 -2 where n ≤ 2 l < 2n: maximize t such that Inclusion conditions, see [START_REF] Yildirim | On the minimum volume covering ellipsoid of ellipsoids[END_REF]:

∀i, 1 ≤ i ≤ p, ∃τ i ≥ 0 s.t. τ i   Q i -Q i c i 0 -c T i Q i c T i Q i c i -1 0 0 0 0     X -z 0 -z T -1 z T 0 z -X  
Volume minimization, see [3, example 18d]:

X ∆ ∆ T D(∆) 0
where D(∆) is the diagonal matrix with the diagonal of ∆.

u 1 t t u 2 0 and ∀i, 1 ≤ i ≤ 2 l -2, u 2i+1 u i u i u 2i+2 0 ∀i, 2 l -1 ≤ i < 2 l -1 + n, u i = δ i-2 l +2
where (δ 1 , . . . , δ n ) are the diagonal coefficients of ∆.

∀i,

2 l -1 + n ≤ i ≤ 2 l+1 -2, u i = 1 (1)
We then define Q * = X and c * = Q * -1 z (in floating-point numbers, then we possibly increase the ratio of Q to ensure the inclusion condition). We can check that the resulting ellipsoid really contains the others with Theorem 1.

Affine Assignments

In this section, we are interested in computing the sound counterpart of an assignment x ← Ax + b, where x is the vector of variables, A is a matrix and b a vector.

Computation.

We want to find a minimal volume ellipsoid such that the inclusion Ell(Q

* , c * ) ⊃ {Ax + b|(x -c) T Q(x -c) ≤ 1} is verified.
By a symmetry argument, we can set c * = Ac+b. By expanding the inclusion equation, we find {Ax

+ b|x ∈ Ell(Q, c)} ⊂ Ell(Q * , Ac + b) ⇐⇒ Q A T Q * A.
Hence Q * is a solution of the following SDP problem with unknowns X an n × n symmetric matrix, z ∈ R n a vector, ∆ a lower triangular matrix and real numbers t, (τ i ) 1≤i≤p (u i ) 1≤i≤2 l+1 -2 where n ≤ 2 l < 2n:

Volume minimization:

The same constraints and objective as in [START_REF] Yildirim | On the minimum volume covering ellipsoid of ellipsoids[END_REF].

Inclusion conditions:

Q A T XA and 1 Id X where Id is the n × n identity matrix and > 0

(2) We then set Q * = X and c * = Ac + b. The second inclusion condition is here to ensure the numerical convergence of the SDP solving algorithm: if A is singular, the image by A of an ellipsoid is a flat ellipsoid. With this condition, we ensure that Ell(Q * , c * ) contains a ball of radius .

To add an input defined by the convex hull of a finite set of vectors (for instance a hypercube), we can just compute the sum for every one of these vectors and compute the union [START_REF] Roux | A generic ellipsoid abstract domain for linear time invariant systems[END_REF].

Verification.

The previous procedure gives us inequalities whose correctness ensures that the ellipsoid Ell(Q * , Ac+b) contains the image of Ell(Q, c) by x → Ax+b. However, c * = Ac + b is computed in floating-point arithmetic, hence the soundness does not extend to our actual result Ell(Q * , c * ). Therefore, we have to devise a test of inclusion for an arbitrary c * . Let us compute the resulting center in two steps: we first assume that b = 0. We have from [START_REF] Yildirim | On the minimum volume covering ellipsoid of ellipsoids[END_REF]:

(∀x, x ∈ Ell(Q, c) ⇒ Ax ∈ Ell(Q * , c * )) ⇐⇒ max x∈Ell(Q,c) (x T A T Q * Ax -2x T A T Q * c * + c * T Q * c * ) ≤ 1 ⇐⇒ min λ,β∈R {β|λ ≥ 0 and λF (Q, c) + βE n+1 G} ≤ 0 where G = A T Q * A -A T Q * c * (-A T Q * c * ) T c * T Q * c * -1 (3)
We can hence verify the inclusion by finding suitable parameters and verifying the resulting LMI.

We finally have to perform the sound computation of the center translation (c + b). Again, this is computed in floating-point arithmetic and we may have to increase the ratio of Q to ensure the verification of the inclusion condition in interval arithmetics: in the test of Theorem 1, we first compute (c + b) and F (Q, c + b) in floating-point arithmetic (and possibly increase the ratio), and with the LMI we check that it "contains" F (Q, c + b) directly computed in interval arithmetic.

Variable Packing

It can be useful to analyze groups of variables independently, and merge the results. Given a set of variables {x 1 , . . . , x p , x p+1 , . . . , x p+q } and an ellipsoidal constraint over these variables (Q, c), we can find an ellipsoidal constraint linking x 1 , . . . , x p by computing the assignment defined by the matrix I p 0 0 0 .

Given two sets of variables {x 1 , . . . , x p } and {x p+1 , . . . , x p+q } linked respectively by (Q 1 , c 1 ) and (Q 2 , c 2 ), their product is tightly overapproximated by:

Ell Q1 2 0 0 Q2 2 , c 1 c 2 .

Verifying Linear Matrix Inequalities

We now describe how we check the LMI's that determine the soundness of our analysis. We use interval arithmetic: the coefficients are intervals of floatingpoint numbers. Each atomic operation (addition, multiplication. . . ) is overapproximated in the interval domain.

Cholesky Decomposition

Recall that the SDP solver gives us an inequality of the form r i=0 α i A i 0, and candidate coefficients (α i ).

We translate each matrix and coefficient into the interval domain, and sum them up in interval arithmetic so that the soundness of the result does not depend on the floating-point computation of the linear expression.

Then, we compute the Cholesky decomposition of the resulting matrix in interval arithmetic. That is, we decompose [START_REF] Johansson | mpmath: a Python library for arbitraryprecision floating-point arithmetic[END_REF] the matrix A into A = LDL T where D is an interval diagonal matrix and L a (non interval) lower triangular matrix with ones on the diagonal. Checking that D has only positive coefficients implies that A is definite positive.

Practical Aspects of the Ellipsoidal Operations

The Precision Issue.

The limitation in the precision of the computations makes us unable to actually test whether a matrix is semidefinite positive: we can only decide when a matrix is definite positive "enough". For instance, standard libraries1 fail at deciding that the null matrix 0 is semidefinite positive.

It means that for all the operations and verifications, we have to perform additional overapproximations in addition to those made by the SDP solver, such as multiplying the ratio of the ellipsoid by a number (1 + ). Moreover, in the verification of LMI's, it can prove useful to explore the neighborhood α i ± > 0 of the parameters (α i ). As Roux and Garoche write in [START_REF] Roux | Computing quadratic invariants with min-and max-policy iterations: a practical comparison[END_REF]: "Finding a good way to pad equations to get correct results, while still preserving the best accuracy, however remains some kind of black magic."

Complexity Results.

From the complexity results of Porkolab and Khachiyan, the resolution of an LMI with m terms in dimension n has a complexity of O(mn 4 ) + n O(min(m,n 2 )) [START_REF] Porkolab | On the complexity of semidefinite programs[END_REF]. Hence the complexity of the abstract operations is polynomial as a function of the dimension n (i.e., the number of variables), with a degree almost always smaller than 4 (for most operations, m ≤ 4). The complexity of the Cholesky decomposition can be directly computed and is O(n 3 ).

Conic Extrapolation

Now that the ellipsoidal operations are well defined, we can describe the construction of the conic extrapolation. The goal is to analyze variable transformations when the ellipsoidal radius evolves (sub-)linearly in the value of the loop counters.

Let us have numerical variables x = (x 1 , . . . , x n ) and loop counters y = (y 1 , . . . , y k ), we want to control the evolution of x depending on the counters y, which are expected to be monotonically increasing.

Inspired by the ellipsoidal constraints, we can use intersections of linear inequalities and a quadratic constraint of the form: Definition 2 (Conic extrapolation). Let q be a definite positive quadratic form (that is, there is a matrix Q 0 such that ∀x ∈ R n , q(x) = x T Qx), c ∈ R n , and for i ∈ 1, k , β i > 0, δ i ∈ R n , λ i ∈ R, and b i a boolean value. We define the ellipsoidal cone:

Con((q, c), (β i , δ i , λ i , b i ) 1≤i≤k ) = {(x, y) ∈ R n × R k |∀i ∈ 1, k , y i ≥ λ i ∧ ∀i ∈ 1, k , (b i ∨ (y i = λ i )) ∧ q(x -c - k i=1 (y i -λ i )δ i ) ≤ ( k i=1 β i (y i -λ i ) + 1) 2 }
Let Q be the matrix associated with q, Ell(Q, c) is the ellipsoidal base of the cone. The λ i ∈ R are the base levels of the cone, that is the minimum values of the loop counters (usually zero). The δ i ∈ R n are the directions toward which the cone is "leaning" (for instance, with a single loop iterating x ← x + 1, we would want δ to be equal to 1). The β i ∈ R determine the slope of the cone in each dimension. The b i are boolean values stating, for each dimension, whether an extrapolation has been made in this dimension. That is, do we consider only the (x, y) with y i = λ i (case b i = False) or all those with y i ≥ λ i and verifying the other conditions (case b i = True).

Conditions of Inclusion

We need to be able to test the inclusion of two cones. The following theorem shows that this inclusion can be reframed as conditions that can be verified with an SDP solver.

Theorem 2. If we consider two cones C = Con((q, c),

(β i , δ i , λ i , b i ) 1≤i≤k ) and C = Con((q , c ), (β i , δ i , λ i , b i ) 1≤i≤k ), then C ⊂ C if and only if                        (i) ∀i ∈ 1, k , λ i ≤ λ i and λ i > λ i ⇒ b i (ii) Ell(q, c) ⊂ Ell      q (1 + k i=1 β i (λ i -λ i )) 2 , c + k i=1 (λ i -λ i )δ i      (iii) ∀i ∈ 1, k , b i ⇒ b i and β i 2 ≥ max u∈R n ,q(u)≤1 q (β i u + δ i -δ i )
To prove this theorem, we first consider the case when the two cones have the same base levels. That is, we reduce it to the case when all the λ i 's are equal to 0.

Lemma 1. If we consider two cones C = Con((q, c), (β i , δ i , 0, b i ) 1≤i≤k ) and C = Con((q , c ), (β i , δ i , 0, b i ) 1≤i≤k ), then C ⊂ C if and only if      (i) Ell(q, c) ⊂ Ell(q , c ) (ii) ∀i ∈ 1, k , b i ⇒ b i and β i 2 ≥ max u∈R n ,q(u)≤1 q (β i u + δ i -δ i )
The proof of these two results is postponed to the end of the section.

Test of Inclusion

Theorem 2 enables us to build a sound test of inclusion between two cones C and C . Condition (i) can be directly tested. We can use the procedure of the previous section to test the ellipsoidal inclusion of condition (ii). Note that in practice, the test of inclusion will be used (during widening iterations) on cones with the same ellipsoidal base. In these cases, we do not want the overapproximations of the SDP solver to reject the inclusion. Therefore we should directly test whether the bases (Q, c) and the λ i 's are equal (as numerical values) and answer True for the test of base inclusion in this case.

To perform a sound test on the subcondition of (iii):

β i 2 ≥ max u∈R n ,q(u)≤1 q (β i u + δ i -δ i )
we can compute an overapproximation of M = max u∈R n ,q(u)≤1 q (β i u + δ i -δ i ) From Theorem 1, we know that

M = 1 + min s,t∈R t | s ≥ 0 and sF ( Q β 2 i , 0) + tE n+1 F (Q , δ i -δ i )
So for any feasible solution (s, t) of this SDP problem, 1 + t is a sound overapproximation of M . The abstract counterpart of a statement y i ← y i + v for some value v, is the operation λ i ← λ i + v: after the statement, the constraint is verified for y i -v, and making this change in Definition 2 leads to the new value of λ i . To have a sound result, we can compute the sum in interval arithmetic, and take the lower bound. Note that, in general, the loop counters are integer valued. In that case, the value can be computed exactly.

Affine Operations on Cones

Affine Transformations.

We want to have a sound counterpart for the affine assignment x ← Ax + b where A is a matrix and b a vector. Let us fix the values of (y i ) 1≤i≤k and note

R = (1 + k i=1 β i (y i -λ i )) and ĉ = c + k i=1 (y i -λ i )δ i . Let Q
be the matrix of q. We first want to find (Q , c ) such that we have the inclusion

{Ax + b|x ∈ Ell( Q R 2 , ĉ)} ⊂ Ell( Q R 2 , c
). By symmetry, we can set c = Aĉ + b. Thus, by doing the same calculations as in Sect.2.3, we have

{Ax + b|x ∈ Ell( Q R 2 , ĉ)} ⊂ Ell( Q R 2 , c ) ⇐⇒ Q A T Q A
The last condition does not depend on the y i 's, so for any quadratic form q whose matrix Q verifies Q A T Q A (which is an SDP equation, we can add the conditions of volume minimization of (1), and Q

1 I n with small enough, to ensure numerical convergence), we have

{(Ax, y)|(x, y) ∈ Con((q, c), (β i , δ i , λ i , b i ) 1≤i≤k )} ⊂ Con((q , Ac), (β i , Aδ i , λ i , b i ) 1≤i≤k )
As in the case of ellipsoidal assignments, Ac + b and Aδ i are computed in floating-point arithmetic. Hence once they are computed, we have to ensure that the resulting numerical cone contains the formally defined cone, i.e. we need to verify the inclusion of ellipsoidal bases with (3) and the procedure described in Sect.2.3. We also need to verify the conic inclusion, i.e. the fact that β i ≥ β i + q (Aδ i -δ i ), where β i and δ i are the parameters of the resulting cone. So we may have to update the parameters and verify the inequalities in a sound manner.

Addition and Removal of Counters

When the analyzer enters a new loop, it needs to take into account the previous constraint and add a dependency on the current loop counter y i . Moreover, when it exits a loop, it needs to build a new constraint overapproximating the previous one that does not involve the counter y i .

Ellipsoidal constraints can be seen as conic constraints with k = 0. Hence we study the problem of adding and removing counters to a conic constraint Con((q, c), (β i , δ i , λ i , b i ) 1≤i≤k ).

Adding a Counter.

Let y k+1 be the counter we want to add. Let λ k+1 be the minimal value of the counter inferred at this point. We set β k+1 = 0, δ k+1 = 0 and b k+1 = True if the value of y k+1 at this point of the analysis is not known precisely, else if we know that y k+1 = λ k+1 , then b k+1 = False.

That gives us the constraint Con((q, c),

(β i , δ i , λ i , b i ) 1≤i≤k+1 ).
Proof. It is immediate from Definition 2 and the distinction made on what we know about y i , that this constraint overapproximates the set of reachable (x, y) at this point.

Removing a Counter.

We now want to remove the counter y k from the conic constraint, provided that we know that

y k ∈ [λ k , M ] with M < +∞ (note that if it happens that b k = False, then M = λ k ). Theorem 3. Let C = Con((q, c), (β i , δ i , λ i , b i ) 1≤i≤k+1 ).
Then C is convex and we have

C |y k ∈[a,b] = C ∩ {(x, y)|y k ∈ [a, b]} = Conv(C ∩ {(x, y)|y k = a ∨ y k = b}).
where we suppose a ≥ λ k and where Conv(X) is the convex hull of X. Proof. Up to translation, we can assume that ∀i ∈ 1, k , λ i = 0. If a = b, it is immediate. We suppose a < b. Then, if Q is the matrix of q, let S be the inverse of its square root (S -2 = Q). We have

(x, y) ∈ C ⇐⇒ q(x -c - k i=1 y i δ i ) ≤ (1 + k i=1 β i y i ) 2 ⇐⇒ ∃u ∈ R p , ||u|| 2 ≤ 1, x -c - k i=1 y i δ i = (1 + k i=1 β i y i )Su ⇐⇒ ∃u ∈ R p , ||u|| 2 ≤ 1, x = y k -a b -a x b + (1 - y k -a b -a )x a where x b = (c + k-1 i=1 y i δ i + (1 + k-1 i=1 β i y i )Su + b(δ k + β k Su)) x a = (c + k-1 i=1 y i δ i + (1 + k-1 i=1 β i y i )Su + a(δ k + β k Su))
From the previous equivalences, we have z a = (x a , y 1 , . . . , y k-1 , a) ∈ C and

z b = (x b , y 1 , . . . , y k-1 , b) ∈ C. Moreover (x, y) = y k -a b-a z b + (1 -y k -a b-a )z a .
Let π y k be the projection along y k . Since convexity and barycenters are preserved up to projections,

π y k (C |y k ∈[a,b] ) = Conv(π y k (C |y k =a ) ∪ π y k (C |y k =b )). So, by a direct calculation π y k (C |y k =a ) = Con(( q (1 + β k (a -λ k )) 2 , c + (a -λ k )δ k ), ( β i 1 + (a -λ k )β k , δ i , λ i , b i ) 1≤i≤k-1 )
We have a similar equality for π y k (C |y k =b ), hence we just have to compute the join (π y k (C |y k =a ) Con π y k (C |y k =b )), which is an overapproximation of the convex hull of the union. However, we have to implement this operation such that it is sound when computed in floating-point arithmetic. Via affine transformation, we can soundly compute an ellipsoidal base Ell(q * , c * ) such that

q(x -(c + (a -λ k )δ k )) ≤ (1 + β k (a -λ k )) 2 q(x -(c + (b -λ k )δ k )) ≤ (1 + β k (b -λ k )) 2 ⇒ q * (x -c * ) ≤ 1
Then, for any i ∈ 1, k -1 such that b i = True, if we note β * i and δ * i the parameters of the resulting cone, in order to have an inclusion of C |y k =a and C |y k =b in C * , we need to establish by Theorem 2 that:

           β * 2 i ≥ max q(u) (1+β k (a-λ k )) 2 ≤1 q * ( β i 1 + (a -λ k )β k u + δ i -δ * i ) β * 2 i ≥ max q(u) (1+β k (b-λ k )) 2 ≤1 q * ( β i 1 + (b -λ k )β k u + δ i -δ * i )
And since from our hypothesis on Ell(q * , c * ) we know that q q * , we can just set δ * i = δ i and the condition becomes β * i ≥ β i . So we can just define β * i = β i , hence the resulting cone after the removing of the k th counter is Con((q * , c * ), (β i , δ i , λ i , b i ) 1≤i≤k-1 )

A Widening Operator

Let C = Con((q, c), (β i , δ i , λ i , b i ) 1≤i≤k ) and C = Con((q , c ), (β i , δ i , λ i , b i ) 1≤i≤k ). We suppose that ∀i ∈ 1, k , λ i ≤ λ i and ∃i ∈ 1, k , λ i < λ i .

We want to define a widening operator over cones. The intuitive idea is that if C "starts strictly below" C (cf. the conditions on the λ i 's), then C * = C C has the same ellipsoidal base as C, but its opening has been "widened" to contain C . The decision of only changing the opening and the orientation of the cone (i.e., to change only the β i 's and δ i 's) relies on the hypothesis that the relative shift of C from C has good chances to be reproduced again. Hence the name of "conic extrapolation".

Definition of p .

More formally, we first study the special case in which we know that Ell(q , c ) ⊂ C and we define a partial widening operator p .

Let

C * = C p C = Con((q, c), (β * i , δ * i , λ i , b * i ) 1≤i≤k
). We note (i), (ii), (iii) (resp. (i ), (ii ), (iii )) the conditions of Theorem 2 relative to the inclusion C ⊂ C * (resp. C ⊂ C * ). By construction of C * , we already have (ii) and with our hypothesis Ell(q , c ) ⊂ C , we just need to verify C ⊂ C * to have (ii ). We

can define ∀i ∈ 1, k , b * i = (b i ∨ b i ∨ λ i < λ i ),

which gives us (i) and (i ).

Finally to verify (iii) and (iii ), we only need to define the β * i 's and

δ * i 's such that ∀i ∈ 1, k ,      b i ⇒ β * i 2 ≥ max q(u)≤1 q(β i u + δ i -δ * i ) b i ⇒ β * i 2 ≥ max q (u)≤1 q(β i u + δ i -δ * i )
which we overapproximate by a triangle inequality for the norm defined by q:

∀i ∈ 1, k ,              b i ⇒ β * i ≥ β i + q(δ i -δ * i ) b i ⇒ β * i ≥ β i r + q(δ i -δ * i ) where r ≥ min{ρ > 0| q ρ 2 q}
With the SDP methods of the first section, we can compute an overapproximating r. For each i, if none of b i or b i is True, then from our hypothesis Ell(q , c ) ⊂ C , b * i = False and we do not have to give values to either

β i or δ i . If only b i (resp. b i ) is True, then we define δ * i = δ i and β * i = β i (resp. δ * i = δ i and β * i ≥ rβ i ). If b i = b i = True, we want to minimize max(β i + q(δ i -δ * i ), β i r+ q(δ i -δ * i )
). If we fix the q-distance q(δ i -δ * i ), we want to minimize the q-distance q(δ i -δ * i ). With this geometrical point of view, we see that the optimal δ * i is a barycenter of δ i and δ i . So we define δ * i = µδ i + (1 -µ)δ i where we want to find µ ∈ [0, 1] minimizing max(

β i + q(δ i -µδ i -(1 -µ)δ i ), β i r + q(δ i -µδ i -(1 -µ)δ i )) = max(β i + (1 -µ) q(δ i -δ i ), β i r + µ q(δ i -δ i )).
Hence, we can exactly (up to floating-point approximations) compute µ, define δ * i and then β * i . This construction of (β * i , δ * i , b * i ) 1≤i≤k ensures that C, C ⊂ C * and defines p .

Definition of .

We now study the general case in which the only assumption made is that ∀i

∈ 1, k , λ i ≤ λ i and ∃i ∈ 1, k , λ i < λ i .
We define a cone C + = Con((q, c),

(β + i , δ + i , λ i , b + i ) 1≤i≤k
), which contains the ellipsoidal base of the two cones. The definition (with q, c and the λ i ) ensures the inclusion of the ellipsoidal base of

C. Let R = 1 + k i=1 β + i (λ i -λ i ) and ∆ = k i=1 δ + i (λ i -λ i ). We define ∀i ∈ 1, k , b + i = (λ i < λ i ). Let r = min{ρ > 0| q ρ 2 q }, if we have Ell( q r 2 , c ) ⊂ Ell( q R 2 , c + ∆) then Ell(q , c ) ⊂ Ell( q R 2 , c + ∆) and
from the definitions of the b + i 's and Definition 2, we would have Ell(q , c ) × {(λ 1 , . . . , λ k )} ⊂ C + . To get this result, we need:

Ell( q r 2 , c ) ⊂ Ell( q R 2 , c + ∆) ⇐⇒ {q(c -c -∆) ≤ (R -r) 2 } ∧ {R ≥ r}
If the transformations applied to the cone are affine, the shift can be seen as the difference between centers. So we choose to define ∆ = c -c. Then we choose the minimal possible value of R to have a cone as tight as possible: once the δ i 's corresponding to ∆ are computed in floating-point arithmetic, we can define an upper bound on q(c -c -∆) + r and define R accordingly, so that the above inequality is verified. These definitions of ∆ and R must be implemented in terms of β + i and δ + i . Since we ensured that there is at least one i such that (λ i -λ i ) = 0, there is always a solution. If only one i fits this criterion the solution is unique, otherwise a choice must be made on how to weight the different variable.

This uncertainty can be easily explained: recall that in real programs, only one loop counter is increased at a time, so we know what causes the change in our constraint. This is not the case if many loop counters are increased at the same time.

Finally, this definition of C + allows us to define the widening operator by:

C C = C p C + p C .
Note that the assumptions of p are verified since C and C + have the same ellipsoidal base, and C + , hence C p C + , contains the base of C .

To ensure the convergence of the widening sequence in the cases described in Sect. 5, we can use a real widening operator on the β i 's that sets them to +∞ after a certain number of steps, for instance.

Proof of the Characterization of Conic Inclusion

Proof of Lemma 1.

• We first prove that (i) ∧ (ii) ⇒ C ⊂ C . From (i), we know that ∀u ∈ R p , q(u) ≤ 1 ⇒ q (u+c-c ) ≤ 1. Thus, for (x, y) ∈ R p ×R k + such that q(xc -

k i=1 y i δ i ) ≤ (1 + k i=1 β i y i ) 2 , we define ν = (1 + k i=1 β i y i ) ≥ q(x -c - k i=1 y i δ i ) and u = 1 ν (x -c - k i=1 y i δ i ).
We have q(u) ≤ 1.

q (x -c - k i=1 y i δ i ) = q u + (c -c ) + (ν -1)u + k i=1 y i (δ i -δ i ) ≤ q (u + c -c ) + k i=1 y i q (β i u + δ i -δ i ) 2 (4)
So if b i = False then y i = 0, hence y i q (β i u + δ i -δ i ) ≤ y i β i , and from (ii), if b i = True, then we have the same inequality since q(u) ≤ 1. So this inequality is true for all i ∈ 1, k .

Thus, we have q (x -c -

k i=1 y i δ i ) ≤ (1 + k i=1
β i y i ) 2 and ∀i ∈ 1, k we have

y i ≥ 0 and from (ii), y i > 0 ⇒ b i ⇒ b i . So (x, y) ∈ C . So C ⊂ C .
• Now we prove that C ⊂ C ⇒ (i) ∧ (ii). It is obvious that C ⊂ C ⇒ (i) by taking the intersections of the cones with the set {(x, 0) ∈ R p+k }.

If ∃i ∈ 1, k s.t. b i = False and b i = True, then there exist a point (x, y) of C with y i > 0, so (x, y) / ∈ C and C ⊂ C . If ∃i ∈ 1, k s.t. b i = True and β i < max q(u)≤1 q (β i u + δ i -δ i ), then let us take u ∈ R p such that q(u) ≤ 1 and β i < q (β i u + δ i -δ i ). We define x(t) = (1 + β i t)u + tδ i + c.

For any t ≥ 0, q (x(t) -c -tδ i ) ≥ q (u + c -c ) -t q (β i u + δ i -δ i ) 2
Since β i < q (β i u + δ i -δ i ), and from the previous inequality, we have for t big enough, q (x(t)

-tδ i -c ) > (1 + β i ) 2 . By a direct computation q(x(t) -tδ i -c) ≤ (1 + β i t) 2 .
And since b i = True, we have for y(t) such that y(t) i = t and y(t

) j =i = 0, (x(t), y(t)) ∈ C, (x(t), y(t)) / ∈ C so C ⊂ C . We have proven ¬(i) ∨ ¬(ii) ⇒ C ⊂ C , so we finally have (i) ∧ (ii) ⇐⇒ C ⊂ C . Proof of Theorem 2. Since (c, (λ i ) 1≤i≤k ) ∈ C, it is clear that (i) is a necessary condition. Moreover, C ⊂ {(x, y) ∈ R p+k |∀i ∈ 1, k , y i ≥ λ i } =: Orth λ , therefore C ⊂ C ⇐⇒ C ⊂ C ∩ Orth λ ⇐⇒ C ⊂ C ∩ Orth λ ∧(i).
Directly from Definition 2, we have for R

= (1 + k i=1 β i (λ i -λ i )) the impli- cation (i) ⇒ C ∩ Orth λ = Con(( q R 2 , c + k i=1 (λ i -λ i )δ i ), ( β i R , δ i , λ i , b i ) 1≤i≤k ). So
up to translation, we can reduce this case to λ i = λ i = 0 and apply Lemma 1.

C ⊂ C ⇐⇒ C ⊂ C ∩ Orth λ ∧(i) ⇐⇒ (i) ∧ Ell(q, c) ⊂ Ell( q R 2 , c + k i=1 (λ i -λ i )δ i ) ∧ ∀i ∈ 1, k , b i ⇒ b i and β i 2 R 2 ≥ max q(u)≤1 q R 2 (β i u + δ i -δ i ) ⇐⇒ (i) ∧ (ii) ∧ (iii)
5 Application and Convergence

1: x ← 0 ∈ R n 2: for y from 0 to ∞ do 3: pick i ∈ 1, n 4: pick ∈ {-1, 1} 5:
x Figure 4: Example of a program and its average analysis time on a 2 GHz CPU. Ellipsoidal cones have been prototyped3 in Python using NumPy [START_REF] Stéfan Van Der Walt | The NumPy Array: A Structure for Efficient Numerical Computation[END_REF], CVXOPT [START_REF] Andersen | CVXOPT: A Python package for convex optimization[END_REF], mpmath [START_REF] Johansson | mpmath: a Python library for arbitraryprecision floating-point arithmetic[END_REF]. The Apron [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF] C library has been used for polyhedra.

i ← x i + n 2
In the definition of the conic extrapolation, we did not describe how to choose the ellipsoidal base. For instance, it is possible to get an ellipsoidal shape by computing some iterates of the loop. This seems to work well in the case of programs composed of loops and nondeterministic counter increments: the iterations capture in which direction the counters globally increase (Fig. 4). Since the diameter of the set containing the numerical variables grows linearly, any cone will be overapproximating for β big enough.

Switched Linear Systems

However, the picture is not as nice if we add linear transformation. This is the case, for instance, for switched linear systems in control theory (Fig. 5): if the quadratic form associated with the ellipsoid is not a Lyapunov function of the linear part of the system (of the matrices A i in Fig. 5), then the growth of its radius is exponential in the loop counters, and cannot be captured by our conic extrapolation. So if Q is the matrix of the ellipsoidal base of the cone, the Lyapunov conditions should be verified simultaneously : ∀i, Q -A T i QA i 0.

1

: x ← 0 ∈ R n 2: (A i , b i ) 1≤i≤k 3:
where Experimental conditions are the same as in Fig. 4. Except for Benchmarks 1 and 2, the resulting polyhedron is trivial. This is not always possible, but one can use the SDP solver to try to find a suitable Q. Note that the identity matrix is not stable in the sense of control theory and should not be included in the search of Q. When Q verifies the Lyapunov conditions, it is easy to show that for β i large enough, the cone will be invariant during loops iterations.

b i ∈ R n , A i ∈ M n (R) 4: for y from 0 to ∞ do 5: i ← rand(1, n) 6: x ← A i x + b i Benchmark 1 2 3

Proof of Convergence with the Lyapunov Condition

Now we show the converse of the assertion of the previous paragraph: if q is a Lyapunov function for the matrix A and b is a vector, then for β large enough C = Con((q, c), (β, δ, λ, True)) is stabilized by the iteration of x ← Ax + b.

Proof. Up to translation, we show the result for λ = 0. We know than for any x ∈ C, q(x -c -yδ) ≤ (βy + 1) 2 and by the Lyapunov condition, there exist > 0 such that ∀x, q(Ax) ≤ (1 -)q(x). ≤ βy + 1 + q(M + y(A -Id)δ) -ηβy ≤ βy + 1 + q(M ) + y( q((A -Id)δ) -ηβ)

So for β large enough (β > q(M ) and β > q((A -Id)δ)/η), we have q(Ax + b -c -(y + 1)δ) ≤ (β(y + 1) + 1) 2 .

Concluding Remarks and Perspectives

We proposed an abstract interpretation framework based on ellipsoidal cones to study systems with (sub-)linear growth in loop counters. The aim of this work is twofold: to build an extension of the formal verification of linear systems, and to devise a framework that can be used outside the context of digital filters. Indeed, only the choice of the ellipsoidal base of the cone has to deal with control theory considerations. The next step is obviously to go beyond the prototype and have a robust implementation to test this framework on actual systems. This will involve a research on how to accurately tune and use the SDP solver, how to deal with precision issues.

The main tools are the SDP solver and the SDP duality to check the soundness of the results of operations via LMI's. However, we are not bound to use SDP solvers to compute these results, and exploring other options might speed up the analysis.

It would also be interesting to generalize this framework to switched linear systems that are more complex than those studied above. An example is the analysis in [START_REF] Daafouz | Stability analysis and control synthesis for switched systems: a switched Lyapunov function approach[END_REF].

Acknowledgments.

We want to thank Pierre-Loïc Garoche and Léonard Blier for the fruitful conversations we had with each of them during this work, as well as the anonymous referees for the time and efforts taken to review this work.

Figure 1 :

 1 Figure 1: Example for p = 1, k = 1.

4. 3 . 1

 31 Counter Increment.

Figure 2 :

 2 Figure 2: Removing the counter y k , hence projecting along its direction.

Figure 3 :

 3 Figure 3: Example showing the various cones involved in the definition of : C 1 in black, C 2 in blue, C + in green and C 1 C 2 in red.

Figure 5 :

 5 Figure5: The structure of a Switched Linear System and some benchmarks. Experimental conditions are the same as in Fig.4. Except for Benchmarks 1 and 2, the resulting polyhedron is trivial.

Let η = 1 - √ 1 - 1 -

 111 and M = (A -Id)c + b -δ. We haveq(Ax + b -c -(y + 1)δ) = q(A(x -c -yδ) + (A -Id)(c + yδ) + b -δ) ≤ √ (βy + 1) + q((A -Id)(c + yδ) + b -δ)

E.g mpmath[START_REF] Johansson | mpmath: a Python library for arbitraryprecision floating-point arithmetic[END_REF]

The prototype Python code and details about benchmarks are available on http://www.eleves.ens.fr/home/oulamara/ellcones.html

† This material is based upon work supported by the National Science Foundation under Grant No. 1136008.


Seifddine Bouallegue

Nozha Cherif

Kaouthar Sethom

Transparent Real time Service on Connected Train

In order to achieve the everywhere at anytime Internet, connection to the network must be available even inside cars, trains and buses, without disruption of service. In order to reach this objective, intelligent communications are now considered necessary and will play an increasing role in the modern Transportation Systems. As train speeds increase, wireless communications between devices on the train and the outside encounter difficulties, and maintaining communication quality is a major challenge. This paper, propose a new multihomed solution for transparent internet access in trains through secure handoff anticipation.

I.

INTRODUCTION

The growth in wireless communication technologies over the last two decades opens up several opportunities for supporting internet access on trains. While wireless access technologies offer higher data rates and wireless network coverage continuously increases, we are still far from seamless and ubiquitous Internet connectivity. Particularly when users move, wireless conditions change and handovers (potentially to different operators or networks) occur, that may yield significantly different communication characteristics-or connectivity may be lost altogether. Even though Internet protocols and applications are (or should be) designed to adapt to changing network conditions, their capabilities to deal with sudden changes are fairly limited-and disconnections are usually not tolerated at all. The former may and the latter usually do lead to errors and applications break. Users demand the ability to keep their ongoing communications while changing their point of attachment to the network as they move around.

Currently, NEtwork MObility (NEMO) solutions [START_REF] Devarapalli | NEMO basic support protocol[END_REF] are being developed by the Internet Engineering Task Force (IETF) and the research community to offer Internet access from vehicles. Special devices (called mobile routers [MRs]), located in the vehicles, handle the communication with the fixed infrastructure and provide access to passengers' devices using a convenient radio technology. This protocol associates each egress interface of a MR with two distinct addresses, much like what is done in Mobile IP [START_REF] Banerjee | Mobility support in wireless internet[END_REF]. The permanent home address MRHoA is obtained in the home network and has the same prefix as the home link. The temporary care-of address MRCoA is obtained in the visited network and formed based on the prefix advertised on the visited link.

II. PROPOSED ARCHITECTURE

Large handover latency causes the loss of a large number of MNN packets. Therefore the reduction of handover latency is a very important requirement in enabling mobile networks to support multimedia communications. NEMO, which has large handover delay and high packets loss ratio, cannot meet the requirements for the real-time applications. To address these issues, a secure and faster handover scheme for trains based on multiple antennas cooperation is proposed in this paper.

Link layer switching

Mobile networks are more likely to be multihomed than the mobile nodes are. Multihoming refers to a situation where a node can choose between several paths to reach a correspondent.

The multiple choices are due to the train router having several interfaces. Such a configuration is particularly useful in mobility contexts because it ensures mobile entities remain permanently connected to the internet even in the following situations: loss of connectivity (as a result of moving out of a coverage area or because wireless technologies are more subject to interference), lack of connectivity (a given technology cannot cover all geographic areas) or lack of bandwidth (technologies with high bandwidth are generally not available for mobile users).

To take advantage of this technique, we propose a multihoming-based seamless handover scheme using a multihomed MR with dual antennas in NEMO on railway trains [START_REF] Ben Reguiga | Fast handoff management for Internet access on train[END_REF] (Figure 1). The two antennas are located at the two far ends of the mobile train. One of the two egress interfaces of MR can continuously receive packets while the other is undergoing a handover. Therefore, the proposed scheme has no service disruption or packet losses during handovers.

Figure.2 PROPOSED ARCHITECTURE

Care of Address pre-configuration

To achieve a low-latency and less-loss handover, the objective of our proposal is to obtain New CoA before handover. To make full use of the train characteristics such as the fixed passenger railway lines and regular movement of trains, we can prepare in advance the list of handover candidate cells and by consequence next ARs. We can thus prepare CoA configurations in advance.

When MR leaves the station home network, it registers its home address to HA. According to the train predefined trajectory, the HA could know the future ARs that the train will meet and can pre-establish with them the list of next CoAs. The HA maintains this list with the right order according to the first crossing AR (CoA n°1), second AR (CoA n°2)…

Security issues

A security research group, "The Hacker's Choice" has reverse-engineered the femtocells operated by a British mobile operator and discovered that it could be used to make illegal calls and send text messages [START_REF] Bright | Insecure vodafone femtocells al-low evesdropping, call fraud[END_REF]. In this paper, we present a secure ITS femtocell scenario and investigate the feasibility of using our solution inside MOBIKE architecture [START_REF]IKEv2 Mobility and Multihoming (MOBIKE)[END_REF] for better security.

The main scenario for MOBIKE is enabling a remote access VPN user to move from one address to another without reestablishing all security associations (SA) with the VPN gateway. MOBIKE updates only the outer (tunnel header) addresses of IPsec SAs, and the addresses and other traffic selectors used inside the tunnel stay unchanged. Thus, mobility can be (mostly) invisible to applications and their connections using the VPN.

III. THE VIRTUAL INTERFACE

Figure . 3. VIP INTERFACES MANGEMENT

The principium of multihomed train with dual antennas was proposed in [START_REF] Park | IP mobility support with a multi-homed mobile router[END_REF]. But the authors consider different IP address for each antenna (ant2 and ant1). This leads to an additional signaling cost and unnecessary antenna switching: When the Head ant1 crosses the boundary of a new cell, it achieves a new handoff with the NAR. When later the trail-ant (ant2) crosses the boundary of the NAR (because of train movement), a second handoff is performed to switch traffic to the ant2. This implies additional signaling cost and binding updates to the NAR and the HA. In our point of view, the solution lies on having the same IP and MAC address on the two MR interfaces ant1 and ant2. By assigning to all the physical devices on the MR the same IP and MAC addresses (with the rule that only one is active in the same subnet at the same time t), the mode of communication during handover will be transparent to higher layer transport protocols.

However, the Internet routing model forces routers to have different MAC and IP address for each active physical interface in the MR. This means that in our scenario the MR will have two different IP addresses one for each antenna ( IP1 for ant1 and IP2 for ant2). Since this is not possible with today implementations, we added a new virtual MAC layer between the hardware level and IP level (Figure 3). We assign a unique unicast IP address to this virtual MAC address, consequently, application might think of any flow as dealing with traffic corresponding to a single interface only.

The proposed interface hides the presence of the different router interfaces to the applications layer by providing the illusion of a unique interface and by consequence IP address (Figure 4). All corresponding node's flows are sent to this virtual MAC interface: before the handoff, it will correspond to ant1 and after the handoff it will correspond to ant2. At any time, the virtual interface must manage the changes in network connection's status (handovers). That's why; it will periodically evaluate interface's status and use this information to select the good interface for communication.

The virtual MAC groups all information from the interfaces in a specific table that is dynamically updated [START_REF] Afifi | VIP: Virtual Interface Prototype for Mobile Communication[END_REF]. After the virtual interface is created, all the network interfaces that have to be attached must be configured as slaves. The MAC address of the virtual interface is taken from its first slave interface. This MAC address is then passed to all following interfaces (Figure 4) and remains persistent (even if the first one is removed). The way the virtual interface is implemented violates this unique MAC address per interface standard, by deliberately making several NICs have the same MAC address. The two MR antenna ant1 and ant2 will share the same IP address thanks to VIP implementation. When the ant1 leaves the AR1 coverage, the ant2 will be used by the virtual interface to continue receiving packets to the MR with the same IP address. The network is thus unaware about the change. One the train complete L3 handover with the new AR through ant1, it switches to receive traffic through ant1 and can use the new CoA.

VI. PERFORMANCE ANALYSIS

In this section, a deep analysis of our solution is proposed based on the handover latency and its impact on packet loss.

Velocity consideration

The time duration (Td) during which ant2 remains connected to PAR after ant1 leaves PAR depends on the distance (d) between ant1 and ant2, and the speed (v) of the mobile network, i.e:

Td = d/v
For a very-low loss handover, ant2 should remain connected to PAR for duration greater than or equal to the handover latency (Th) of ant1, i.e., Td ≥ Th. For example, suppose a mobile network on a train where d = 100 meters and v = 100 km/hr. The value of Td will thus be 3.6 seconds, which is a sufficient time to allow ant1 to complete binding updates with its HA before ant2 leaves PAR. .

Signaling cost

We have analyzed and compared the protocol cost of our VIP-based proposal with basic NEMO [START_REF] Ben Reguiga | Fast handoff management for Internet access on train[END_REF]. The handover latency is given by:

ܵ ோெை = ܵ ଶ + +ܵ CoA + ܵ ு_ (1)
ܵ ூ = ܵ ଶ + ܵ dd + ܵ ுି (2)
From ( 1) and ( 2), it's clear that we have:

ܵ ூ < ܵ ோெை
Using VIP has a cost since packets have to go through an additional layer before being sent on the physical medium and vice-versa. To measure this cost, we studied the impact of VIP on UDP applications and compare the result with that of the standard Linux implementation (section 3).

Test-bed

We implemented a prototype for performance evaluation. The Femto System Architecture used in our test-bed is shown in Figure 5. It is largely based on the work of 3GPP working group SA3 which is responsible for the overall security of all 3GPP systems. The system architecture is described as having the following features:

• The backhaul link, is connected from the Femto AP (FAP) to the operator's core network via a SeGW (Security Gateway).

• SeGW represents operator's core network to perform mutual authentication with FAP.

• Security tunnel is established between FAP and SeGW (through Mobike) to protect information transmitted in backhaul link.

•An AAA server authenticates the hosting party module, a SIMcard based mechanism that is optionally deployed in the Femto architecture to help the operators effectively managing the FAP.

We choose to install Strongswan software [START_REF]MOBIKE open source[END_REF] because it's currently the only open source implementing IKEv2 and supporting MOBIKE, and therefore we use it to study the feasibility of using this protocol on femtocell networks. Finally, to simulate the network conditions, we installed Iperf [8], which is an open source software used as a testing network tool that can create UDP and TCP data streams and measure the network performance: bandwidth, delay and packet losses. we used wireshark software [START_REF]Network protocol analyzer[END_REF] for traffic analysis. We conducted experiments on several Linux hosts (Figure 5) whose main features are shown in Table1.

Handoff latency

We measured handoff latency as the time between the last packet from MN and first received packet after handoff. Two tests were performed according to IKE authentification methods (Figure 6): in the first scenario MOBIKE used public-key cryptography based on RSA algorithm. The second scenario uses certificate x509 to authenticate the two peers of the IPsec tunnel.

The VIP implementation was running during all the tests. Our solution performs with a very low handoff delay of 47 ms in maximum (Figure 6). Compared to previous solutions such as NEMO (where the handoff delay is about 1s [START_REF] Ng | Analysis of multi-homing in network mobility support[END_REF]), our proposal reduces considerably the handoff latency. The performance measurements match our expectations and effectively show the advantages of implementing mobility management at lower layer. As the switching process is very fast, the handoff is performed in a seamless way without long period of interruption.

Figure 7 shows throughputs measurements. As we can see, VIP overhead is very small compared to that of the standard Linux implementation; especially in the case of UDP traffic where it could be equal to zero. This can be explained by the fact that VIP operates at the link layer which does not reduce the volume of data a packet may include. Moreover, as all the physical interfaces share the same MAC address (as the virtual interface), no MAC address translation or swapping is needed; which means no additional packet encapsulation /decapsulation. VIP overhead is only due to the time needed by the virtual interface to consult its local commutation table to decide on which physical interface it could send data.

Figure 4 .

 4 Figure 4. VIP IMPLEMENTATION

Figure . 5 Figure . 6

 56 Figure .5 Test-bed scenario

Figure . 7

 7 Figure .7 Throughput overhead for UDP traffic


Seifeddine Bouallegue

Kaouthar Sethom

Guy Pujolle

Power Optimization in Two-tier Networks

Keywords: Macro, microcell, LTE, mobility management

A future cellular network demands a new architecture that can facilitate the autonomous deployment of the infrastructure similar to Wi-Fi. A novel method of deploying a cellular network has been introduced with small cellular base stations, or femtocells, autonomously deployed by users in an underlay macro-cellular network. This autonomous cellular concept allows the network to grow in an organic manner, which reduces the traditional work on infrastructure installation, network configuration and maintenance. To this end, we propose hereafter an intelligent and autonomic system for power control in the femtocell context. The first simulation results seem to confirm the advantage of our solution in reducing energy consumption.

INTRODUCTION

Femtocell networks are unique in that they are largely installed by customers or private enterprises often in an ad hoc manner without traditional RF planning, site selection, deployment and maintenance by the operator. Moreover, as the number of femtocells is expected to be orders of magnitude greater than macrocells, manual network deployment and maintenance is simply not scalable in a cost-effective manner for large femtocell deployments. Femtocells must therefore support an essentially plug-and play operation, with automatic configuration and network adaptation. In the LTE overall description specification [1], the self-configuration process is defined as the process where the newly deployed base stations are configured by automatic installation procedures to get basic parameters and download necessary software for operation. In this paper, we propose a new energy-aware handoff algorithm that tries to adjust femtocell power with the regards to unwanted mobility events.

There are several reasons for the growing awareness of energy-efficient wireless networks in the telecommunication community. Increasing energy prices imply that electricity bills have become a significant cost factor for mobile operators. In addition, mobile telephony and mobile broadband are entering new emerging markets, with an increasing share of base stations that are not connected to the electricity grid. Such off-grid sites are typically diesel powered, where fuel is costly and distribution often unreliable for distant sites that are difficult to access. For operators with many off-grid sites, energy provision may contribute up to 50 percent of their total operational cost. There is also an increasing awareness in the society about manmade climate effects, and the need to slow down global warming. Moreover, political initiatives are beginning to put requirements on manufacturer and operators to lower CO2 emissions of communication networks. The rest of the paper is organized as follows: section 2 describes state of the art on energy management in wireless networks. Section 3 presents our algorithm for femtocell power adjustement. Section 4 and 5 try to evaluate our proposal through an analytical model and simulations.

STATE OF THE ART

The transmit power of femtocell consists of: (i) pilot power (responsible for cell selection and channel estimation) and, (ii) traffic power (includes signalling power and data power). Pilot power determines the coverage of the cell: large pilot power results in a large cell coverage and small pilot power may lead to insufficient coverage. Moreover the larger the pilot power the less the power left for traffic, which result in minimizing the throughput of the femtocell.

The related work in the literature on cellular power optimization mostly deals with centralized computation methods. Such mechanisms involve the calculation of parameters such as number and locations of base stations (BS), pilot channel transmit powers or antenna configurations using a central server running an optimization algorithm. The configuration statistics of the whole network are passed on to the central entity, which then computes the optimal/quasi-optimal configuration settings. The algorithms are Genetic Algorithms, Greedy Algorithms, Simulated Annealing or other classical optimization methods [START_REF] Ho | channel femtocells on the call dro scenario[END_REF][START_REF] Lieska | La Optimization with Genetic Algorith[END_REF][START_REF] Molina | Athanasiadou Location of Base-Stations for Opt New Combinatorial Approach[END_REF][START_REF] Siomina | Yu of Service Coverage and Base Stat UMTS Networks[END_REF][6].

POWER SAVING ALGORITHM

We consider an overlay wireless networ macrocell and femtocell. During oper on the number of mobility events a collected and used for further refineme by self-optimization of the pilot power We here propose an optimization m decision based on unwanted mobi transient users into account that briefly femtocell and handout immediately afte within 'R' meter of radius of the m because the SINR of mobile w assumed to be quite high.

2. When the mobile user is movin velocity, no handoff from the mac executed. The mobile remains Macrocell. As a user with very undergoes huge number of mac within a very short period of time the macro BS thus increases unn in this paper we have considered a Vth (see section 4).

The general principle of the proposed s in Figure 1.

Incoming call

Yes

NO V< Vth

Rej

Power saving Algorithm rk with two layers: ration, information and their time are ent of the coverage r of the femtocell. method that takes ility events from y hand over to the er passing. Scenario f the system model deployed randomly with varied velocity ype:

macro to femtocell macro base station within this area is ng at a very high cro to the femto is attached to the y high velocity it cro/femto handoff e. The overhead of necessarily. Hence, a velocity threshold scheme is depicted 0,5dBm. However, the minimum FAP power should cover U1 user if he is attached to his femtocell.

ii. The femtocell then starts a new mobility event count for the updated configuration. If the number of unwanted events is smaller or equal to n2 events for a time period t2, this is a stability phase, no power modification.

iii. Finally, if the number of unwanted events is bigger to n2 for a time t2, the femtocell increases its pilot power by +0,5dBm, to provide improved indoor coverage. The maximum Power is limited by an upper value Pmax to avoid inter-femtocell interference.

This means that at the initial stage:

(1) Emin= Eidle, and Emax= Eactive However, at the optimization stage:

(2)

If U1exists

Emin= E(just to cover U1) Else Emin= Eidle,

In case of power increasing scenario, the Femtocell j must measure the level of other-cell interference I that is received from its vicinity (V) as it's illustrated in the figure below. The interfering signal received at the edge border of the cell at the ith iteration is expressed by:

(3)

∑ d , 2 Rjd , cosθ

Where: is the current femtcell radius, d , is the distance between the Femto j and the Femto k, is the interfering signal from the macrocell , is the surrounding femtocells k transmit power and, , , are the path loss exponents and the wall penetration loss. The femtocell j evaluates the received interference plusnoise power and Pmax is calculated so that:

(4) 10 log <

Where, i difined threshold for tolerate interference level at femtocell j and W is the noise.

ANALYTICAL MODEL

In this section, a simple analytic model is developed to mainly analyze the performance parameters of the proposed scheme.

Let's first begin by defining the speed upper bound for our proposal. Given mobile user UE with an average speed v and traversing a two-tier network (for a distance Δ), a valid handover occurs if: the time that the mobile will spend in the femtocell is long enough to compensate for the data loss due to the switching overhead. This means that:

(5)

∆

Where:

is the handover delay , is the throughput of the femtocell and is the trouhput of the macro.

is a hysteresis factor introduced to avoid handover when the two competing cells have negligible bandwidth difference.

In our proposal, the active state is divided into 3 cases:

1. The number of unwanted handoff k is under n1 in which case the femtocell Power P has to be increased by +0,5dBm. With the respect of an upper power limit Pmax. 2. The number of unwanted handoff is n1≤k≤n2 in which case no change in femtocell Power (so E is set to Ecurrent) 3. The number of unwanted handoff is k> n2 in which case P has to be decreased by -0,5 dBm (with respect to an under power limit that correspond to the idle state Pidle)

Let's now try to calculate the probability of an unwanted handoff.

In this work, the P(k, T) denotes the probability of k handover events occurring within the period time T . In general, the Poisson distribution is represented as

, !

Where λ is the average proportion of the event happened. The probability of a handover which has not occurred within time Tj is 0, , Where, and tj is the time period of the received SNR of Femtocellj (FBSj) from the UE is larger than the threshold value. The λjTj is the average handover number within the time duration Tj.

The probability of handover is then:

1

The average energy consumption for the data transmission of a UEj (user equipement) performing a handover in the Ashraf protocol [START_REF] Claussen | W femtocell coverage to minimize t mobility signalling[END_REF] is:

(8) 1
Where is the average energy consumption of the data transmission of an UE before entering the coverage of FBSj.

We introduce two values of tdwell and texpected, where tdwell is the dwell time of a UE of keeping the communication with FBSj, where the UE is in the coverage of FBSj and texpected is the expected transmission time of data of the UE. If a UE cannot completely transmit all of the data within the tdwell, then an unwanted handoff occurs.

The probability of a wanted handover is when the remainder data of UEj can be completely uploaded within time texpectedj through the FBS i.e. no handover within texpectedj: [START_REF] Moon | Effects of user-deployed, coop probability in a residential ahteenmaki[END_REF] 0,

where the is the average number of complete uploading within time tdwell k , where texpected k is the average expected transmission time using FBS k and tdwell k is the time starting from the UE communicating with FBS k and stopping to communicate with FBS k .

The expected transmission time can be calculated as:

(10)

t D R
Where, Dremainder is the remainder data and R the average transmission rate of FBS k .

At initial time t= 0: The femtocell energy can be Ecurrent =Eidle if no attached user to the femto else Ecurrent=Eactive.

(11)

1 ∑ 1 ∑ 1 1 Where: If j< n1 E opt = , 5 if If n1=<j< n2 E opt =Ecurrent If j> n2 E opt = , 5 if
It is easily seen that 0; since and .

Our proposal outperforms a classical approach in terms of energy consumption.

SIMULATION RESULTS

In this section, simulation results are pre the performances of the proposed networks with femtocells. For compa performances of the network with Ashr also presented. Ashraf et al. [START_REF] Claussen | W femtocell coverage to minimize t mobility signalling[END_REF] recently proposed procedure that allows the femtocell to off its radio transmissions and associate not involved in an active call. From our method is not realistic because wake up time a new user come, which will be and will increase the ping pong effects i Figure 4 shows that our algorithm blocking probability because the net optimized in order to eliminate unwante Figure 5 confirms that our proposal red the amount of energy consumption (the 25% in a heavy network). These sim power of a femtocell implementing ou allocation algorithm. The power is aut auto-optimized according to users' mo that femtocells have different coverag optimized transmitting power. Our context-aware then previous works. Mo holes in the network compared to [START_REF] Claussen | W femtocell coverage to minimize t mobility signalling[END_REF].

CONCLUSION

In this paper, we have proposed an mobility based algorithm for redu handoff in hierarchical macro/femto balancing the load of macro and the fem energy consumption. The performance esented to evaluate scheme in LTE arison purpose, the raf solution [START_REF] Claussen | W femtocell coverage to minimize t mobility signalling[END_REF] are bability an energy-saving completely switch ed processing when point of view, this p will be done each energy consuming in the network. reduces handover twork coverage is ed mobility events.

duces considerably e gain is more than mulations show the ur dynamic power to-configured, then bility. We can see ge due to different proposal is more oreover, it decrease n energy efficient ucing unnecessary o networks while mto BSs at minimal e of the proposed algorithm is also analyzed us Simulations show good perform

Figure 1 :

 1 Figure 1: Mobility Management S

Figure 2 :

 2 Figure 2: Power Saving A

Figure 3 :

 3 Figure 3: Interference Evaluation Scheme

Figure 4 :

 4 Figure 4: Handover blocking prob

Figure 5 :

 5 Figure 5: Network ene


Aicha Ben Salem

Seifeddine Bouallegue

Kaouthar Sethom

A QoS based Resource Allocation in Femtocell Networks

Keywords: Wireless networks, long-term evolution, resource allocation

LTE has been identified as a new wireless standard by the 3rd Generation Partnership Project (3GPP) which is using the VoIP to transmit the voice services and packet the data for all services. Traffic scheduling plays an important role in LTE technology by assigning the shared resources among users in the most efficient manner.

The main objective of this paper aims to design an efficient scheduling algorithm for LTE standard. It can not only obtain the high system performance but also maintain the proportional fairness. Each user is allocated the requested resource according to the predefined QoS parameters. The scheduling algorithms performances on the downlink were measured using a MATLAB based system level simulation.

I .INTRODUCTION

A solution to maintain this LTE performance in user dense areas or areas with bad reception is the deployment of socalled femtocells. Femtocells are small base stations that are deployed indoors and share the RF spectrum with the whole mobile network. The idea is that femtocells will increase mobile operators network coverage and capacity while it at the same time increase users data throughput.

The QoS provisioning has been an important issue in the mobility management of wireless femtocell networks [START_REF] Shakkottai | Scheduling Algorithms for a Mixture of Real-Time and Non-Real-Time Data in HDR[END_REF][START_REF] Basukala | Performance Analysis of EXP/PF and M-LWDF in Downlink 3GPP LTE System[END_REF][START_REF]Performance Analysis of Two Packet Scheduling Algorithms in Downlink 3GPP LTE System[END_REF][START_REF] Research | LTE MAC Scheduler & Radio Resource Scheduling[END_REF][START_REF] Nasralla | A downlink scheduling approach for balancing QoS in LTE wireless networks[END_REF]. To provide QoS in wireless networks, the Radio resource management (RRM) plays a crucial role in managing the limited radio resources effectively [START_REF] Piro | Simulating lte cellular systems: an open source framework[END_REF]. The Packet Scheduler is an entity of RRM in LTE that resides in the MAC layer of eNodeB [START_REF] Gpp | Requirements for further advancements for EvolvedUniversal Terrestrial Radio Access (E-UTRA) (LTE-Advanced)[END_REF][START_REF] Iturralde | Resource allocation for real time services using cooperative game theory and a virtual token mechanism in LTE networks[END_REF]. It is responsible for the allocation of shared radio resources among the mobile User Equipments (UEs). The scheduler assigns resources to users with the granularity of resource blocks (RBs) every TTI, based on the channel condition feedback received from UEs in the form of Channel Quality Indicator (CQI).

Due to the importance of the scheduling process at the MAC layer in LTE, various packet scheduling algorithms have been developed to support RT and NRT services, comprising the most commonly used Proportional Fair (PF), M-LWDF and Exponential Proportional Fair (EXP-PF) schedulers [START_REF] Shakkottai | Scheduling Algorithms for a Mixture of Real-Time and Non-Real-Time Data in HDR[END_REF][START_REF] Basukala | Performance Analysis of EXP/PF and M-LWDF in Downlink 3GPP LTE System[END_REF][START_REF]Performance Analysis of Two Packet Scheduling Algorithms in Downlink 3GPP LTE System[END_REF][START_REF] Research | LTE MAC Scheduler & Radio Resource Scheduling[END_REF]. With regard to the previously mentioned schedulers, each flow is assigned a metric value depending on specific measurements. Therefore, the bearer which carries the flow with the highest metric value will be scheduled first at the correspondent, Transmission Time Interval (TTI).

The QoS guarantees become more feasible when radio resources are allocated according to the well-defined demands of traffic types rather than by estimation. In this paper, we focus on how to perform scheduling at the eNobeB while providing QoS to users according to their needs and network access priority. .

II. PROBLEM STATEMENT

Traditionally, macrocellular networks require complex and expensive manual planning and configuration. Currently, 3GPP LTE-Advanced and IEEE 802.16m are standardizing the Self Organizing Network (SON) concept for IMT-Advanced networks. The main functionalities of SON for integrated femtocell/macrocell networks are selfconfiguration, self-optimization, and self-healing [START_REF] Mhiri | A Survey on Interference Mitigation Techniques in Femtocell Self-Organizing Networks[END_REF]. The self-configuration function includes intelligent frequency and bandwidth allocation among neighboring F-BSs; selfoptimization attribute includes optimization of transmission power among neighboring F-BSs, maintenance of neighbor cell list, coverage control, and robust mobility management; and self-healing feature includes automatic detection and resolution of most failures. Fig1. shows the basic features and framework of the proposed SON-capable integrated femtocell/macrocell network architecture. Network operators may need to deploy the hierarchical femtocell network architecture based on centralized or distributed manner. The centralized architecture is necessary for cooperative hotspot coverage, but the distributed and flat way is required for individual, ad-hoc, and random femtocell coverage. In this paper, we propose a decentralized resource management with open access mode in Femtocell networks.

III. PROPOSEd RESOURCE ALLOCATION

Our solution consists of two steps:

A. Distribution of the total bandwidth among traffic classes

To resolve this resource allocation problem [START_REF] Iturralde | Resource allocation for real time services using cooperative game theory and a virtual token mechanism in LTE networks[END_REF] proposed to use game theory. Game theory is a mathematical tool for analyzing the interaction of two or more decision makers. A (strategic) game consists of three components: a set of players, the strategy set for each player and a utility (payoff) function for each player measuring the degree of "happiness" of the player. The users interaction in a wireless network can be modeled as a game in which the users terminals are the players in the game competing for network resources (example bandwidth). Any action taken by a user affects the performance of other users in the network. Game theory is the natural tool for studying this interaction.

The resource allocation problem is where a finite divisible bandwidth capacity B must be divided among a set N of flow users. For each class A n , each group of flows claim a bandwidth share ∈ . The vector of class resources claim is denoted as g ≡ (g i ) i N , with g i is the product of ki and b i , g i = k i b i . Each player is represented by a class. The benefit of this division is the total resources at each TTI. A coalition is defined when several classes share an amount of resource, and the benefits should be distributed between all of the members of the coalition.

We consider a dynamic allocation process, and the number of users in each class is variable. In a bandwidth allocation problem, the classes of users represent the players who benefits from capacity B. We define 3 users classes as players in our scenario N= {UsP1, UsP2, USP3 }while taking into account their priority level in the femtocell system:

 UsP1 : Users with priority P1  UsP2 : Users with priority P2  UsP3 : Users with priority P3.

To resolve this resource allocation problem we propose to use the simple equation ( 1):

(

BPk = min ( B -∑i=0,k-1 bpi ; ∑i=0,2 ni(Pk) x bpk)

Where -BPk: is the bandwidth allocated to the priority class Pk.

-n i (P k ): the number of flow of type i in the class Pk Following equation ( 1), we can see that users with higher priority are satisfied before the others. At each TTI, a new redistribution of resources is performed. When a new flow joins the network and claims for resources, the arbitrator must start to re-divide the bandwidth, this is executed in the next TTI. Each class has its corresponding bandwidth chunk and must divide the resource among their flows. Our solution is less complex than [START_REF] Iturralde | Resource allocation for real time services using cooperative game theory and a virtual token mechanism in LTE networks[END_REF] where at each TTI, a new heavy redistribution of resources is performed through game theory (CPU and time consuming). When a new class of users joins the game and claims for resources, the femtocell must start a new game to re-divide the bandwidth, this is executed in the next TTI.

In our case, each class has its corresponding bandwidth chunk and must divide the resource among their users. As we can see the execution of the algorithm satisfies P1 users first then P2 one, the remaining bandwidth is for P3 clients.

B. Step 2: Packet scheduling

Due to the voluminous and equal growth of multimedia services and NRT services, it is worth thinking of tailoring a downlink packet scheduling scheme that copes with both service classes simultaneously, delivers balanced QoS and utilizes the system radio resources efficiently.

Resource allocation for each UE is usually based on the comparison of per-RB metrics: the k-th RB is allocated to the j-th user if its metric mj;k is the biggest one. QoS differentiation is handled by associating a set of QoS parameters to each flow. Knowing the values of such parameters, the scheduler can treat data to guarantee some minimum required performances, either in terms of guaranteed data rates or of delivery delays.

Almost all QoS aware schedulers is somehow inspired by the classical proportional fair (PF) scheduler [START_REF] Shakkottai | Scheduling Algorithms for a Mixture of Real-Time and Non-Real-Time Data in HDR[END_REF]. We note that the PROP-FAIR rule does not account for delays of packets and can result in poor delay performance. M-LWDF algorithm thus incorporates HOL packet delay together with PF properties (e.g. the ratio of achievable data rate to the average data rate) when determining users' priority. M-LWDF prioritizes the user with higher HOL packet delay and better channel conditions relative to its average levels [START_REF] Basukala | Performance Analysis of EXP/PF and M-LWDF in Downlink 3GPP LTE System[END_REF]. A very promising strategy was presented in [START_REF] Nasralla | A downlink scheduling approach for balancing QoS in LTE wireless networks[END_REF]. It adopts the consideration of the queue size and the packets delay parameters in the VT-M-LWDF and M-LWDF rules respectively.

The scheduling rule is given by:

( MATLAB and LTE-Sim simulator [START_REF] Piro | Simulating lte cellular systems: an open source framework[END_REF] are used to perform our tests. We use a single cell scenario where users are moving at speed of 3 km/h in random directions (random walk). LTE-Sim simulator is used to perform tests.

As it can be seen in Figure 2, two classes P1 an P3 are competing for the bandwidth resources. Our bandwidth algorithm treats in priority P1 traffic, even if no more resources are available for the rest of classes. In fact after serving P1 users the rest of bandwidth is equal to 40Kbps; the total RBs for the class P3 is zero because 40Kbps doesn't satisfied one Video stream.

To better understand the obtained results in figure 3, the following notations are used: "EXP" represents the exp rule scheduler; "ML" for M-LWDF algorithm,"S" represents our solution.

With respect to these measures (Figure 3), we found that our new algorithm performs the best among the classical scheduler because it treats differently any type of flows RT and NRT.

Our results show that our mechanism used in conjunction with an intelligent scheduling algorithm can improve the efficiency of this algorithm for multimedia services.

Due to the voluminous and equal growth of multimedia services and NRT services, it is worth thinking of tailoring a downlink packet scheduling scheme that copes with both service classes simultaneously, delivers balanced QoS and utilizes the system radio resources efficiently. In other words, the users nowadays request not only video and VoIP services but also CBR, Internet browsing and best-effort services simultaneously. .

VI. CONCLUSION

This paper mainly focused on the performance of a modified EXP-rule and M-LWDF packet scheduling algorithms in downlink LTE femtocell system. Our proposed solution combine the two scheduling algorithms in order to create an intelligent scheduler which insure a throughput optimal according to the number of users per femtocell and their access priority. Simulation results argue in favor of our solution

Fig. 1

 1 Fig.1 Bandwidth allocation

Fig. 2 :

 2 Fig.2: Example of scheduling between P1 and P2 classes