Mariem Abdelmoula
email: mariem.abdelmoula@unice.fr

Daniel Gaffe
email: daniel.gaffe@unice.fr

Michel Auguin Leat

AUTSEG: Automatic Test Set Generator for Embedded Reactive Systems

Keywords: AUTSEG, Test Sets, State Machines, States Space Covering, Sequences Generation, Contactless Smart Card, Specification, Synchronous Model

One of the biggest challenges in hardware and software design is to ensure that a system is error-free. Small errors in reactive embedded systems can have disastrous and costly consequences for a project. Preventing such errors by identifying the most probable cases of erratic system behavior is quite challenging. In this paper, we introduce an automatic test set generator called AUTSEG. Its input is a generic model of the target system, generated using the synchronous approach. Our tool finds the optimal preconditions for restricting the state space of the model. It only works locally on significant subspaces. Our approach exhibits a simpler and efficient quasi-flattening algorithm than existing techniques and a useful compiled form to check security properties and reduce the combinatorial explosion problem of state space. To illustrate our approach, AUTSEG was applied to the case of a transportation contactless card.

Introduction

Verifying automatically and formally that a system is working correctly is not trivial nowadays due to the increasing complexity of computer programs and their strong interaction with the environment. An important class of systems facing such problems are reactive systems. They continuously react and respond to their environment. Reactive systems belong to the large family of FSMs (Finite State Machines). They are ubiquitous in everyday life, varying from simple thermostats to the control of nuclear power plants, avionics, telesurgery, and online payment. Security for these systems is critical; even minor errors are unacceptable. In this paper, we focus on verification of embedded software controlling the reactive system behavior. To illustrate our approach, we aim to verify the implementation of the OS integrated in a contactless smart card for transportation. We specifically target the verification of the card's functionality and security features. Smart Cards are ubiquitous, with more than 200 million used across the globe for transportation, telephony, health insurance, banking, ID, etc. Frauds are especially critical for banking cards, as counterfeiters are able to exploit the vulnerabilities of coding systems.

Furthermore, the card's complexity makes it difficult for a human to identify all possible sensitive situations or to validate it by classical methods. We need approximately 500 000 years to test the first 8 bytes if we consider a classical Intel processor that generates 1000 test sets per second. As well, combinatorial explosion of possible modes of operation makes it nearly impossible to attempt a comprehensive simulation. The problem is exacerbated when the system integrates data processing, so results have significant effects on system behavior. Thus, we strive for highly-automated testing techniques. We aim as well to describe with symbolic means the reachable state space model of the card specification for a particular security property. Expertise in symbolic verification and synchronous languages are required to automatically generate exhaustive test sets that represent critical situations.

We hence focus on a set of techniques known as formal methods, based on the Binary Decision Diagram BDD [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF] that are used in computer science to ensure correct system behavior. We propose in this paper, an automatic test set generator called AUTSEG. Generating automatic test sets and covering all transitions is not a new research area. However, we notably address in this paper the state space explosion problem. We first generate a powerful quasi-flattening algorithm which performs a simple and deterministic model, thus facilitating code generation. We qualify by a second algorithm the correct behavior of the global system, without requiring coverage of all system states and transitions.

In the remainder of this paper, we give an overview of related work in Section 2. We present in Section 3 our global approach for test generation. AUTSEG and details on its capabilities are presented in Section 4. Section 5 presents the application of our generator to a specific contactless card for transportation. Experimental results are shown in Section 6. Finally, Section 7 concludes the paper with some directions for future work.

Related Work

Lutess V2 [START_REF] Seljimi | Automatic generation of test data generators for synchronous programs: Lutess v2[END_REF] is a test environment, written in Lustre, for synchronous reactive systems. It automatically generates tests that dynamically feed the program under test from the formal description of the program environment and properties. This version of Lutess deals with numeric inputs and outputs unlike the first version [START_REF] Dubousquet | An overview of lutess: A specification-based tool for testing synchronous software[END_REF]. Lutess V2 is based on Constraint Logic Programming (CLP) and allows the introduction of hypotheses to the program under test. Due to CLP solvers' capabilities, it is possible to associate occurrence probabilities to any Boolean expression. However, this tool requires the conversion of tested models to the Lustre format, which may cause a few issues in our tests.

B.Blanc presents in [START_REF] Blanc | Handling state-machines specifications with gatel[END_REF] a structural testing tool called GATeL, also based on CLP. GATeL aims to find a sequence that satisfies both the invariant and the test purpose by solving the constraints problem on program variables. Contrary to Lutess, GATeL interprets the Lustre code and starts from the final state and ends with the first one. This technique relies on human intervention, which is stringently averted in our paper.

C.Jard and T.Jeron, present TGV (Test Generation with Verification technology) in [START_REF] Calam | Specification-Based Test Generation With TGV[END_REF], a powerful tool for test generation from various specifications of reactive systems. It takes as inputs a specification and a test purpose in IOLTS (Input Output Labeled Transition System) format and generates test cases in IOLTS format as well. TGV allows three basic types of operations: 1. It identifies sequences of the specification accepted by a test purpose, based on the synchronous product; 2. It then computes visible actions from abstraction and determinization; 3. Finally, it selects test cases by computation of reachable states from initial states and co-reachable states from accepting states. A limitation lies in the non-symbolic (enumerative) dealing with data. The resulting test cases can be big and therefore relatively difficult to understand. D.Clarke extends this work in [START_REF] Clarke | Stg: A symbolic test generation tool[END_REF], presenting a symbolic test generation tool called STG. It adds the symbolic treatment of data by using OMEGA tool capabilities. Test cases are therefore smaller and more readable than those done with enumerative approaches in TGV. STG produces the test cases from an IOSTS specification (Input Output Symbolic Transition System) and a test purpose. Despite its effectiveness, this tool is no longer maintained.

[7] describes STS (Symbolic Transition Systems), quite often used in systems testing. STS enhances readability and abstraction of behavioral descriptions compared to formalisms with limited data types. STS also addresses the state explosion problem through the use of guards and typed parameters related to the transitions. At the moment, STS hierarchy does not appear very enlightening outside the world of timed/hybrid systems or well-structured systems. Such systems are outside of the scope of this paper.

ISTA (Integration and System Test Automation) [START_REF] Xu | A tool for automated test code generation from high-level petri nets[END_REF] is an interesting tool for automated test code generation from High-Level Petri Nets. ISTA generates executable test code from MID (Model Implementation Description) specifications. Petri net elements are then mapped to implementation constructs. ISTA can be efficient for security testing when Petri nets generate threat sequences. However, it focuses solely on liveness properties checking, while we focus on security properties checking.

J.Burnim presents in [START_REF] Burnim | Heuristics for scalable dynamic test generation[END_REF], a testing tool for C called CREST. It inserts instrumentation code using CIL (C Intermediate Language) into a target program. Symbolic execution is therefore performed concurrently with the concrete execution. Path constraints are then solved using the YICES solver. CREST currently reasons symbolically only about linear, integer arithmetic. Closely related to CREST, KLOVER [START_REF] Li | Klover: a symbolic execution and automatic test generation tool for c++ programs[END_REF] is a symbolic execution and automatic test generation tool for C++ programs. It basically presents an efficient and usable tool to handle industrial applications. Both KLOVER and CREST cannot be adopted in our approach, as they accommodate tests on real systems, whereas we target tests on systems still being designed.

Global Process

Let us start with a description of the global architecture we have designed for our test. Fig. 1 shows 4 main operations explained in detail in the following sections. 2. Quasi-flattening process: we flatten only hierarchical automata, the rest of automata remaining parallel. This offers a simple model and brings more flexibility to identify all possible evolutions of the system.

3. Compilation process: it generates an implicit automaton represented by a Mealy machine from an explicit automaton. This process compiles the model, checks the determinism of all automata and ensures the persistence of the system behavior.

4. SSG (Sequences Symbolic Generator): it extracts necessary preconditions which lead to specific, significant states of the system from generated sequences.

Quasi-flattening process

The straightforward way to analyze a hierarchical machine is to flatten it (recursively substitute in a hierarchical FSM each super state with its associated FSM), then apply as an example a model-checking tool on the resulting FSM. Let's consider the model shown in Fig. 2, which shows automata interacting and communicating between each other. Most of them are sequential, hierarchical automata (e.g. automata 1 and 2), while others are parallel automata (e.g. automata 6 and 8). We note in this architecture 13122 (3 × 6 × 3 × 3 × 3 × 3 × 3 × 3) possible states derived from parallel executions (graphs product) while there are many fewer active states at once. Indeed, this model is designed by the graphical formalism SyncChart [START_REF] André | Representation and analysis of reactive behaviors: A synchronous approach[END_REF]. A classical analysis is to transform this hierarchical structure to the synchronous language Esterel [START_REF] Berry | The esterel synchronous programming language: Design, semantics, implementation[END_REF]. Such transformation is not quite optimized. Furthermore, Esterel is not able to realize that there is only one active state at once. In practice, compiling such structure by Esterel generates 83 registers making roughly 9.6 ×10 24 states. Hence, the behoof of our process. Opting for a quasi-flattening, we have flattened only hierarchical automata. Thus, state 2 of automaton 1 is substituted by the set of states 4,5,6,7,8,9 of automaton 2 and so on. Required transitions are rewritten thereafter. Parallel automata are acting as observers that manage the model's control flags. Flattening parallel FSMs explodes usually in number of states. Thus there is no need to flatten them, as we can compile them separately, then concatenate them with the flat model retrieved at the end of the compilation process.

Algorithm 1 details our quasi-flattening operation. We denote downstream the initial state of a transition and upstream the final one. This algorithm implements three main operations. for (all sub-t of sub-FSM) do turn-down the sub-t priority (or turn up t priority) delete t add and rename all sub-t transitions from subFSM to SL add and rename all sub-St state from subFSM to SL cancel marked states Flattening the hierarchical model of Fig. 2 results in a flat structure shown in Fig. 3.1. As the activation of state 2 is a trigger for state 4, these two states will be merged, just as state 6 will be merged to state 10, etc. Automata 6 and 8 (observers) remain parallel in the expanded automaton; they are small and do not increase the computational complexity. The model in Fig. 3.1 contains now only 144 (16 × 3 × 3) state combinations. In practice, compiling this model according to our process generates merely 8 registers, equivalent to 256 states.

Our flattening differs substantially from those of [START_REF] Paiva | Modeling and testing hierarchical guis[END_REF] and [START_REF] Wasowski | Flattening statecharts without explosions[END_REF]. We assume that a transition, unlike the case of statecharts, cannot exit different hierarchical levels. Several operations are thus executed locally, not on the global system. This yields a simpler algorithm and faster compilation. To this end, we have integrated the following assumptions in our algorithm: -Normal termination. Fig. 5 shows an example of normal termination carried when a final internal state is reached. It allows a unique possible interpretation and facilitates code generation. -Strong preemption. Unlike classical preemption, internal outputs of the preempted state are lost during the transition.

Compilation process

We proceed in our approach to a symbolic compilation of the model into a Mealy machine, implicitly represented by a set of Boolean equations (circuit of logic gates and registers presenting the state of the system). Compiling an explicit automaton into an implicit one is a well-known process in hardware design. Classical works use the one-hot representation [START_REF] Chiuchisan | Finite state machine design and vhdl coding techniques[END_REF], while our compilation requires only log 2 (nbstates) registers. Actually, concurrent automata and flat automata are compiled separately. Compilation results of these automata are concatenated at the end of this process. They are represented by an union of sorted equations rather than a Cartesian product of graphs to support the synchronous parallel operation and instantaneous signals diffusion. Accordingly, we note a substantial reduction on the size of tested system. We explain in this section the process we follow to automatically generate symbolic sequences of test sets. As mentioned before, we seek to restrict the states space and confine only to significant states. The model of Fig. 6 presents all possible sequences of commands describing the system behavior. It is a classical representation of the dynamic system evolutions. It shows a very large tree or even infinite tree. Thus, exploring all possible program executions is not feasible. We will show in section 6 the weakness of this classical approach. If we consider the representation of the system by a sequence of commands executed iteratively, the previous sequences tree becomes a repetition of the same subspace pattern as shown in Fig. 7. We will focus in our approach only on this subspace. This represents a specific system command which can be repeated through possible generated sequences. Each state in the subspace is specified by the symbolic values of the program variables, the path condition and the command parameters (next byte-code to be executed). The path condition represents constraints that should be satisfied by the symbolic values to progress the execution of the current path. It defines the preconditions to successfully follow that path. Our work targets extracting these preconditions from the subspace check. Indeed, we have applied BDD-analysis from the local initial state to local final states of the specified subspace. For each combination of registers, BDD manipulations allow the extraction of the next awaited variables, that lead to the next state and required preconditions. Outputs are then pushed into a stack, in conjunction with resulting preconditions. Finally, sequence generation pops the constructed stack. Once the necessary preconditions are extracted, a next step is to backtrack the tree until finding the initial sequence fulfilling these preconditions. The backtrack operation is ensured by the compilation process which kept enough knowledge to find later the previous states.

SSG (Sequences Symbolic Generator)

Contrary to the classical sequence generator, our tool constantly generates a tree of pure future states, thus preventing loops from occurring. In other words, previous states always converge to the global initial state. This approach easily favors backtrack execution.

Let's consider the example of Fig. 7. Starting from the local initial donated state "LI", we generated all possible paths of tested subspace to reach the final local states using BDDs. Taking into account "LF" (local final state) as a critical final state of the tested system, we executed a backtrack from the "LI" state until covering the sequence that satisfies the extracted preconditions. Assuming state "I" as the final result of this backtrack, the sequence from "I" to "LF" is an example of a good test set. However, considering the representation of Fig. 6, a test set from "I" to "LF" will be performed by generating all paths of the tree. Such a test becomes unfeasible if the number of steps to reach "LF" is greatly increased.

AUTSEG Description

In this section, we present our testing tool called AUTSEG that implements the approach introduced in the previous section. AUTSEG is particularly used in this paper to test models of various smart cards. Generated automatic test Fig. 8. AUTSEG structure sets typically must differ according to system input parameters, for example the adopted smart card technology: contact versus contactless. Changing card parameters requires recompiling each new specification separately and re-running the tests. This approach is unrealistic, because this can take many hours or even days to compile. In addition, this would generate as many models as system types, which can highly limit the legibility and increase the risk of specification bugs. Hence, we have generated a single appropriate global model for all card types and applications, The model's explicit test sets are to be filtered thereafter by AUTSEG. To this end, AUTSEG will query via predefined signals a configuration file specific to each system application. As shown in Fig. 8, AUTSEG operation is carried by 5 main entities: (1) The generic model, (2) Quasi-flattening, (3) Compilation, (4) SSG and ( 5) The configuration file.

After quasi-flattening the hierarchical structure by the "autom-expand" [START_REF] Gaffé | Research web site[END_REF] tool implemented according to Algorithm 1, the expanded automaton is compiled separately and linked later with other compiled parallel automata, as shown in Fig. 9. Compilation process is carried out by the "autom2circuit" tool [START_REF] Gaffé | Research web site[END_REF], explained in section 3.2. The execution of "autom2circuit" generates a blif file [START_REF]Berkeley logic interchange format[END_REF] as shown in Fig. 9. A blif file is a compact format to express a netlist and is well-suited to represent Boolean equation systems. Using the "merge-blif" tool [START_REF] Gaffé | Research web site[END_REF], the generated blif files are concatenated at the end of the compilation process to produce the final global blif file (SSG input file).

In fact, AUTSEG defines two types of preconditions: (1) preconditions related to command parameters as described in section 3.3 and (2) preconditions defined by the configuration file. For a particular test generation, AUTSEG will extract the basic characteristics of the system from the configuration file unit. They are presented as Boolean variables, characterizing the preconditions of the system execution. If preconditions are not satisfied , the tested model will be refined, thus reducing the combinatorial explosion problem during sequence generation.

Use case

To illustrate our approach, we studied the case of a contactless smart card designed for the transportation sector. We aim to verify the correct and secure behavior of this card using AUTSEG.

Smart Card Model

The generic model of the studied smart card is designed from a given transport standard called Calypso. This standard defines 33 commands. The succession of these commands (e.g. Open Session, SV Debit, Get Data, Change Pin) presents possible scenarios of the card operation. All commands have been modeled with the Galaxy tool [START_REF] Gaffé | Research web site[END_REF]. Galaxy is an automata editor of finite state machines, able to generate four types of automata: simple (basic automata), parallel automata, hierarchical (light Esterel [START_REF] Ressouche | Modular compilation of a synchronous language[END_REF]) and syncChart. We chose to use light Esterel (a light version of SyncChart), a synchronous graphical model that integrates high-level concepts of synchronous languages in an expressive graphical formalism. The resulting model presents 52 interconnected automata including 765 states. Forty-three of them form a hierarchical structure. The remaining automata operate in parallel and act as observers for control data of the hierarchical automaton. Fig. 10 shows a small part of our model introducing the beginning of card scenarios. Applying "autom-expand" to the hierarchical automata shows in Fig. 11 a flattened structure running in parallel with the observers. Due to "autom-expand", we moved from 477 registers to only 22.

Configuration and Tests

According to the Calypso standard, several types and configurations of the card are defined (contact/contactless, maximum buffer size, etc.). We present these characteristics as preconditions of the system execution (AU T SEG Contact M ode, AU T SEG ch1 Selected, etc). The remaining preconditions are established during the execution of Calypso commands. They inform about system status, for instance, AU T SEG V Select F ile is true if the command "Select File" is executed normally, generating the output code SW9000.

Experimental Results

In this section, we show experimental results of applying AUTSEG to the contactless transportation card. We intend to test the security of all possible combinations of 33 commands of the Calypso standard. Each command in the Calypso standard is encoded on a minimum of 8 bytes. We conducted our experiments on a PC with Intel Dual Core Processor, 2 GHz and 8 GB RAM. A classical test of this card can be achieved by browsing all possible paths of the model as represented in Fig. 6. A second test applies AUTSEG on the card model represented in the same manner as Fig. 7. Results show that our approach enables coverage of the global model in a substantially short time. It allows separately testing 33 commands (all the system commands) in only 10 steps, generating a total of 1784 paths. These results are highlighted in Fig. 12 by a comparison of our approach to the classical generation method. We note from the AUTSEG curve a lower evolution that stabilizes at 10 steps and 1784 paths, allowing for coverage of all states of the tested model. Covering all states in only 10 steps, our results demonstrate that we test seperately one command (8 bytes) at once in our approach. Few additional bytes (2 bytes in our case) are required to test system preconditions.

We show below an excerpt of generated sequences presenting the two last paths. We observe the extraction of necessary preconditions that should be satisfied for each sequence. AU T SEG Contact M ode and AU T SEG ch1 Selected are preconditions from the configuration file. They serve to specify the execution context and thus possible resulting sequences. The remaining preconditions (AU T SEG V Select F ile, AU T SEG V erif Always DF , etc) will be used to play iteratively the backtrack (e.g, check Setlect File command) until the source sequence is found. We notice the END of sequence generations by 1784 paths, thus covering the entire system execution.

AUTSEG TEST SET -----------------------------------------------PATH: 1 . . .

-----------------------------------------------PATH: 1783 PRECONDITIONS: AUTSEG_Contact_Mode AUTSEG_CH1_Selected AUTSEG_Verif_Always_DF and AUTSEG_V_Select_File not AUTSEG_Too_many_modifications_In_session SEQUENCE: -h00 -h04 -h00 ---> SW9000 Next_command - ----------------------------------------------PATH: 1784 PRECONDITIONS: AUTSEG_CH1_Selected AUTSEG_Verif_Always_DF and AUTSEG_V_Select_File AUTSEG_Too_many_modifications_In_session SEQUENCE: -h00 -h04 -h00 ---> SW6400 Next_command -----------------------------------------------EXPLORATION END FINDING 1784 PATHS...

Conclusion

We have proposed AUTSEG, an Automatic Test Set Generator for embedded reactive systems. We particularly focused in this paper on systems executing iterative commands. Our tool is able to handle large models, where the risk of combinatorial explosion of states space is important. This has been achieved by essentially [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF] providing an algorithm to quasi-flatten hierarchical FSM and reduce the states space, and (2) focusing on pertinent subspaces and restricting the tests. This enables coverage of the global system behavior and generates the list of all possible system evolutions according to the configuration file. Since our tool ensures communication with an interactive specification block, this approach can be adapted to process in parallel several types of system specifications.

In the near future, we will integrate data evaluation during the test process. We aim to use the Linear Decision Diagram LDD [START_REF] Chaki | Decision diagrams for linear arithmetic[END_REF] to accomplish this. LDD allows the characterization and expression of the given preconditions by numerical constraints. It checks several constraints and concludes about the feasibility of the corresponding sequence. For example, if the union of constraints is unsuccessful by LDD, then we can confirm that tested sequence is impossible and remove it. With this approach, we can reduce the states space and avoid large calculations.

Fig. 1 .

 1 Fig. 1. Global process structure

Fig. 2 .

 2 Fig. 2. Model Design

  Overall, It replaces each macro state with a corresponding FSM. It first interconnects the internal initial states. It then re-Algorithm 1 Flattening operation St ← State; SL ← State List of FSM; t ← transition in FSM while SL = empty do Consider each St from SL if (St is associated to a sub-FSM) then mark the deletion of St load all sub-St from sub-FSM (particularly init-sub-St) for (all t of FSM) do if (upstream(t) == St) then upstream(t) ← init-sub-St // illustration in Fig.3 (t0, t1, t2 relinking) for (all t of FSM) do if (downstream(t) == St) then if (t is a normal-term transition) then // illustration in Fig.5 for (all sub-St of sub-FSM) do if (sub-St is associated to a sub-sub-FSM) then create t (sub-St, upstream(t)) // Keep recursion if (sub-St is final) then for (all t of sub-FSM) do if (upstream(t ) == sub-St) then upstream(t ) ← upstream(t) merge effect(t) to effect(t ) mark the deletion of sub-St else // normal transition: illustration in Fig.3 // For example t3 is less prior than t6 and replaced by t6.t3 and t6 for (all sub-St of sub-FSM) do create t (sub-St,upstream(t),trigger(t),effect(t))

Fig. 3 .

 3 Fig. 3. Initial and Normal Transition Linking

Fig. 4 .

 4 Fig. 4. Flat Model

Fig. 5 .

 5 Fig. 5. Terminal Transition Linking

Fig. 6 .

 6 Fig. 6. Classical Sequences Generation

Fig. 7 .

 7 Fig. 7. Model Representation

Fig. 9 .

 9 Fig. 9. Model Tool chain

Fig. 10 .

 10 Fig. 10. Calypso smart card model

Fig. 11 .

 11 Fig. 11. Calypso Flat Model

Fig. 12 .

 12 Fig. 12. Combinatorial explosion of classical tests

Refers to SyncCharts "normal termination" transition[START_REF] André | Representation and analysis of reactive behaviors: A synchronous approach[END_REF]


J S Gomez

A Vergne

P Martins

L Decreusefond

Wei Chen

Influence of Network Deployment on Resource Block Allocation

Keywords: Ginibre Point Process, Poisson Point Process, Network dimensioning

In this paper, the influence of network deployment on downlink dimensioning under an interference limited regime is studied. Theoretical and numerical results are derived for a network deployed as a Poisson point process. We show that slightly degraded propagation conditions has a beneficial effect on network dimensioning and performance. Spatial influence is also studied thanks to the β-Ginibre model. Simulations show that a regularly deployed network improves dramatically spectrum usage and network performances.

I. INTRODUCTION

S MARTPHONES and their ecosystem pushed user experi- ence towards throughput intensive services. In this context, fourth generation wireless networks and 802.16e standard introduced OFDM on the radio link. The band is divided into orthogonal sub-carriers, which minimizes spectrum occupancy and fulfills capacity demand. In order to further increase spectrum capacity and mitigate interference, LTE and WiMax have introduced dynamic frequency and time access (OFDMA). Sub-carriers are aggregated in Resource Blocks (RB) of 1ms length and 180kHz wide. A typical LTE eNodeB can manage up to 100 RB per 10ms, for a total band of 20MHz. One can increase the number of RBs per eNodeB, however, provided some user demand and some loss requirement, is there a limit in the number of RBs one can allow? Inter-site interference also plays a great role since the number of resources block allocated to one user depends on the quality of the channel, which is strongly linked to the statistical properties of the eNodeB deployment.

Statistical properties of wireless networks have been widely explored in literature. Pioneer works of Baccelli [START_REF] Baccelli | Stochastic Geometry and Wireless Networks, Volume I -Theory[END_REF] have provided a strong baseline for analyzing properties of networks deployed as a Poisson point process. However, such Poisson based models does not fit ideally real deployments, since there exists a strong probabilistic dependency between base station locations. Other point processes have been considered. Among J.S. Gomez is with the Institut Mines-Télécom, Télécom ParisTech, CNRS, LTCI (Paris, France) and the Departement of Electronic Engineering of Tsinghua University (Beijing, China), e-mail: jean-sebastien.gomez@telecomparistech.fr A. Vergne, P. Martins and L. Decreusefond are with the Institut Mines-Télécom, Télécom ParisTech, CNRS, LTCI (Paris, France), e-mails: {anais.vergne, philippe.martins, laurent.decreusefond}@telecom-paristech.fr Wei Chen is with the Department of Electronic Engineering of Tsinghua University (Beijing, China), e-mail: wchen@tsinghua.edu.cn them, the β-Ginibre point process, which properties has been studied in [START_REF] Deng | The ginibre point process as a model for wireless networks with repulsion[END_REF], successfully fitted the network deployment of four operators on Paris, France [START_REF] Gomez | A case study on regularity in cellular network deployment[END_REF]. The β parameter gives insights on the regularity of the deployment: if β is near zero, the point process is considered as uniform and is tending to a Poisson point process. If β is near one, there is a strong dependency between the placement of the base stations. The point process is considered as regular and its statistical properties are the ones of a Ginibre point process. For the Poisson point process and the β-Ginibre point process, the SINR distribution has been studied respectively in [START_REF] Błaszczyszyn | Using poisson processes to model lattice cellular networks[END_REF] and [START_REF] Nakata | Spatial stochastic models for analysis of heterogeneous cellular networks with repulsively deployed base stations[END_REF]. This means that one can induce the quality of the radio signal on a network level, providing the type of point process used.

The objective of this paper is to study the influence of the network deployment on the dimensioning of the base stations. Especially, general downlink performances of a cell placed in the middle of a network deployed as a Poisson or β-Ginibre point process will be analyzed. Path-loss and fading are also considered in the channel model. As for frequency planning, the worst case scenario is considered since all base stations share the same band. The users are placed in the network following a Poisson point process. We evaluate the maximum number of RB that one base station can allocate, provided known user demand and outage probability. Since the exact maximum number of RB is computationally hard to obtain, we propose a pessimistic lower bound based on the concentration inequality, that fits both engineering requirements for computational complexity and robustness. We also evaluate the outage probability in function of the path-loss exponent, provided a fixed number of RB and user demand. Thanks to the results of Błaszczyszyn et al. [START_REF] Błaszczyszyn | Using poisson processes to model lattice cellular networks[END_REF] it is possible to provide an theoretical analysis for Poisson deployed networks. Simulation analysis will also explore the differences of performances induced by the type of deployment, as we consider several β-Ginibre deployed networks.

Resource allocation algorithms for OFDMA systems have been studied extensively. In [START_REF] Lin | A tutorial on cross-layer optimization in wireless networks[END_REF], many optimization based algorithm are proposed for allocating and scheduling resources. Other works have included Markov chains [START_REF] Combes | Self-organizing relays: Dimensioning, self-optimization, and learning[END_REF], queuing theory or game theory to conceive original algorithms. In [START_REF] Anchora | A framework for scheduling and resource allocation in lte downlink using Nash bargaining theory[END_REF], the optimal resource allocation strategy is modeled as a Nash bargaining equilibrium. However, dimensioning and planning issues have been more recently investigated. In this paper, we adopt the same theoretical foundations as in [START_REF] Decreusefond | Robust methods for lte and wimax dimensioning[END_REF]. However, its results are only valid in noise limited systems, since only one base station is considered. This paper extends and completes its results on a network level. It also gives insights on the link between network performances and deployment.

This paper is organized as follows. In the first section, the system model and theoretical hypothesis are given. A theoretical analysis is provided for Poissonnian deployed networks in Section II. In Section III, simulation analysis and performance analysis are provided for Poisson deployed and β-Ginibre deployed networks. In Section IV, conclusions are drawn.

II. SYSTEM MODEL

A. Channel model

The system is composed of a network of identical omnidirectional OFDMA base stations. They are deployed in the plane according to a certain point process of a given intensity λ n . The state of the network is considered at a given time slot. For each given time slot, active users are localized in the plane according to a Poisson point process with intensity λ u . Each user asks for the same capacity C and each base station shares the same spectrum and without any cooperation scheme. Furthermore, each base station can allocate up to N avail RBs per time slot. A user belongs to the base station under the condition that it provides him with the best SIR. Channel model includes path-loss and fading. Therefore, the power received by a mobile from a base station i is modeled by:

P (d ij ) = P i G ij d -γ ij
, where P i is the transmission power of the base station, d ij the distance between the base station i and the mobile j and γ is the path-loss exponent. The channel fading G ij is a random value following a exponential law of parameter one. Furthermore, the number of resource blocks allocated to each user, given by the following equation:

N j = min C W rb log 2 (1 + max i (SIR i,j ) , l m .
W rb denotes the bandwidth of one resource block and x is the ceil value of x. l m is the maximum number of RBs that can be allocated to one user. The SIR between the ith base station and the jth user is given by:

SIR i,j = P (d ij ) k =i P (d kj )
.

The total number of RBs that are demanded in one cell is the random integer given by:

N tot = j N j
Quality of the network deployment is assessed thanks to the loss probability: P(N tot > N avail ) .

Three case scenarios are investigated:

• considering a given loss-probability, the influence of γ on E [N tot ] is studied, • considering a given N avail , the influence of γ on the lossprobability is studied, • considering a given loss-probability, an approximation of N avail thanks to the concentration inequality.

B. Influence of γ on dimensioning.

Theorem 1. In Poisson point process deployed network and for a provided loss probability , E [N tot ] decreases as γ increases.

Proof. For a given poissonian deployed network, the SIR at each point of the network is assumed to be independent to one another. This assumptions is reasonable since the homogeneous PPP is a stationary process. We model the users location and traffic demand by a marked PPP on E = [|1, . . . , l m |]×C:

λ u dν(z) = λ u (α(l) ⊗ dz)
α(l) = α l corresponds to the probability that a user demands l RBs and each α l defined as follows:

α l =      P(t 1 < SIR) if l = 1, P(t lm ≤ SIR) if l = l m , P(t l ≤ SIR < t l-1 ) otherwise, where t l = 2 C/lW rb -1.
The family (α 1 , . . . , α lm ) corresponds to the mean proportion of the plane where one can allocate receptively 1, . . . , l m RBs to a user. Hence, for each cell in the network, the number of RBs demanded by the users N tot follows a compound Poisson distribution:

N tot = lm l=1 lM l .
Each M l is an independent Poisson of parameter m l = λ u α l . The mean total number E [N tot ] of RBs allocated in the cell C, for users distributed according to a PPP is the sum:

E [N tot ] = lm l=1 x∈C l α l λ u dx
According to Błaszczyszyn et al. [START_REF] Błaszczyszyn | Using poisson processes to model lattice cellular networks[END_REF], for all t ≥ 1 and γ > 2 the SIR coverage probability for a poissonian network is expressed as:

P(SIR ≥ t) = γ sin (2π/γ) 2π t -2/γ
Therefore, it is proven in Appendix citer that the coefficient α l becomes dominant for small values of l as γ increases. E [N tot ] thus decreases with γ.

C. Influence of γ on loss probability.

Theorem 2. In Poisson point process deployed network, for a fixed threshold N avail , the loss probability decreases as γ increases.

Proof. As in [START_REF] Decreusefond | Robust methods for lte and wimax dimensioning[END_REF], the distribution of lM l s constructed by the rule:

p l (ω) = 0 if ω mod l = 0, exp (-m l ) m q l /q! if ∃ q ∈ N, ω = ql.
As the random variable N tot is a linear combination of independent random variable, its density can be recovered by convolution of the densities of lM l . Since α l for small values of l becomes more dominant, the probability of small values occurring increases.

In interference limited networks, the path-loss γ has a beneficial impact on the overall quality of the signal since it limits mutual cell interference.

D. Approximation of N avail .

Since the probability density of N tot is known, numerical simulations are conducted to find N avail such that:

P (N tot ≥ N avail ) ≤ ,
being the desired loss threshold. For engineering purposes, a lower robust bound is provided thanks to the concentration inequality.

Theorem 3. The lower bound is given by:

P(N tot ≥ E[N tot ] + a) ≤ exp - E N 2 tot l m g a l m E[N 2 tot ]
,

where g(θ) = (1+θ) ln (1 + θ)-θ and the moments are given for any p natural integer:

E [N p tot ] = lm l=1 x∈C l p α l λ u dx.
Proof. Since the number of RBs l is a positive integer with maximum l m , Theorem 4 of [START_REF] Decreusefond | Robust methods for lte and wimax dimensioning[END_REF] is applied to derive the expression.

The lower bound of N avail is then given by:

N avail = E[N tot ] + a,
where a is the solution of:

g a l m E[N 2 tot ] = - ln( ) l m E[N 2 tot ]
.

III. SIMULATIONS

In this section, the previous theoretical analysis are confirmed by numerical simulations. We also explore the influence of the regularity of the deployment on resource block allocation and loss probability in the network. Simulation parameters are summarized in Table I. The values λ n and λ u are chosen to match a busy urban environment. Users are assumed to be identical and ask for a download throughput of 1 Mb/s.

Figure 1 illustrates Theorem 1, where the mean number of RB needed decreases dramatically from 170 to 120 with γ. Such results are coherent with the fact that this study focuses on interference limited systems. Since radio propagation conditions becomes harsher with a high value of γ, interfering signals are therefore less strong compared to the main signal, granting more surface of the cell a higher SNR. Likewise, Figure 3 shows that for a fixed number of RBs per cell, the loss probability decreases with γ, as stated in Theorem 2. Figure 2 shows that the approximation given by the inequality concentration stated in Theorem 3 is as expected pessimistic and over estimate the exact result by 10%. The authors in [START_REF] Gomez | A case study on regularity in cellular network deployment[END_REF] have shown that the β-Ginibre Point Process (β-GPP) provides a robust model for fitting real deployment. The PPP indeed fails to catch the underlying repulsiveness that exists between base station sites, since location of the points are considered to Fig. 3: Loss-probability for N tot = 100 in function of γ be independent with one another. Therefore, cluster of points might occur. A network deployed such as a PPP is qualified as uniform. On the contrary, a network where clusters occur with infinitesimal probability is qualified as regular. The β-GPP stands in between, thanks to β. When β goes to zero, the β-GPP converges to a PPP in law. However, the 1-GPP is the Ginibre Point Process. For each figure, the worst case scenario is held by the PPP whereas the best case scenario is given by the 1-GPP. The SIR is indeed improved in the network with β going to one as shown in [START_REF] Nakata | Spatial stochastic models for analysis of heterogeneous cellular networks with repulsively deployed base stations[END_REF]. Figure 1 and Figure 2 show that the improvement between PPP and 1-GPP varies between 12% and 26% depending on the value of γ. Likewise, the lossprobability is improved up to a factor of four between the PPP and 1-GPP.

IV. CONCLUSION

In this paper, the impact of the path-loss exponent on network dimensioning has been studied. Theoretical and numerical analysis demonstrated that in a PPP deployed network, a higher path-loss exponent has a beneficial effect on network performances under interference limited regime. Numerical analysis performed with β-GPP deployed networks has shown that spatial regularity has a dramatic effect on increasing network performances. Future works will aim at understanding the role of the noise in dimensioning cellular networks.

APPENDIX A

Influence of γ on the coefficients α l .

According to the definition of the family (α 1 , . . . , α lm ) , α 1 and α lm are strictly monotonously increasing and decreasing respectively for γ ≥ 2. In order to prove that the coefficients α l for small l become preponderant in the weight sums, one must consider the pairwise difference:

d l (γ) = α l+1 -α l , = γ sin(2π/γ) 2π 2t -2/γ l -t -2/γ l-1 -t -2/γ l+1
.

A necessary and sufficient condition for the pairwise differences to be positive is

q l (γ) = t l-1 t l -2 γ + t l+1 t l -2 γ ≤ 2.
A study of the variations of q l (γ) establishes that this function satisfies to the condition if and only if:

t l+2 t l t 2 l+1 ≥ 1,
The variation study of this ratio proves that this condition is always verified. Therefore for γ large enough: 1) α 1 ≥ . . . ≥ α lm , 2) lim γ→∞ α 1 = 1, 3) lim γ→∞ α l = 0, with l = 1. This proves that the coefficients α l for small l become preponderant in the weight sums with γ increasing.

Fig. 1 :

 1 Fig. 1: E [N tot ] for a loss-probability of = 10 -2 in function of γ

Fig. 2 :

 2 Fig. 2: E [N tot ] for a loss-probability of = 10 -2 in function of γ

TABLE I :

 I Simulation parameters

	λn	3.0 per km square
	λu	400 per unit square
	lm	10
	C	1 Mb/s
	W RB	180 kHz
	Path-loss exponent	from 2 to 5
	Network radius	1,8 km