Hidenori Chida
email: hidenori.chida@gmail.com

Catya A Zuñiga
email: catya.zuniga@recherche.enac.fr

Daniel Delahaye
email: delahaye@recherche.enac.fr

Topology design for Integrating and Sequencing Flows in Terminal Maneuvering Area

The current overloaded airspace near large airports leads the stakeholders to develop more fundamental means to improve the use of available air capacity in dense traffic areas as Terminal Maneuvering Area (TMA). A smart planning of aircraft trajectories and an appropriate designing of route structure can be a solution. Therefore, to analyse the capability of them, this paper proposes a novel approach to deal with the merging and sequencing problem of arrival traffic in Terminal Maneuvering Area, and examines the performance of diverse conflict resolution strategies and different TMA route structure.

A evolutionary algorithm is employed to resolve potential conflicts, altering one or more of the following decision variables; routes, speeds, and entrance time to Terminal Maneuvering Area (slot). Two different fitness functions were developed. One aims to minimize potential conflicts and the other aims to minimize at the same time potential conflicts and delay induced at runway. The performance of different combinations of decision variables, or conflict resolution strategies, is evaluated through a set of arrival aircraft to Grand Canaria airport. Also, four different route structures are tested by using the same set of incoming aircraft. The results showed that the slot and speed change and mix of all change stratagies can successfully resolve all conflicts in an efficient manner. The results also suggested that topologies with one main merging point are more efficient than the ones that have two merging points. Finally, a significant abatement of delay was observed when minimizing conflicts and delay while achieving conflict free solutions.

I. INTRODUCTION

To ensure the safety and fluidity of Air Transport over the twenty years, it has been necessary to revisit some key aspects through diverse modernization projects such as The Single European Sky ATM Research (SESAR) launched by the European Community and the Next Generation Air Transportation System (NextGen) launched by the US government, among others. One of the bases of these projects is to exploit technological advances in diverse fields as Communication, Navigation and Surveillance, among others, to improve the overall Air Traffic Management System.

There are a variety of airspace concepts under development to satisfy their strategic objectives such as improving safety and capacity by reducing congestion and environmental impact while increasing operational and flight efficiency. According to [START_REF]Airspace concept handbook for the implementation of performance based navigation (pbn)[END_REF], some of the innovative Airspace Concepts to enhance capacity include a practical and efficient. organization of the airspace and its operations. Practical organization of the airspace includes among others revisiting the ATS route structure, separation minima, route spacing and obstacle clearance.

The concept of an advance Terminal Airspace Area and its operations has been introduced as part of both modernization projects due to the complex operations that are handle in it and which are facing an increasing Air Traffic demand. Every day operations are subjected to delays, frequent large turns, incompletely specified flight plans, incomplete or undefined Arrival and Departure routes, or lack of navigation systems for guidance, among others factors whose affect the performance of the overall system.

A prevalent initiative is to implement Area Navigation (RNAV) procedures as RNP Standard Terminal Arrival (STAR) and Standard Instrument Departure (SID) in the Terminal Airspace to organize incoming and outcoming flows in a more efficient manner. Procedures such as the RNAV allows to fly on any desired path without the need to fly directly toward or away from a ground-based navigation aid (NAVAID). In this case, the position of an aircraft is defined by a mix of instruments contained in the aircraft such as an inertial reference system, and the global positioning satellite system (GPS). Nowadays, more and more RNAV procedures have been implemented in both, Terminal Area (or Terminal Manoeuvre Area, TMA) and En-Route navigation. Advanced RNAV include the ability to access navigation database (that can be loaded into an aircraft Flight Management System (FMS)) to fly a path using the flight director or autopilot.

There are several potential benefits with the introduction of RNAV arrival and departure procedures, [START_REF] Szurgyi | Analysis of observed aircraft-to-aircraft separations[END_REF] including:

1) Reduce the need to vector aircraft 2) Fewer radio transmissions due to less need for controller instructions 3) Improve situational awareness 4) Reduce flying time and distance, i.e. more direct routing 5) Reduce time and fuel consumption 6) Increased airspace/runway capacity through the use of defined paths 7) Increased flight path predictability and repeatability 8) Facilitate closely-spaced parallel arrivals and departures A key to obtain these advantages (particularly in Terminal Airspace) is the need to design efficient arrival and departure routes as a function of the interaction between them while ensuring obstacle clearance. It has also been stated that route topologies in the Extended Terminal Airspace play an important role in scheduling performance and that an efficient scheduling and route assignment affects important performance metrics such as runway delays, throughput, fuel efficiency, and robustness to uncertainties in operations [START_REF] Ivanescu | Models of air traffic merging techniques: Evaluating performance of point merge[END_REF], [START_REF] Favennec | Point merge integration of arrival flows enabling extensive rnav application and cda -operational services and environment definition[END_REF].

In the capacity and airspace usage planning concept, the demand for efficient traffic flows plays an essential role in addressing the efficient organization of airspace volumes, which could increase the airspace capacity if properly addressed. At the same time, the airspace control management must use these forecast and analyze the strategies to minimize the risk of potential conflicts while maximizing users' initial business interests choices as often as possible (under SESAR concepts). Therefore, the future system is migrating to more predictable arrival flows where aircraft land at a specified time. This will enable air traffic control system to issue more efficiently TMA flows by providing shorter and more safety flights using more efficient airspace which will increase airspace capacity [START_REF] Hull | Technology-enabled airborne spacing and merging[END_REF].

The purpose of this work is to compare diverse STAR procedures to provide efficient means to merge multiple inbound streams of aircraft and deliver them safety spaced to the runway control. It should be notice that the random arrivals must be converted into an orderly stream while merging aircraft flows coming from different entry points, commonly done in a short time horizon (about 45-60 minutes). Resolution strategies have been designed to provide shorter route length and/or time to avoid conflict and to support Continuous Descent Operations. Parallel routes have been designed to avoid having bidirectional traffic on the same route providing various route options between the destination airport.

The algorithm has been successfully applied to Gran Canaria airport (Spain) with real traffic demand samples for which conflict free flow merging is produced smoothly with optimal runway feeding. The algorithm generates new speed and routes profiles aim to remove conflicts at merging points while maintain the minimum separation between aircraft following the same route according to their wake turbulence constraint.

The reminder of this works is as follows; Section II contains some of the most important related works in the field of Airspace Design, Sequencing and Merging flow of aircraft within TMA and the Conflict Detection and Resolution problem. Section III explains in detail the strategy to formulate the problem, the topologies to be analyzed and the mathematical model. A summary of the Evolutionary Algorithms (EAs) techniques are introduced in Section IV followed by the description of the model in Section V presented in Subsection III-D is described in detail. The results obtained from a sample simulation study are presented in Section IV. Finally, conclusions and future works are discussed at the end of the paper.

II. PREVIOUS RELATED WORKS

An aircraft approaching to TMA typically follows a STAR providing the transition from the En-Route structure to Terminal Airspace. These, landing aircraft are organized in arrival streams, i.e. the individual paths of each aircraft are gradually merged till reaching the active landing runway. It should be noticed that all aircraft are required to maintain a safe separation distance, or separation standards which are a function of the landing velocities of the leading and following aircraft as well as the size of the aircraft involved at the final approach, among other factors [START_REF] Dear | The dynamic scheduling of aircraft in the near terminal area[END_REF].

Before the approach takes place, each aircraft must be assigned with a landing time and a runway number. The landing time corresponds to a time window, bounded by an earliest and a latest time of arrival. Ideally, this landing time should be the same than the one in the flight plan. Unfortunately, the system is subjected to many types of perturbations in every day operations. To avoid potential conflicts at TMA, Air Traffic Control issues a set of vectoring instructions to pilot to overcome merging and sequencing of arrival flows. Delay in the landing times are induced if an aircraft is required to either slow down, hold, or change route to avoid potential conflicts. The delay is the difference between the schedule landing time and the assigned landing time and it has a cost associated to it. The cost is not only associated to fuel burn or CO 2 emission, but also to the overall efficiency of the ATS causing up stream disruptions on airport operations capacity.

To properly address TMA landing operations and procedures, a search in the literature was conducted to identify the main related concepts such as the Merging and Spacing Problem and the Airspace Design and Planning process.

The aim of the Aircraft Sequencing Problem (ASP) is to optimize the assignment of aircraft to runways while optimizing the sequence of aircraft departures and arrivals on each runway. There have been different approaches since the 70s as in [START_REF] Dear | The dynamic scheduling of aircraft in the near terminal area[END_REF] where it was first observed that the firstcome, first-serve policy was inefficient for the medium and long term of the ASP. As a consequence of their analysis, a decision methodology termed Constrained Position Shifting (CPS) was proposed to eliminate the undesirable behavior. Based on the Constrained Position Shifting method, diverse approaches have been developed to solve the ASP.

Balakrishnan et al. [START_REF] Balakrishnan | Scheduling aircraft landings under constrained position shifting[END_REF] presented an study to determine the sequence that minimizes makespam for the static case of the ASP subject to diverse operational constraints. In further researches of the authors [START_REF] Balakrishnan | Algorithms for scheduling runway operations under constrained position shifting[END_REF] and [START_REF] Chandran | A dynamic programming algorithm for robust runway scheduling[END_REF], an extension their work considers as a core problem maximizing runway throughput (equivalent to minimizing the makespam or the landing time of the last of a given set of aircraft) for arrivals operations, departures operations and mixed operations (simultaneous arrival and departure scheduling on a single runway). It is claimed that the output of the algorithm is not a single schedule, but a tradeoff between the likelihood of controller intervention and the time to complete runway operations for the given set of aircraft (makespam of the sequence).

In [START_REF] Beasley | Scheduling aircraft landings -the static case[END_REF], the authors uses a mixed-integer zero-one formulation of the ASP together with a population heuristic algorithm. Some years later, Beasley et al. developed several studies that apply population based meta-heuristics for the formulation of the ALP using real data to validate their results, [START_REF] Beasley | Scheduling aircraft landings at london heathrow using a population heuristic[END_REF], [START_REF] Beasley | Displacement problem and dynamically scheduling aircraft landings[END_REF]. They state that their work could improved Air Traffic Control decisions between 2% and 5% in terms of reducing the timespan required to land.

Dear et al. [START_REF] Dear | The dynamic scheduling of aircraft in high density terminal areas[END_REF], [START_REF] Dear | An algorithm for computer assisted sequencing and scheduling of terminal area operations[END_REF] presented a CPS heuristic for the static and dynamic case of the Aircraft Landing Problem which aims to decide a landing time for each aircraft such that each one lands within a predetermined time window and that separation standards are respected. Other approaches solve the ASP by meta heuristics as the branch and bound algorithm as in the work of Psaraftis [START_REF] Psaraftis | A dynamic programming approach for sequencing groups of identical jobs[END_REF], where a dynamic programming approach of a single machine scheduling problem was developed and applied in the context of sequencing aircraft arrival operations.

A broader suite of concepts have been investigated to address merging and spacing problems arising from structured RNAV and Required Navigation Performance (RNP) routes in the Terminal environment referred as Spacing of Performance-based Arrivals on Converging Routes (SPACR) [START_REF] Becker | Methods for maintaining benefits for merging aircraft on terminal rnav routes[END_REF]. Their work addressed the near-term merging and spacing problem.

The method called "Point Merge technique" [START_REF] Boursier | Integrating aircraft flows in the terminal area with no radar vectoring[END_REF], [START_REF] Boursier | Merging arrival flows without heading instructions[END_REF], [START_REF] Hofhan | Analysis of spacing guidance for sequencing aircraft on merging trajectorie[END_REF], [START_REF] Favennec | Point merge integration of arrival flows enabling extensive rnav application and cda -operational services and environment definition[END_REF], aims to merge arrival flows of aircraft without using heading instructions. It's principle is to achieve the aircraft sequence on a point with conventional direct-to instructions, using predefined legs at iso-distance to this point for path shortening or stretching.

In another approach [START_REF] Zuniga | A cd&cr causal model based on path shortening/path stretching techniques[END_REF], it has been described a Discrete Event model based on Coloured Petri-Nets formalism, useful to specify an algorithm focusing on the arrival phase of flight. The causal model developed considers different alternative pre-defined turning points for each flight by evaluating path shortening/path stretching of all trajectories upwards the assigned merging points in a TMA.

III. PROBLEM MODELLING

The work consists of testing different conflict resolution strategies and diverse TMA route structure. The following sections describe in detail the modelling approach followed by the authors.

A. Conflict Detection Strategy

The Conflict Detection (CD) phase consists of predicting potential conflicts among the set of arrivals. A conflict is detected when the separation between two aircraft is smaller than a minimum separation criteria. The separation criteria depends on many factors, such as the aerodynamic requirement, the class of the two aircraft (the leading and the following) and the density of air traffic and the airspace. As different rules exist, the International separation standards which has been established by the International Civil Aviation Organization (ICAO) on the provisions of ICAO Doc 4444 (Procedures for Air Traffic Management) have been adopted. Table I summarizes the nominal horizontal separation minima based on a wake turbulence category of each aircraft.

The order of the leading and the following aircraft is determined based on arrival times at a merging node. Figure 1 illustrates this process. First, an aircraft combination is selected and a merging node is detected which is the node ahead of the aircraft concerned and shared by the two trajectories where the aircraft will fly. Next, the estimated arrival time of each aircraft is calculated with the residual distance to the merging node and its velocity. Then, based on these estimated arrival times, the leading and the following aircraft relationship is defined, yielding the corresponding separation minima (Table I). Finally, a conflict is detected when the actual separation between aircraft is smaller than the separation minima.

B. Conflict Resolution Strategies

According to [START_REF] Pallottino | Conflict resolution problems for air traffic management systems solved with mixed integer programming[END_REF], conflict resolution strategies are based either on the Heading Angle Change problem (HAC), the Velocity Change (VC) problem, or a mix of both cases. The HAC resolution approach is a method to avoid conflicts by changing the direction of the flight while the speed remains constant during the entire manoeuvre. In the VC resolution, aircraft is allowed to change the velocity of the flight but the heading angle remains fixed. The mix of both strategy combines HAC and VC, providing an aircraft an opportunity to alter both of the heading angle and the velocity.

In addition to the route and speed change strategies, slot allocation strategy is also used in practice by Air Traffic Controllers. This strategy is also known as "holding pattern" prior to entering TMA, which allows aircraft to shift the entry time to TMA in the sequence. The goal of the slot change is to induce a delay to an aircraft so that it can avoid conflicts by switch the order of entry to TMA with another aircraft.

The resolution approaches can also be classified as cooperative or, non-cooperative. In the cooperative approach, all aircraft are assumed to coordinate their actions while in the non-cooperative approach only one of the aircraft involved in the conflict is assumed to perform the resolution manoeuvre.

The first objective of this work is to compare diverse conflict resolution strategies to evaluate the performance of each one when dealing with a set of arrivals at TMA. Therefore, based on the existing strategies, we adopt HAC, VC, slot allocation changes and the mix of these strategies in a cooperative approach.

The HAC strategy is used as a strategic measure which determines alternative routes, or sub-routes used to avoid potential conflicts which will minimize the used of vectoring aircraft. Because this strategy is a selection of routes rather than a change of the heading angle, it is called route change strategy hereafter. The route structures, or the topology designs are briefly described in Section III-C and VI-B.

The VC strategy is translated into speed changes performed when entering TMA. Aircraft are assumed to fly Fig. 2. Gran Canaria STAR highest/lowest permissible speeds over each route (this value is normally considered around the ± 20% of its average Ground Speed). The modelling is based on the assumption of wind absence,i.e. the True Air Speed (TAS) can be considered as Ground Speed (GS). If speed resolution strategy is active, the speed is adjusted are performed at entry point and is assumed not to change the during the flight.

Some other assumptions and simplifications are made in the modelling and execution of the experiment. Aircraft trajectories were entirely deterministic. Uncertainties in the estimation of aircraft position or unexpected wind fields are not considered. Aircraft execute their planned trajectories without neither data-link transmissions, nor pilot-action delays. Conflicts among aircraft can be predicted with perfect accuracy over any time horizon. Arrival traffic management initiatives such as miles in trail restrictions, time-based metering, or ground-delay programs are not taken into account.

C. Proposed STARs

As for the route change strategy, different route structure designs have been analyzed to evaluate its operational performance according to some key performance indicators such as: speed profile, distance flown & delay at runway. Therefore, as depicted in Figure 3, four distinctive TMA configurations, or topologies are proposed in this work, which have been use to performed test in the second case study.

The STAR configuration of the Gran Canaria TMA, shown in Figure 2 has been used as the reference topology layout in this work. One can see that in the arrival phase, two routes fuse into one route towards the final approach (runway 03L/03R) with merging at a single waypoint. The two arrival routes correspond to STAR defined in the Spanish Aeronautical Information Publication (AIP) and are called TERTO3C and RUSIK3C, starting from the entry point TERTO (30 o 06'15"N,012 43'02"W) and RUSIK (28 o 54'22"N,012 48'59"W), respectively. In all proposed topologies, three entry points are defined; two of them correspond to the STAR on Figure 2 while the third route corresponds to an additional waypoint defined so as to smoothly merge the traffic flow coming. The new route has been named as NPWT3C and starts by the entry point NPWT (27 o 40'00"N,013 o 30'00"W) and ends at runway.

For the design of these routes, diverse Airspace Restrictions have been taken into account as to avoid Danger, Restricted and Prohibited Areas, or constraint regarding Flight level and lateral routes dimensions. The routes from different directions towards the final approach are designed to be safety separated laterally in accordance with ICAO recommendations.

The proposed topologies consist of a route network in which aircraft are allowed to fly in order to avoid potential conflicts. Each original route has a defined number of alternative routes, or sub-routes which depend on the original route structure. One route is comprised of diverse numbers of links which join an entry point to runway. A link is defined as a portion of a route which connects two waypoints or nodes. For example, in Topology A1 depicted in Figure 3, the original route TERTO3C is represented by a plain line that begins at entry point TERTO (or Node 1) and merges with the other routes at CANIS (or Node 4). This route is conformed by an ordered list of Links: 1, 2, 3, 4, 5, 6 and 7; which are connected by Nodes: 1, 7, 8, 9, 10, 4, 5 and 6. 5 sub-routes are attached to this original route as illustrated by dashed lines. For instance, one of these sub-routes is consisted of Link 8, 13, 14, 15, 16, 17, 18, 6 and 7. This topology design has one main merging point (Node 4), 3 original routes with 5, 8 and 4 sub-routes, making a total of 16 sub-routes.

Four topologies have distinctive features in their subroute structures and the number of merging points. For example, while topologies having letter "A" have sub-route structure like fish bones which allow aircraft to deviate from the original path, those with "B" are provided with trapezoid shaped sub-route structures. The topologies with the number "1" have only one merging point, whereas those with the number "2" have two merging points.

D. Mathematical Modelling

Consider a set of flights F = {1, ..., F } planned to land in a given time horizon, [0, T ]. This time horizon is discretized by a time increment ∆t, yielding a set of

T = {s * ∆t | s ∈ Z, 0 ≤ s ≤ T /∆t}.
Let R k be the set of routes which start at entry point

(or node) k (k = 1, 2, 3). Thus, R k = {r ik | i ∈ N, 1 ≤ i ≤ R k },
where r ik is the one route starting point k and R k is the number of routes (main route and its attached sub-routes) associated with an entry point k .

Each flight f in F has the following predetermined information:

• e f : TMA entry point of flight f . e f ∈ {1, 2, 3}. • wt f : Wake turbulence category of flight f (heavy, medium, light). Let d f f (t) be a distance between the leading f and the following f aircraft at time t ∈ T . A conflict is detected in the following case:

d f f (t) ≤ s f f ∀f, f ∈ F , ∀t ∈ T ,
where s f f is the separation minima which depends on the aircraft's wake turbulence category of each aircraft, wt f and wt f .

The accumulative number of conflicts n f associated with the following aircraft f throughout the time horizon is:

n f = T t=0 F f =1 c f f (t), c f f (t) = 1 if d f f (t) ≤ s f f , 0 otherwise.
where c f f identifies a conflict in aircraft f at instant t.

As introduced in Section III-B, the conflict resolution strategies involves the following decision variables: route, speed and slot regulation. These decision variables are subject to the following constraints:

• Route change Route selection can be performed, as introduced in Section III-C, among all possible routes starting from the corresponding entry point e f . Thus,

r f ∈ R e f , ∀f ∈ F .
where r f is the route decision variable of flight f after the conflict resolution strategy is applied.

• Speed change As stipulated in Section III-B, speed can be changed within a maximum and a minimum value, being discretized in ∆v increments. Thus, The selected parameters for the experiment are: ∆v = 2 kt, v min = 250 kt, and v max = 310 kt.

v f ∈ V , ∀f ∈ F , where V = {v min + s * ∆v | s ∈ Z, 0 ≤ s ≤ (v max -v min )/

• Slot change

The arrival time at TMA entrance can be altered within a discretized set of allowable slot values,

t f ∈ T , ∀f ∈ F , where T = {t sch f + s * ∆t s | s ∈ Z, 0 ≤ s ≤ ∆t smax /∆t s },
∆t smax is the longest permissible holding time at TMA entry point, ∆t s is the time increment, and t f is the slot decision of flight f after the conflict resolution strategy is applied. Here, the selected parameters for the experiment are: ∆t s = 30 seconds, and ∆t smax = 300.

Having discrete and continuous decision variables such problem belongs to the class of mix optimization problems.

Let X be the state space of this problem. X can be described as a set of all decisions of all flights, thus,

X = {(d 1 , ..., d F )| d f ∈ D f for all 1 ≤ f ≤ F }, where D f = {(r f , v f , t f )| r f ∈ R e f , v f ∈ V , t f ∈ T }, and d f = {r f , v f , t f } is a decision of flight f .
The state space dimension can be calculated by the following formula:

|X | = F f =1 |D f |, = F f =1 R e f (n vmax + 1)(n smax + 1),
where n vmax and n smax are the integer values satisfying n vmax = (v max -v min )/∆v and n smax = ∆t smax /∆t s respectively.

In the proposed topology, R 1 = 6, R 2 = 9, R 3 = 4. When it is assumed that the average number of routes per each entry point is 6 and that F = 50, |X | is approximately (6 * 31 * 11) 50 .

IV. EVOLUTIONARY ALGORITHMS

Evolutionary algorithms (EAs) is an abstraction of evolutionary biology which focuses in problem solving systems based on principles of evolution and hereditary to find approximate solutions to optimization problems [START_REF] Goldberg | Genetic Algorithms in Search, Optimization and Machine Learning[END_REF], [START_REF] Michalewicz | Genetic algorithms + Data Structures = Evolution Programs[END_REF], [START_REF] Koza | Genetic Programming[END_REF], [START_REF] Schwefel | Evolution and Optimum Seeking[END_REF].

The EAs maintain a population of individuals P OP (k) = (x 1 , ...x n ) for each iteration k. An individual represents a potential solution to the problem to be solved and is represented by a list of parameters, called chromosome or genome. In line with biological usage of the terms, it has become customary to distinguish the 'genotype' as the encoded representation of the variables, from the 'phenotype' the set of variables themselves.

To begin, several individuals are generated to form the first initial population which should be spread throughout the search space (see Figure 4). The major questions to consider are firstly the size of the population, and secondly the method by which the individuals are chosen. In respect of how the initial population is chosen, it is nearly always assumed that initialization should be 'random'; secondly, the choice of the population size must be always of a tradeoff between efficiency and effectiveness.

After the initial population is generated, it undergoes a evaluation and selection processes which identify the most adapted individual. Individuals are evaluated and assigned with a fitness score (returned by a fitness function). Based on this evaluation, individuals that have higher fitness (i.e. represent better solutions) can be identified, and these are given more opportunity to breed. The higher fitness score an individual has, higher the chances to reproduce. In addition, some individual of the new population undergo transformations by means of three main recombination operators to form new solutions: nothing, crossover, and mutation. The recombination of individual is carried out using simple analogies of genetic crossover and mutation.

Crossover allows solutions to exchange information (see Figure 6). One method (termed single point crossover) is to choose pairs of individuals promoted by the selection operator, randomly choose a single locus (point) within the chromosome and swap all the information to the right of this locus between the two individuals. Mutation is used to modify (flip) an individual to form another. The value of chromosomes within individual strings are then 'randomly' change. It is used very sparingly.

After recombination operators have been applied to the initial population, a new population will have been formed. This process of selection, crossover and mutation is continued until a fixed number of generations have elapsed or some form of convergence criterion has been met.

V. CODING THE EA MODEL

Decision variables are summarized in Fig. 5. The chromosome consists of the following 3 variables:

• Route decision (green elements) • Speed decision (red elements) • Slot decision (blue elements)

A. Initialization

To begin with the Evolutionary process, one must be able to initialize a population of chromosomes. There are several methods for the initialization. One way is to use a uniform random trial to initialize the population, while one of the other possibilities is to carryout a series of initializations for each individual and then pick the highest performing values. Alternatively, estimations can be made by other methods (e.g. heuristic process) in an attempt to locate approximate solutions, and the algorithm can be started from such points. The one which has been used in our experiments is a random generator for the initial population.

B. Fitness Computation

Fitness is an evaluation score of each individual obtained by the fitness function associated with the optimization criteria. In our approach, the fitness function is associated with a number of conflicts and formulated as follows. The value of the fitness function f i (x i ) is computed as:

f i = 1 0.01 + y i .
where y i is the conflict ratio for each individual x i ∈ P OP (k), an described as follows:

y i = N con N 0 con ,
where, N con is a summation of conflicts of all f in the individual x i ,

N con = F f =1 n f ,
and N 0 con is the summation of conflicts of all f when all of them fly without any decision changes, that is;

r f = r sch f , v f = v sch f , ∀f ∈ F , t f = t sch f .

C. Selection

Selection attempts to apply pressure upon the population, i.e. poorer performing individuals are weeded out and better performing, or fitter, individuals have a greater than average chance of passing the information they contain to the next generation.

The selection process which has been used in our experiments is a deterministic (λ, µ) tournament selection. This selection begins by randomly selecting λ individuals from the current population, P OP (k). Then, µ individuals having the highest fitness among them are selected again and added to a new population. This two steps are iterated until the generation of a new intermediate population P OP i (k) is completed.

D. Crossover

After the selection process, a crossover operator is applied to individuals selected with the crossover probability p c . Crossover generates one or more offspring individuals from two parent individuals P and P which belong P OP (k). The generated offsprings are added to a population of the next generation, P OP (k + 1). These processes ultimately result in the generation of a next population P OP (k + 1) that is different from the intermediate population (see Figure 4).

The crossover operator used in this research is bias uniform crossover, which works as the following steps (Figure 6). Firstly, two parent individuals P and P are selected randomly from the intermediate population, P OP i (k). Secondly, two positions of genes (flights), i and j, are selected randomly to determine which genes to be changed. For all genes, the following probability is computed:

p cr f = 1 - n f n f + n f (i ≤ f ≤ j),
where n f is the conflict number of gene (flight) f of P , and n f is that of P .

Then, for all genes f between i and j, all decisions associated with f of P is copied to the gene f of P with the probability of p cr f and those associated with f of P is copied to the gene f of P with the probability of 1 -p cr f . When there is no conflict in both parents, p cr f is set to 1/2.

Finally, two offspring individuals different from their parents are generated, and added to the next population, P OP (k + 1).

1 P P ' ⋯ ⋯ ⋯ 1 F ⋮ f ⋮ ⋮ 1 F ⋮ f ⋮ ⋮ 1 F ⋮ f ⋮ ⋮ Fig. 6. Bias Crossover.
This crossover operator has the bias to transfer the decisions of the gene which has less conflicts.

E. Mutation

If an individual is not altered by the crossover, it still has a chance to be changed by the mutation operator with the probability of p m /(1 -p c ), where p m is a mutation probability. The mutated individual is added to P OP (k + 1).

In the mutation operator, it would be an issue which gene ought to be mutated and how to determined the new allele. This could be a random choice or an ordinal relation between allele values which may be more sensible to restrict the choice to alleles that are close to the current value, or bias the probability distribution. In this research, it is introduced a bias crossover operator focusing on aircraft involved in conflicts.

As shown in Figure 7, once a parent individual P is selected, the bias mutation operator chooses one gene f with a probability associated with the conflict number;

p mu f = n f N con ,
and alters its decision variables.

In the selected gene, decision variables are changed randomly. For example, as for the route change, one route is chosen randomly from the possible set of routes R e f and r f is set to it. The speed change is given by the following formula,

P 1 F ⋮ f ⋮ 2 POP i (k) Selection of one parent individuals ! 1! 1 P ⋯ ⋯ ⋯ p m Change of gene f selected with p f mu ! 2! n 1 / N con n F / N con ⋮ n f / N con
v f = v min + ∆v * n v ,
where n v is a random integer variable satisfying

{n v |n v ∈ Z, 0 ≤ n v ≤ n vmax }, and n vmax = (v max - v min )/∆ v .
The slot change is done by the following formula:

t f = t sch f + ∆s * n s ,
where n s is a random integer variable satisfying {n s |n s ∈ Z, 0 ≤ n s ≤ n smax }, and n smax = ∆s max /∆s. After the decision change, the individual is added to the next population P OP (k + 1).

The bias mutation operator tries to prioritize the change of gene with a larger number of conflicts.

It can be note that the objective function is non linear, not convex and not separable. The state space is not connected meaning that deterministic optimization approach are not suitable for such problem. This problem is NP-Hard. Therefore, a stochastic approach based on Evolutionary Algorithms has been developed.

VI. RESULTS

This section has been divided in two case studies. The first one is intended to evaluate the effect of different

A. Case Study I: Comparison of the different strategies

The performance of each strategy: speed, route, slot change, or mix of them, is investigated in this section. Topology A1 in Figure 3 is used as the TMA design configuration for this analysis.

A traffic scenario with 50 aircraft per hour is used. Table III shows the traffic scenario in detail. It can be noticed that the most congested entry points is No. 2 corresponding to 38.0% each one of the total traffic. Within the flow entering by Node 2, the 26.3% correspond to aircraft classified as "heavy" and the remaining 73.7% is consider as "medium". The flow from Node No.1 contains 23.5% of heavy aircraft and 76.5% of medium size, composing 34.0% of total traffic flow. Finally, the remaining Node No.3 consists of 28.0% of total flow with 92.9% of heavy aircraft and 7.1% of medium size.

Table IV summaries the major results obtained in this case study using parameter presented in Table II. For the 50 aircraft traffic scenario, 917 initial conflicts are potentially induced as shown in the row called Initial conflicts. The initial conflicts are the conflicts induced when no strategy is applied, i.e. aircraft do not use neither of speed, route or slot change.

The row called Successful runs shows the number and percentage of runs which can successfully reach the conflict free solutions. For example, having 100% in this field indicates that all runs can derive conflict free solutions while a 13.3% (as in the case of speed change strategy) indicates that only 4 out of 30 runs can find conflict free solutions. Residual conflicts field shows the number and percentage of conflicts which remained unresolved within 500 generations. The percentage is the ratio to the initial conflicts and these values are average values of 30 runs.

The other rows represent the operational performance of obtained results. These values are the average of successful runs, thus the values are NA for the route and slot change strategies, because no run can derive the conflict free trajectories.

Regarding the four strategies which use speed change (speed change alone, speed and route change combined, slot and speed change combined, and mix of all changes), it should be noted that all of the strategies have the potential to derive the conflict free solutions. While even speed change alone can reach conflict free solution in 4 runs out of 30 runs, this performance is augmented drastically when it is combined with other decision changes, being able to resolve more than 98.2% of the initial conflicts. Especially when the speed change is combined with slot change, the strategy can resolve all conflicts in all of the runs. Meanwhile, 4 strategies lead very little differences to the average and maximum modified velocity as well as the number of aircraft which are subject to velocity changes. Approximately 48 aircraft are subject to changes in its speed, resulting in flying at a new speed of 282 kt on average.

Unlike the speed change, one can see that any of the runs with route change alone cannot reach a conflict free solution. The obtained residual conflict is the worst among 3 strategies using each change alone. However if the route change is applied in conjunction with another change or both of the others, solutions can be found in at least over 13 runs. In those strategies, the number of residual conflicts are very small ranging from 0.1% to 1.8%. In the runs which are able to reach a conflict free solution, the performance on flight distance is almost identical. The average extra flight distance ranges from 5.1NM to 5.4NM and the maximum extra flight distance is 15.6NM. These manoeuvre are applied to 39.5 to 41.7 aircraft in average.

The slot change by itself also can not reach conflict free solutions, but when it is applied in conjunction with another change or the mix of all it can find solutions, as already mentioned above. As for the delay at TMA entrance induced by slot change, the route and slot change induces 90.8 seconds delay, which is longer than those in the other strategies which range from 75.2 to 78.2 seconds.

Finally, an evaluation of the average and maximum delay at runway has been done to compare all strategies. Among the strategies which can reach the conflict free solutions, the speed change alone exhibits the best performance, inducing 61. [START_REF] Boursier | Integrating aircraft flows in the terminal area with no radar vectoring[END_REF] Figure 8 and 9 represents the evolution of average fitness and the average conflict ratio y = i y i /F through the generations. Here, one can see that slot and speed change strategy can reach the saturation fastest, which is followed by mix of all. While fitness growth of route and slot strategy is faster than that of speed and route strategy until 200 generations, it decelerates its pace after that point and surpassed by the speed and route strategy. Eventually, the route and slot shows the worst conflict resolution performance among the strategies using two decision changes. It is also interesting to point out that while speed change alone and slot change alone still shows potentials to grow their fitness at 500 generation, route change alone already shows the saturation of fitness.

These results suggest several implications. Firstly, speed decision has the highest potential in resolving conflicts among the 3 decisions. Secondly, when more than two decision variables are combined, the efficiency in deriving solutions is largely increased, and above all slot and speed change strategy and mix of all strategy can resolve conflicts quiet effectively. Thirdly, as the number of decision variables used in EA increases, larger delay is imposed at runway due to the nature of the conflict resolution strategies.

B. Case Study II: Comparison of the different topologies with the two traffic scenarios

The previous case study is intended to test the benefits of a set of strategies to minimizes the total number of conflicts of an arrival in on hour traffic scenario. For the second case study, it is aimed to compare the efficiency of different TMA design configurations by minimizing both, the total number of conflicts, and the delay of each aircraft. Therefore, other fitness function has been develop to evaluate the benefit of the delay minimization.

Tests are conducted with two different fitness functions: the first fitness function deals with the minimization of the total number of conflicts, as described in Section V-B; while the second fitness function minimizes the delay time at the runway, and is defined as follows:

f i = 1 0.01 + y i + 1 0.01 + z i , z i = F f =1 max{0, (t a f -t asch f )/60} F ,
where t asch f is the scheduled arrival time at the runway of flight f , t a f is an arrival time after the conflict resolution strategies are applied, and z i represents the average of delay caused by the strategies for all aircraft, normalized by 60 seconds.

The performance of diverse topologies depicted in Figure 3 where tested within this Section. The traffic scenario used is presented in Table III. The parameters used to tune the Evolutionary Algorithm are the ones presented in Table II, except for the number of generations. For this experiment, 1500 generation is adopted to see the evolution of delay more clearly.

Table V summaries the major results obtained in this case study. Different numbers of initial conflicts are predicted for each topology. For example, for Topology B1, it has been found 842 potential Initial conflicts meanwhile Topology A2 predicts 1228 potential Initial conflicts. It should be noted that for both sub-route structures (A and B), two merging points always impose higher level of initial conflicts. This is because in the two merging points cases, aircraft from entry node 2 and 3 need to be merged and are required to fly in the same link earlier than in the one merging point cases.

The Residual conflict row shows that more than 99.9% of the initial conflicts are resolved in all topologies, while the Successful runs row shows that the worst case is to use Topology A2 with minimizing only conflicts, which succeeds in resolving all conflict in 25 runs of 30.

In both fitness functions, four topologies propose similar results regarding the velocity. When minimizing only con-flicts, the average modified velocity varies between 281.6 to 284.1 kt, Maximum modified velocity is approximately 309 kt, and about 48 aircraft are subject to change their velocity. When minimizing both conflicts and delay, the strategy changes the velocity of approximately 44 aircraft, which results in the Average modified velocity of 298.1 kt to 300.3 kt and the Maximum modified velocity of 310 kt. It should be noted that adding the delay minimization fitness increases the velocities and reduce the number of decision changes.

Unlike the velocity changes, four topologies bring some changes to the results regarding the flight distance performance in both fitness functions. For example, it is interesting to see that Topologies "B" is better in Number of aircraft with route changes, inducing less aircraft to change their route decisions than Topologies "A". Regarding the distance, when dealing only with the minimization of conflicts, the Average extra flight distance ranges between 4.9 NM to 5.9 NM. When minimizing both conflict and delay, the Average extra flight distance is reduced by between 50% and 60%, ranging from 2.6 NM to 3.5 NM. The worst efficient design in term of extra distance is A2, adding the largest extra distance and the number of decision changes.

The average delay at TMA entrance is also subject to change by the topology difference. When minimizing only conflicts, topologies having one merging point seem to be the most efficient, introducing an average delay of approximately 74 seconds to 24 aircraft. When minimizing both conflicts and delay, this feature is also the same, but between A1 and B1, Topology A1 shows better performance. As expected, one can see the abatement of delay level at TMA when minimizing both conflicts and delay.

The total Delay time at runway is taken as a key performance indicator to compare the topology efficiency. In this sense, when minimizing only conflicts the most efficient topologies are topologies having one merging point. When minimizing conflicts and delays, this is also the case but Topology A1 shows better results than B1, inducing a total average delay of 35.3 seconds to 26 aircrafts. Here, one can also see the significant abatement of the Delay time at runway and the number of delayed aircraft by using delay optimization.

Figure 10 and Figure 11 depict the evolution of the average fitness and the average conflict ratio (y) respectively. As depicted in Figure 11, conflict ratio decreases almost to zero after 200 or 300 generations in all topologies. Figure 10 reveals that Topology A2 has the worst performance in fitness evolution while the other three topologies show almost the same performance.

Figure 12 shows the evolution of the average fitness for all topologies when minimization delay in conjunction with conflicts. Also in this case, the performance of Topologies A1, B1 and B2 is quite similar except for Topology A2 which has lower efficiency in reaching conflict free solutions. The associated evolutions of the average conflict ratio (y) and the average delay at runway (z) are given in Figure 13. Here, one can see that the average conflict ratios reach to almost zero after 200 or 300 generations. After achieving this enough abatements of conflicts, the average delays at runway start to decrease. In Figure 13, it should be noted that Topology A2 imposes higher delay at runway in the early stage of generation, while the other topologies impose the same level of delay. Also it is interesting to point out that topologies having one merging point achieve faster decrease of delay at runway than the topologies having two merging points.

As overall conclusions, some points are suggested. First, the results shows that one merging point topologies have better performance especially in delay criteria. Secondly, the experiment reveals that Topology B1 is the most efficient when minimizing only conflicts because of the performance in route decision change. Thirdly, Topology A1 is the most efficient when minimizing both conflicts and delay, because of its delay performance.

VII. CONCLUSIONS

The imminent growth of the air traffic requires a broadly applicable and reliable set of Decision Support tools to improve strategic planning in the Air Traffic Management domain. Such tools must be able to cope efficiently and safely with the growing demand.

Genera9on

A1"conflict" A2"conflict" B1"conflict" B2"conflict" A1"delay" A2"delay" B1"delay" B2"delay" Fig. 13. Evolution of average conflict ratio (y) and average delay at runway (z) when minimizing conflicts and delay A novel approach for the aircraft sequencing and merging problem in TMA was presented. An Evolutionary Algorithm was adopted to tackle this problem, for which chromosome coding and several computational operators have been developed. For each aircraft, route, speed & entry time can be changed as decision variables to find a set of conflict free trajectories. This algorithm has been applied to Gran Canaria airport in Spain with real traffic demand samples.

The first objective of this work is to do a comparative study among strategies to analyzed how the different strategies affect the various performance like efficiency in conflict resolution and delay time. In this case study, the results showed that slot and speed strategy is the most effective to resolve conflicts within TMA. This strategy induces to 84% of the aircraft an average delay at runway of 140 seconds. The mix of all strategy also shows the efficient conflict resolution, but this time 92% of aircraft are delayed at runway for 199 seconds.

The second objective of this work is to investigate the effect of different topologies designs for TMA. Therefore, four topology designs were proposed as TMA route structure. In this case study, it has been found that topologies having one merging point usually impose less delay. Also it is shown that Topology B1 is the most efficient when minimizing only conflicts, whereas Topology A1 is the most efficient when minimizing delay at runway. Through this case study, it was also demonstrated that incorporating delay evaluation in the fitness function successfully worked and the algorithm could abate the delay level significantly.

Further research can be done in order to develop a continuous model approach to deal with the route change strategy at TMAs. To this aim, the scheduling model and algorithm must be improved with, for example the Constrained Position Shifting (CPS) method [START_REF] Balakrishnan | Algorithms for scheduling runway operations under constrained position shifting[END_REF]. Other research directions concern with the development of algorithms for computing optimal routes from En-Route sectors. The model can also be improved to test the sequencing algorithm in a dynamic simulation in which aircraft are added to the entry queue as soon as they arrive and being removed from the queue as they land.

VIII. ACKNOWLEDGMENT

This research effort has been partly funded by a project in the air traffic management domain with the aim of providing a significant contribution to the attainment of the common European goals set by the SESAR program and beyond. The project has been called XXX by XXX. Other part of the founding come from the Mexican Institution called Consejo Nacional de Ciencia y Tecnología (CONA-CyT) whose efforts have been also very important.

Fig. 1 .

 1 Fig. 1. Conflict detection strategy

• r sch f :

 f Scheduled route of flight f . • v sch f : Scheduled velocity of flight f at TMA entry point. • t sch f : Scheduled time slot of arrival of flight f at TMA entry point.

Fig. 3 .

 3 Fig. 3. TMA configuration

Fig. 4 .

 4 Fig. 4. Genetic Algorithm with Tournament Selection. The first step consists in the selection of the best individuals from population P OP (k).Afterward, recombination operators are applied in order to produce the P OP (k + 1) population.

Fig. 5 .

 5 Fig. 5. State Space coding

Fig. 7 .

 7 Fig. 7. Bias Mutation.

  followed by the speed and route change strategy, which shows 128.4 seconds average delay to 43.7 aircraft.

Fig. 9 .

 9 Fig. 8. Evolution of average fitness

Fig. 10 .Fig. 11 .Fig. 12 .

 101112 Fig. 10. Evolution of average fitness when minimizing only conflicts

  Both case studies are based on one hour of arrival traffic at Gran Canaria airport. The experiments are executed on a 2.4Ghz Mac OS X operating system PC based on a Java code. TableIIpresents the parameters used to run the Evolutionary Algorithm for both case studies .

	Parameters		Value
	Simulation runs		30
	Number of generation	500
	Population size		100
	Probability of Crossover	0.2
	Probability of Mutation	0.8
	Elitism		yes
	Selection (λ, µ)		(5, 3)
	TABLE II
	PARAMETERS FOR CASE STUDY I
		Traffic	Heavy	Medium
	Traffic flow entering by Node 1	34.0%	23.5%	76.5%
	Traffic flow entering by Node 2	38.0%	26.3%	73.7%
	Traffic flow entering by Node 3	28.0%	92.9%	7.1%
	TABLE III
	CHARACTERISTICS OF THE SCENARIO WITH 50 AIRCRAFT PER HOUR
	conflict resolution strategies in a cooperative approach; the
	second case study aims to compare diverse TMA topologies
	(arrival route structures) using a mix of conflict resolution
	strategies.

  seconds average delay to 48.3 aircraft. This result is

	Scenario				50
	fitness				Section V-B
	Topology			A1 (Figure 3 (a))
	Strategy	Speed	Route	Slot	Speed +Route	Route + Slot	Slot + Speed	All
	Initial conflicts				917
	Residual conflict	38.1 (4.2%)	183.4 (20.0%)	53.0 (5.8%)	16.2 (1.8%)	4.8 (0.5%)	0.0 (0.0%)	0.1 (0.0%)
	Successful runs	4 (13.3%)	0 (0.0%)	0 (0.0%)	13 (43.3%)	15 (50.0%)	30 (100.0%)	29 (96.7%)
	Average modified velocity [kt]	281.7	NA	NA	282.6	0.0	282.1	283.2
	Maximum modified velocity [kt]	309.5	NA	NA	309.1	0.0	309.5	309.4
	Number of aircraft with velocity changes	48.3	NA	NA	48.5	0.0	48.2	48.1
	Average extra flight distance [nm]	0.0	NA	NA	5.3	5.1	0.0	5.4
	Maximum extra flight distance [nm]	0.0	NA	NA	15.6	15.6	0.0	15.6
	Number of aircraft with route changes	0.0	NA	NA	41.7	39.5	0.0	41.1
	Average delay at TMA entrance [sec]	0.0	NA	NA	0.0	90.8	78.2	75.2
	Maximum delay at TMA entrance [sec]	0.0	NA	NA	0.0	298.0	297.0	299.0
	Number of aircraft with slot changes	0.0	NA	NA	0.0	29.7	25.4	24.2
	Average delay at runway [sec]	61.7	NA	NA	128.4	152.3	140.3	199.7
	Maximum delay at runway [sec]	281.7	NA	NA	399.4	434.2	524.7	594.7
	Number of aircraft delayed	48.3	NA	NA	43.7	45.2	41.7	46.0
			TABLE IV
	RESULTS OF CASE STUDY I: COMPARISON OF STRATEGIES

TABLE V RESULTS

 V OF CASE STUDY II: COMPARISON OF THE DIFFERENT TOPOLOGIES


Bertrand Jeannet

Fabien Gaucher

Debugging Embedded Systems Requirements with STIMULUS: an Automotive Case-Study

Keywords: Requirement Engineering, Real-time Embedded Systems, Domain Specific Languages, Formal Methods, Debugging, Simulation. I

In a typical software project, 40% to 60% of design bugs are caused by faulty requirements that generate costly ite rations of the development process as specifications need to be re de fined, design and implementation modified accordingly, and the n retested. The major reason for this situation is that no practical tool exists for debugging requirements while drafting spe cification, and the many tools that exist for requirement management and traceability do not address this problem.

STIMULUS provides an innovative solution for the early de bugging and validation of functional real -time systems re quirements. It provides a high-level language to express textual ye t formal requirements, and a solver-driven simulation engine to ge nerate and analyze execution traces that sati sfy re quirements. Visualizing what systems will do enables system architects to discover ambiguous, i ncorrect, missing or conflicting requireme nts before the des ign begins.

We demonstrate the use of STIMULUS on the specification of automatic headlights from the automotive industry. We show how this unique simulation technique enables to discover and to fix ambiguous and conflicting requirements, resulting in a clear and e xecutable specification that can be shared among engineers.

INTRODUCTION

Many tools have been proposed for the development of embedded software, in which the validation activity may represent more than 60% of the whole development effort. In this process, functional validation aims at checking that the system design is correct with respect to requirements, but few tools exist for the functional validation of system requirements themselves.

In this paper, we focus on real-time requirements, such as the following cruise control example: "When active, the cruise control shall not permit actual and desired speeds to differ by more than 2 km/h during more than 3 seconds."

Such requirements usually describe a combination of logical and numerical properties of system signals over time. They stand in contrast to non-functional requirements, such as performance, usability, reliability, cost, etc. Being requirements, they express what a system should do or not do, but they do not describe how to achieve it: here for instance it could be done with a PID (proportional-integral-derivative) controller.

In practice, requirements are mostly written in natural language and are generally validated through manual reviews. As a consequence, many ambiguities and errors remain until validation testing. It is well-known that the later these errors are detected, the more expensive it is to fix the bug. The cost is even worse when third parties are involved as the extra process iterations involve specification and contractual changes.

Argosim STIMULUS addresses this issue of requirement early debugging and validation by providing two key features:

(I) Expresses real-time requirements and environment assumptions in a formal yet close to natural specification language;

(II) Generates and observes simulation results that satisfy requirements under environment assumptions.

The ability to formalize requirements in an easy-to-read language is a necessary condition for the approach to get acceptance by users, while the ability to simulate "what systems shall do" makes requirements validation possible while writing specifications, instead of delaying it to a later phase of the development process. This limits specification errors and ultimately reduces costs in the design phase.

In this paper we show how STIMULUS supports these claims by describing its technical foundations and by illustrating its use to formalize, debug and validate the requirements of a car automatic headlights controller which was provided to us by a Japanese software and tools vendor.

II.

RELATED WORK Several requirement engineering tools do exist, such as IBM DOORS. Compared to STIMULUS, they focus on requirement management and traceability, rather than validation.

Specification and simulation tools, like UML/SysML or Mathworks Simulink, aim at modeling and validating system design and architecture rather than high-level requirements. There are efficient at describing how a system should be implemented, but they lack the expressiveness to describe and to simulate what a system should do without describing the how. The case-study of this paper will clarify this point.

Formal methods tools, in particular model-checkers and proof systems, like the Rodin platform based on Event-B [START_REF] Abrial | Modeling in Event-B -System and Software Engineering[END_REF], provide expressive languages and exhaustive validation features. There are the tools to use to prove the consistency of a set of worked-out requirements, but less so to incrementally debug partial, possibly incorrect requirements and to discover missing requirements, for the two following reasons.

1. They can only detect formalized inconsistencies: they do not help the user to discover problems that he has not anticipated.

Consider the cruise control example given in introduction.

Before submitting this requirement to a model-checker or a proof assistant, the user has to define a relevant property to prove on it, which is not trivial. Moreover, there is no a priori guarantee that the chosen property can detect a mistake like omitting the absolute value operator when translating the condition "speeds should not differ by more than two km/h". In contrast, as we will see, the simulation feature of STIMULUS enables the user to discover unanticipated problems in requirements by observing simulation traces.

2. Model-checkers and proof assistants require fairly complete requirements to issue relevant results , that is, either a successfull proof of a non-trivial property on them, or a meaningful counter-example to it. This makes this approach hard to use in an incremental specification process where rough initial requirements are progressively refined.

The two approaches are actually complementary:

 STIMULUS enables to debug requirements and to validate them by simulation; its strength is its ability to quickly exhibit problems. This provides a level of confidence in the quality of requirements, which is arguably higher than the level provided by manual reviews, but do not deliver either a formal proof of consistency and correctness.

 Once good quality requirements are obtained, they can be submitted to model-checkers and/or proof systems to obtain formal proofs. Problems can still be discovered at this step, but much less frequently than if the previous step had not been performed.

This complementarity motivated a partnership with SafeRiver, a consulting company specialized in safety and cyber-security for software-based systems. SafeRiver makes intensive use of formal methods and tools, and is looking for solutions to speed up the correct formalization of safety requirements before performing exhaustive proofs on them.

III. STIMULUS TECHNICAL FOUNDATIONS

The scientific backgrounds of STIMULUS being detailed in [START_REF] Abrial | Modeling in Event-B -System and Software Engineering[END_REF], we give only an overview of it. The two key features of STIMULUS are an expressive formal specification language and a simulation engine based on a constraint solver.

A. A Constraint Real-Time Specification Language

Stimulus combines the concepts of the synchronous languages LucidSynchrone [START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF] and Lutin [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow programs[END_REF]:  LucidSynchrone (like its industrial version SCADE) provides proven and mature concepts for modeling realtime systems, such as dataflow equations, hierarchical state machines, and synchronous parallel composition.  Lutin provides the concepts needed for modeling realtime non-deterministic behaviours, namely dataflow constraints and non-deterministic control choices. It was designed for describing generic test scenarios for realtime systems. We list below the main concepts of the resulting language.

a. Data: Synchronous Data-Flow Constraints

The behaviour of signals is specified with dataflow constraints like: count = (0 -> last count) + (if evt then 1 else 0); count <= 10; in which the integer signal count counts the number of occurences (in time) of the Boolean signal evt and is constrained to be less than or equal to 10. -> is the initialization operator : e1 -> e2 evaluates to e1 on reset, and to e2 otherwise, and last v denotes the value of signal v in the previous step. In other words, this specifies than evt might be true at most ten times during an execution, but specifies nothing more about when evt can or cannot be true.

b. Control: Hierarchical State Machines.

They are typically used to model running modes, to define the temporal operators of the standard library, and also to model probabilistic choices in scenarios. States can contain constraints, as shown by the state machine of Fig 1 . State machines in STIMULUS have a strong, preemptive transition semantics according to the terminology of [START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF]: transitions are fired and their condition evaluated in the same step as their destination state. In addition, they implement an original notion of termination which happens to be crucial to combine the temporal operators of the standard library.

c. Modularity: Systems and Macros.

As other synchronous languages or Mathworks Simulink, Stimulus encapsulates statements into systems that can then be Fig. 1: requirement about the occurrences of evt instantiated at several places. One can for instance define a system Count that counts the number of occurrences of an event (using an internal memory) and that can be reused to specify more complex constraints, like Count(evt1) >= Count(evt2).

Stimulus also provides a robust system of macros with clear scoping and typing rules that accepts statements as parameters, in addition to signals having a value. They are used to define temporal operator, such as the when <condition>, <BODY> operator defined by the macro depicted on Fig. 2.

d. Readability: Sentence Templates

Formal requirements are easier to read when they look like textual requirements instead of programs. To achieve this goal, a system or macro can be associated with a user-defined format that specifies how instances should be edited and displayed in the editor.

For instance, if one associates to the macro When and the system Count the formats When %condition%, %<BODY>% and number occurences of %event%, the requirement of Fig. 1 rewritten using When and Count will appear as: which is arguably more concise and more readable than the automaton of Fig. 1, while still enjoying the same unambiguous, formal definition.

e. Architecture: Block Diagrams.

Systems can be instantiated not only as a sentence, as described above, but also as blocks connected to other blocks in block diagrams, like in Mathworks Simulink, see Fig. 8. This enables developers to graphically describe the architecture of a system and to visualize the flow of information in it.

Other technical features of the STIMULUS language are a construct for controlling constraint propagation and orienting constraints, in the spirit of [START_REF] Somogyi | A system of precise modes for logic programs[END_REF], which provides scalability both for solving constraints and for model understanding by the user, type inference techniques of functional languages [START_REF]The OCaml programming language[END_REF][START_REF]The Haskell programming language[END_REF] to minimize the annotations required from users, and a physical dimension analysis [START_REF] Goubault | Inférence d'unités physiques en ML. Journées Francophones des Langages Applicatifs[END_REF][START_REF] Kennedy | Dimension Types[END_REF] to statically detect this kind of inconsistencies.

Regarding the modeling of time, currently STIMULUS provides a simple periodic physical time model, by using a period to assign physical time values to logical time steps. In the long term we plan to provide a more flexible, aperiodic time model.

B. Compilation Process and Simulation Engine

SIMULUS compilation process follows the principles of [START_REF] Hamon | Modular resetting of synchronous dataflow programs[END_REF][START_REF] Colaço | Type-based initialization analysis of a synchronous data-flow language[END_REF][START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF][START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow programs[END_REF] for (i) reducing parallel composition of hierarchical state machines to sets of statements guarded by choices on the clocks representing the active states of state machines, and (ii) ordering statements properly with res pect to dependency constraints.

The simulation engine follows the principles of [START_REF] Jahier | Case studies with Lurette V2[END_REF][START_REF] Raymond | Lutin: A Language for Specifying and Executing Reactive Scenarios[END_REF] and combines an exploration algorithm for resolving the nondeterministic choices induced by state machines and a constraint solver for resolving the non-determinism induced by constraints on variables. The solver handles logiconumerical constraints mixing logical operators on Boolean and enumerated variables, and linear constraints on numerical variables. The restriction to linear numerical expressions concerns only the unknown variables to be solved: the solver can deal with non-linear sub-expressions on variables that are known at solving time, like inputs or memories. For instance the constraint x*(last x) >= y*(last y)*(last y) is linear on the unknowns x and y.

IV. METHODLOGY FOR DEBUGGING REQUIREMENTS

In the previous section, we gave an overview of a new real-time constraint programming language built by combining the two research lines of work lead by M. Pouzet [START_REF] Hamon | Modular resetting of synchronous dataflow programs[END_REF][START_REF] Colaço | Type-based initialization analysis of a synchronous data-flow language[END_REF][START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF][START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow programs[END_REF] and by the synchronous team of VERIMAG laboratory [START_REF] Jahier | Case studies with Lurette V2[END_REF][START_REF] Raymond | Lutin: A Language for Specifying and Executing Reactive Scenarios[END_REF][START_REF] Jahier | Engineering functional requirements of reactive systems using synchronous languages[END_REF][START_REF] Jahier | Environment model-based testing of control systems : cases studies[END_REF]. Now, how can it be used to debug requirements of real-time systems ? With the current practice, requirements are mostly textual that are worked out and validated through manual reviews, and then given as inputs to 1. system designers and programmers on the one hand, who will implement the system; 2. test engineers on the other hand, who are in charge of writing functional test cases and test verdicts to confront the implementation w.r.t. the initial requirements. Fig. 3 depicts the functional test bench architecture of a realtime system. I and O denote resp. the inputs and outputs of the System Under Test (SUT), which is considered as a black box. The box "Scenarios" feeds the SUT with inputs I, possibly taking into account outputs O to produce realistic inputs. The box "Requirements" reads both inputs I and outputs O of the IUT and emits a verdict.

As mentioned in the introduction, the experience shows that half of the bugs discovered by functional tests are requirements bugs, and not implementation bugs. The problem is that these bugs can be found only after the SUT becomes available.  The box "scenarios" in Fig. 4 acts as an inputs generator: given outputs O provided to it by the feedback loop, the simulation engine solves the constraints in the remaining unknowns I and picks a random solution for them.

The fact that scenarios may be generic scenarios with a large variability on control and data allows the simulation engine to generate many different simulation traces, and ultimately makes more likely the discovering of an unexpected behaviour corresponding to a problem in the requirements. Actually scenarios are optional: one may simulate requirements alone. However, in practice, one often needs some general assumptions on the stability or the variation of signals to make simulation traces readable or realistic.

Another important observation is that once scenarios and requirements have been worked out using the architecture of Fig. 4, they can be reused directly in the test architecture of Fig. 3 with a black-box system under test: indeed, there are executable, and STIMULUS have a mechanism to turn a generator into an observer, which enables to turn the requirements box of Fig. 4 in the requirements box of Fig. 3.

We described in the two previous sections the scientific foundations of STIMULUS and the methodology it enables for debugging requirements together with their associated generic test scenarios. The sequel of the paper aims at answering to the following questions:  How does it work in practice? Is it easy to formalize informal textual requirements with STIMULUS? How far is the formalized version to its informal counterpart in term of readability (traceability feature)?  Are simulation traces effective at discovering problems?

In other words, despite the non-exhaustiveness of our validation-by-simulation approach, is it "exhaustive enough" in practice? To answer to these questions, we will illustrate the use of STIMULUS for formalizing and debugging requirements of an automatic light system coming from the automotive industry.

V. FORMALIZING THE REQUIREMENTS OF AUTOMATIC HEADLIGHTS

These requirements were provided to us by a Japanese software and tools distributor, as a typical example of the kind of requirements his customers have to deal with in the automotive industry. We insist on the fact that they have not been specifically invented for evaluating a tool like STIMULUS, neither by us nor by researchers or developers of alternative solutions.

The original, textual specification of the automatic headlights is depicted on Fig. 5. The head sentence is a sort of informal, high-level requirement that describe the general purpose of the four more precise, lower level requirements that follow. This purpose is to command the switching of the lights. In the sequel we will formalize the four requirements named 3Aa, 3Ab, 3B and 3C.

Fig. 6 depicts the initial formalization of requirement 3Aa, which will be debugged by simulation and upgraded in the next sections. One recognizes in Fig. 6 the pieces of sentence underlined on Fig. 5. This formalization is based on the use of STIMULUS standard library, which provides a number of sentence templates that are ubiquitous in real-time requirements, such as:  "as long as <expression>, <statement>"  "initially <statement>, afterwards <statement>"

As explained in Section III.A.d, such sentence templates are user-definable views for formal systems and macros, and their purpose is to make easy tracing the formalized requirement back to the textual, non-formalized requirement.

The other requirements 3Ab, 3B and 3C are similarly formalized. 3Aa and 3Ab roughly specifies an hysteresis. 3B and 3C in addition require the light intensity to be low or high to hold for some time before s witching respectively on or off the headlights. This is to prevent the headlights to blink too quickly, for instance when driving under a bridge.

VI.

SIMULATING AND REFINING THE REQUIREMENTS We just showed how the requirements can be formalized. However the major innovation of STIMULUS is the ability to simulate them.

A. Simulation architecture

Fig. 8 depicts the block diagram defining the simulation architecure considered in this paper. The block En v generates values for the signal lightIntensity that satisfy the assumptions depicted on Fig. 9. These assumptions combine general physical assumptions the range of the light intensity (a percentage of a maximum intensity) and of its derivative, and a scenario making it alternatively increase or decrease. In this paper, we maintain the signal switch to AUTO, as we want to simulate the behaviour of the system under this mode.

The block R003_v1 on Fig. 8 is defined by the requirements discussed in Section Erreur ! Source du renvoi introuvable.. This block will generate possible values for headLight that are compatible with these requirements and the values of the other signals.

B. First simulation and detection of a problem

Fig. 10 depicts a possible execution trace of the system defined by Fig. 8. One can observe the behaviour of lightIntensity and headLight signals. L60 and L70 are the two thresholds 60% and 70% that appear in the requirements.

What can be observed is that at start headLight has the expected behaviour: it is first OFF because the light intensity is above the 70% threshold, and when the light intensity falls below the 60% it becomes ON. However, afterwards the behaviour seems completely random and appears in contradiction with the intended behaviour.

Hence the simulation exhibits a problem either in the textual requirements, or in their formalization, or in both.

C. Investigating and solving problem 1

Consider the textual requirement 3Aa on Fig. 6 and more precisely its second part: "[…] Afterwards the headlights should continue to stay ON in AUTO as long as the light intensity is not above 70%". The textual expression "as long as" is actually ambiguous: does it mean 1. as long as condition, something [afterwards nothing]" (sequential behaviour)

If the switch is AUTO then the headlights turn on or off, depending on the ambient light intensity -with a defined hysteresis to prevent blinking. REQ_003Aa: if the switch is turned to AUTO, and the light intensity is at or below 70% then the headlights should stay or turn immediately ON.

Afterwards the headlights should continue to stay ON in AUTO as long as the light intensity is not above 70%. REQ_003Ab: if the switch is turned to AUTO, and the light intensity is above 70% then the headlights should stay or turn immediately OFF.

Afterwards the headlights should continue to stay OFF in AUTO as long as the light intensity is not below 60%. REQ_003B: if the switch is in position AUTO, the headlights are OFF, and the light intensity falls bellow 60%, then the lights should turn ON if this condition lasts for 2s. REQ_003C: if the switch is in position AUTO, the headlights are ON, and the light intensity is above 70%, then the lights should turn OFF if this condition lasts for 3s. or "[always] when condition, something" (cyclic behaviour)? This ambiguity is not really an artefact introduced by STIMULUS sentence templates: it is a real ambiguity which already exists in the textual version, between a sequential or a cyclic behaviour.

On Fig. 6 we opted inadvertently for the first interpretation, but clearly we expect a cylic behaviour here. Let us try the second one, which is available in the standard library. Requirement 3Ab which follows the same pattern is similarly modified. Let us simulate this new version of requirements:

We obtain a conflict at simulation step 6: this means that some requirements are contradicting each other. Let us highlight the requirement 3Aa and 3Ab in the debugger at step 6 where the conflict occurs:

The debugger highlights the active parts of the requirements, and allows the user to discover that at this step, the requirements implie headLight to be ON and OFF at the same time!

D. Investigating and solving problem 2

Consider again the textual requirement 3Aa on Fig. 1. We formalized the expression "headLights should continue to stay ON" underlined in Fig. 1 with the formalized sentence "headLights shall be ON". Was that the right interpretation? The sentence could also mean:

"if it was ON, maintain it at ON, otherwise do nothing".

To check this hypothesis, we defined a new, user-defined sentence template "<expression> should continue to stay <constant>" A last problem, that we will not detail as much, concerns the requirements 3B and 3C: they express that something should happen when a condition hold for some time duration, but say nothing about what should happen before. Hence unwanted, blinking head lights behaviour might occur with a more generic scenario in which the switch is not always equal to AUTO. This is a typical example of a missing requirement.

VII. DISCUSSION

The four textual requirements of Fig. 5 look rather simple and reasonable. Yet they contain several ambiguities and omissions, some of them leading to unwanted behaviours, others to contradictions. Actually, although looking simple, they specify a complex behaviour that depends on the past history of signals, and on physical time. This complexity behind apparent simplicity is typical of real-time requirements and explains the strong need for their early validation, especially as they are often requirements of security-critical systems.

A. Comparison of simulation approach to alternative

requirements validation approaches It is difficult to discover by manual reviews the problems we discovered by simulation. This is why many of them are discovered later, either by developers or test engineers when they start exploiting the requirements given to them, or, worse, even later during the functional test phase.

We claim that model-checker or formal proof systems are not very suitable either for this debugging and elicitation task. For detecting and fixing the first problem found in Section VI.D, it is necessary 1. to explicitly formalize the higher-level property capturing the bad behaviour, which requires having already identified it as a potential error; 2. to check the validity of the requirements against this propertythis will fail of course; 3. to analyse the cause of the failure and to try a new alternative.

The simulation approach made possible by STIMULUS (i) completely removes the need for subtask 1; the user can still insert property observer to automatize the detection of an already identified potential problem, but this is optional; this subtask is actually replaced by the observation of simulation traces enabling the discovery of unanticipated behaviours or getting an higher confidence in the relevance of the requirements (ii) makes subtask 2 arguably easier: model-checkers may have an is sue with too complex models, either in terms of size or expressiveness (non-linear computations for instance), and proof systems are not always fully automatic; in contrast simulation techniques are less computationally demanding and can handle complex models fully automatically1 . Subtask 3 remains the same but in overall the removal or the simplification of the other subtasks make the trial-error cycle much quicker.

The use of model-checking and formal proof approaches is of course still meaningful to obtain an exhaustive confirmation of consistency, or to discover inconsistencies occurring in very uncommon cases that a simulation approach may miss.

B. Evaluation w.r.t. announced criteria

At the end of Section IV describing our methodology, we proposed two main evaluation criteria to our approach, namely: 1. Easiness of formalization, readability of formal models and traceability w.r.t. informal, textual requirement; 2. Effectiveness of the simulation engine in generating simulation traces exhibiting problems, that is, sufficient "practical exhaustiveness". We hoped to have successfully convinced the reader that the formalized requirements of Figs. 6 and 7 remain close to and as concise as their informal counterpart of Fig. 5. Although these formal requirements are not pure English, everybody can understand what they are talking about. In addition, they gain a perfectly formal semantics: the user can look at the formal definitions of the sentence templates to get a more in-depth understanding of a sentence, and simulate them to observe their dynamic behaviours.

Technically, this is a benefit of the combination of a powerful programming language (which is mostly hidden to the user), the use of sentence template as a view for programming constructs, and the design of well-thought standard library.

Regarding the second evaluation criteria, the two problems discovered in Section VI were both discovered with the very first simulation trace. This means that although the validationby-simulation approach is not exhaustive, in practice the simulation engine is efficient at quickly exhibiting problems when they exist. In particular, the conflict discovered at the end of Section VI.C, which would have been easily found by a model-checker, was in practice as easily found by the simulation engine, using the very unspecific generic scenario of Fig. 9.

Of course, if the assumptions on the environment disallow some scenario, STIMULUS will not exhibit problems that are specific to them. But the same applies to model-checkers and formal proof systems: formal proofs are valid only w.r.t. the considered assumptions on the environment. STIMULUS actually supports the incremental process of starting debugging requirements with very simple scenarios, and later stimulating them with more complex or corner-case scenario. This process allows the user to progressively gain confidence in the quality of its requirements, instead of having to cope with too many unwanted behaviours at a time.

Technically, the effectiveness of the STIMULUS simulation engine for generating "really random" traces inside the set of possible traces satisfying the requirements comes from the use of a general constraint solver and of a fair algorithm to pick a random solution inside the solution space.

VIII.

CONCLUSION In this paper, we presented STIMULUS, a modeling and simulation tool for the early validation of functional real-time requirements, and we demonstrate its effectiveness for debugging a few requirements typical of the industrial practice, which contain subtle ambiguities and omissions.

STIMULUS is based on modern programming languages and simulation techniques, with many features dedicated to requirement readability. It exploits mature and well-proven research results to make things simple for the users.

It enables engineers to formalize requirements using predefined or user-defined sentence templates, to model environment assumptions and to observe execution traces that satisfy the requirements using the innovative simulation architecture of Fig. 4. It helps finding ambiguous, incorrect, incomplete, or conflicting requirements, as shown on the realtime requirements of an automatic head lights controller of a car provided to us by a software and tools vendor.

Relying on this case study, we discussed the additional benefits that the validation-by-simulation approach for requirements engineering proposed by STIMULUS can bring to the current validation-by-review and validation-by-proof approaches. One can actually observe than in the different domain of control system design, one of the most popular tool is TheMathworks Simulink, which also implements a validation-by-simulation approach.

We did not detail in this paper how to reuse STIMULUS scenario and requirements models for testing black-box realtime systems as depicted on Fig. 3, but this is a hot topic for our customers. Other topics are the automation of some common editing tasks, such as providing functional coverage criteria for requirements, and to automate debugging and testing tasks, such as guiding executions to favor the functional coverage of requirements according to these criteria.

Fig. 2

 2 Fig.2 Macro defining the temporal operator When

Fig. 3 :Fig. 4 :

 34 Fig. 3 : Classical test architecture of a real-time system

Fig. 5 :Fig. 6 :

 56 Fig. 5: Original specification of the automatic headlights

Fig. 8 :Fig. 9 :Fig. 10 :

 8910 Fig. 8: simulation architecture

Fig. 12 :Fig. 11 :

 1211 Fig. 12: Simulation of requirements after the second correction

As mentioned in Section III.B, the constraints of STIMULUS models should be linear, but only on the unknown variables at solving time, which is not restrictive in practice.