Jean-Marc Nicod

Laurent Philippe

Lamiel Toch Thème

Cartoon

A Genetic Algorithm to Schedule Workflow Collections on a SOA-Grid with Communication Costs

Keywords: Batch scheduling, grid computing, heterogeneous platform, genetic algorithm

In this paper we study the problem of scheduling a collection of workflows, identical or not, on a SOA grid. A workflow (job) is represented by a directed acyclic graph (DAG) with typed tasks. All of the grid hosts are able to process a set of task types with unrelated processing costs and are able to transmit files through communication links for which the communication times are not negligible. The goal is to minimize the maximum completion time (makespan) of the workflows. To solve this problem we propose a genetic approach. The contributions of this paper are both the design of a Genetic Algorithm taking the communication costs into account and the performance analysis.

Algorithme Génétique pour Ordonnancer un Ensemble de Workflow sur une Grille Orientée Service avec des Co ûts de Communications

Résumé : Dans ce rapport de recherche nous considérons un problème pour ordonnancer un ensemble de workflows, identiques ou non, sur une grille fondée sur une architecture orientée service. Un workflow (job) est représenté par un graph acyclique orienté avec un des tâches typées. Chacune des machines de la grille savent exécuter un ensemble de type de tâches prédéfinies avec des coûts indépendants les uns des autres. L'objectif est de minimiser la date de fin de la derniére tâche (le makespan) de l'ensemble de workflows. Pour résoudre ce probléme nous proposons une approche génétique. Nous apportons une contributions à la fois dans la conception d'un algorithme génétique prenant les coûts de communication en compte et dans les analyses des performances.

Mots-clés : Ordonnancement de lots, grille de calcul, plateforme hétérogène, algorithme génétique Laboratoire d'Informatique de l'Université de Franche-Comté, UFR Sciences et Techniques, 16, route de Gray, 25030 Besanc ¸on Cedex (France)

Introduction

Nowadays, to go further in their research, scientists often need to connect several applications together. That is why for few years, workflow systems have been designed to provide tools that support their multi-application simulations. In the e-Science [START_REF]Workflows for e-Science[END_REF] many fields use workflow applications: medical image processing [START_REF] Kumar | Large image correction and warping in a cluster environment[END_REF], geosciences [START_REF] Deelman | Managing Large-Scale Workflow Execution from Resource Provisioning to Provenance Tracking: The CyberShake Example[END_REF], astronomy [START_REF] Schaaff | Workflow in astronomy : the vo france workflow working group experience[END_REF].

A workflow is a set of applications which are connected to each other by precedence constraints. An input data set enters the workflow, it is processed by an application which computes an output data set. This result data set is sent to the next application as defined by the structure of the workflow. Generally a workflow has the structure of a DAG (Direct Acyclic Graph): a graph whose nodes are the tasks and whose edges are the precedence constraints.

When the size of the data entering the workflow increases the processing time may become very long and it becomes mandatory to use larger computing resources as grids. Because of their heterogeneity -the platforms have hosts with different calculation and memory capacities -they are difficult to use for non computer scientists but several research projects have already tackled this problem. The Pegasus framework [START_REF] Deelman | Pegasus: a framework for mapping complex scientific workflows onto distributed systems[END_REF] proposes a convenient way for scientists to compute their workflows onto heterogeneous platforms without learning distributed programming concepts. Other tools, like DIET [START_REF] Caron | Diet: A scalable toolbox to build network enabled servers on the grid[END_REF] or NINF-G [START_REF] Tanaka | Design, implementation and performance evaluation of gridrpc programming middleware for a large-scale computational grid[END_REF], provide a SOA-Grid (Service Oriented Architecture) that facilitates user accesses to remotely accessible computing applications and make the execution of workflows on a heterogeneous platform easier. When the number of workflows to be executed in parallel is huge, it is however mandatory to efficiently map them onto the resources of a heterogeneous platform.

Minimizing the execution time of a workflow or a set of workflows onto a heterogeneous platform is an optimization problem that is known to be NP-Hard. We can just rely on heuristics to find a solution as good as possible. The quality of the heuristic solution is based on the performance obtained in the scheduling of different workflows. Genetic Algorithms (GA) are known to give good results in several optimization domains. GA have already been used in the scheduling of workflows [START_REF] Daoud | GATS 1.0: A Novel GA-based Scheduling Algorithm for Task Scheduling on Heterogeneous Processor Nets[END_REF][START_REF] Goh | A hybrid evolutionary approach for heterogeneous multiprocessor scheduling[END_REF]. With these algorithms it is however not possible to give an approximation and a static study of the algorithm may be worth it. The performance evaluation must be done by simulating the algorithm behavior in a large number of cases.

The general problem we deal with is to schedule a set of workflows (jobs) onto a SOA-grid. Each task of a workflow has a type that corresponds to a service type or to an application type in the SOA-Grid. We consider the two cases: (1) the general case when the structure of each workflow differs from one another; (2) the particular case when the structure of the workflow is the same for all the jobs. In this paper we focus on researches that we carried out on the design of a Genetic Algorithm and we assess its performance to schedule a set of workflows. The contributions of this paper are both the design of a Genetic Algorithm taking the communication costs into account and the performance analysis. In the general case (1) we compare the performance obtained by a GA approach to the performance obtained by a list-based scheduling algorithm. In the particular case (2) of the scheduling of a collection of identical workflows which structure is limited to intrees, we compare our results to a lower bound and we show that our Genetic Algorithm approach allows us to get a schedule with good performance.

The paper is organized as follows. In section 2 we detail the framework which defines both the grid and the workflow models. Section 3 is devoted to an overview of the related work. We present in section 4 a Genetic Algorithm that takes communication costs into account to deal with our problem. Section 6 introduces the simulation setup, the results of the simulations and their analysis for workflows of different shape. Section 7 presents the simulations for workflows with identical structure. Finally, we conclude in section 8.

Framework

Scheduling a set of workflows on a SOA-grid amounts to schedule each task of each workflow onto a grid host that provides the application corresponding to its task type. In this section we outline the applicative framework, the targeted platform and the communication model.

Applicative framework

In our study, the problem that we have to solve deals with the scheduling of a collection B = {J j , 1 ≤ j ≤ N } of N workflows. Each workflow J j is represented by the graph (DAG) J j = (T j , D j ) where T j = {T j 1 , . . . , T j n j } is the set of its tasks and D j represents the precedence constraints between the tasks of the workflow. Let T = ∪ N j=1 T j = {T j i j , 1 ≤ i j ≤ n j and 1 ≤ j ≤ N } be the set of tasks to schedule. Figure 1 gives an example of a workflow J 1 that consists of three tasks T 1 1 , T 1 2 and T 1 3 which types are respectively A, D and B. Each edge of J 1 indicates a precedence constraint and its associated value is the amount of data that has to be exchanged. These precedence constraints actually represent file transfers between applications. These transfers, that may be costly, implies that communication costs must be taken into account in the schedule. As we mention above we distinguish the two following cases: scheduling identical workflows or scheduling different workflows.

Targeted platform

The targeted platform is a heterogeneous platform of n machines modeled by an undirected graph PF = (P, L) where P = {p 1 , . . . , p n } is the set of vertices which represents the machines and where L is the set of bidirectional communication links between machines (∀ 1 ≤ i, j ≤ n and i = j then (p i , p j ) ∈ L). Let τ be the set of all the task types available onto the platform. Each machine p i is able to perform a subset of τ . If the type t ∈ τ is available on the machine p i , w(t, p i ) is the time to perform a task of type t on p i . Moreover, each link (p i , p j ) has a bandwidth bw(p i , p j ) which is the number of data per time unit that can be transferred through that link. 2 gives an example of a platform where the letters A, B, C and D represent the task types that can be performed onto the nodes. The number above the link is the bandwidth. Figure 3 gives an example of the capabilities of each machine to perform each task type. The values correspond to the number of time units necessary to carry out the corresponding task type onto a given processor. When the value is infinity, the machine cannot perform the task type. For instance, processor p 1 can perform both the functions A and C but cannot perform neither B nor D.

p 1 p 2 p 3 p 4 Type A 20 ∞ ∞ 15 B ∞ 10 5 ∞ C 10 10 ∞ ∞ D ∞ ∞ 10 10

Communication model

In our study processors are interconnected by communication links in a pointto-point fashion to model a computation grid. In the literature [START_REF] Beaumont | Assessing the impact and limits of steady-state scheduling for mixed task and data parallelism on heterogeneous platforms[END_REF][START_REF] Casanova | Modeling large-scale platforms for the analysis and the simulation of scheduling strategies[END_REF], several communication models exist such as the one-port model or the all-port model. We choose to use the one-port model because of its ease of modeling and of implementation while still being realistic. In this model only one data can be transmitted at the same time over a communication link and a node can do at most one reception and one transmission at the same time.

Related work

Scheduling problems have extensively been studied in the literature and minimizing the makespan (maximum completion time) of a DAG execution on a distributed homogeneous platform with limited resources, i.e., a limited number of processors, is known to be a NP-Complete problem [START_REF] Lenstra | Complexity of scheduling under precedence constraints[END_REF]. As a consequence, the problem considered here is also NP-Complete since the heterogeneity of the resources makes the problem more complex. So there is no direct method that can find an optimal solution in polynomial time and the schedule decisions must rely on heuristic solutions.

Classical solution scheduling algorithms often rely on list-based scheduling algorithms. They use heuristics such as Heterogeneous Earliest Finish Time (HEFT) [START_REF] Topcuouglu | Performance-effective and lowcomplexity task scheduling for heterogeneous computing[END_REF] or Critical Path [START_REF] Kwok | Dynamic critical-path scheduling: An effective technique for allocating task graphs to multi-processors[END_REF]. In a homogeneous context, [START_REF] Kwok | Static Scheduling Algorithms for Allocating Task Graphs to Multiprocessors[END_REF] gives a survey on the DAG scheduling topic. Moreover the more complete study [START_REF] Braun | A comparison of eleven static heuristics for mapping a class of independent tasks onto heterogeneous distributed computing systems[END_REF] evaluates eleven heuristics, such as Min-min, Max-min or Sufferage, three heuristics based on the Minimum Completion Time (MCT). These results obtained onto homogeneous platforms give hints to schedule DAGs onto heterogeneous platforms but have not been validated for Heterogeneous Computing.

Makespan oriented strategies to schedule workflows onto the grid are presented in [START_REF] Mandal | Scheduling strategies for mapping application workflows onto the grid[END_REF], with the description of real life medical applications, or in [START_REF] Caniou | Ocean-Atmosphere Modelization over the Grid[END_REF] for Ocean-Atmosphere modeling. In [25], the problem of scheduling a set of LIFC different DAGs is studied. These approaches compute an off-line schedule considering the whole set of tasks. But, when the number of tasks scales up, the computation time becomes too long because of the complexity of the algorithm.

M. Daoud and N. Kharma present in [START_REF] Daoud | GATS 1.0: A Novel GA-based Scheduling Algorithm for Task Scheduling on Heterogeneous Processor Nets[END_REF] a makespan oriented genetic based algorithm (GA) for tasks scheduling. It has been designed for scheduling tasks of one workflow onto a heterogeneous platform but without taking communication costs into account. C. Goh et al. use in [START_REF] Goh | A hybrid evolutionary approach for heterogeneous multiprocessor scheduling[END_REF] the same genome coding but communications are not handled too.

Other studies tackle workflow scheduling onto heterogeneous platforms but with other objective functions than the makespan. The results presented in [START_REF] Benoit | Computing the throughput of replicated workflows on heterogeneous platforms[END_REF] use Timed Petri Nets and pipelines to optimize the throughput of replicated workflows onto heterogeneous platforms. The steady-state technique presented in [START_REF] Beaumont | Assessing the impact and limits of steady-state scheduling for mixed task and data parallelism on heterogeneous platforms[END_REF] provides an optimal algorithm to schedule a set of identical workflows also for the throughput objective function. Other optimization criteria are studied in the literature, such as the latency [24], or even performance-related criteria together with energy consumption [START_REF] Benoit | Performance and energy optimization of concurrent pipelined applications[END_REF].

GA with communication costs

For the execution we use the same genome representation as in [START_REF] Daoud | GATS 1.0: A Novel GA-based Scheduling Algorithm for Task Scheduling on Heterogeneous Processor Nets[END_REF][START_REF] Goh | A hybrid evolutionary approach for heterogeneous multiprocessor scheduling[END_REF], i.e., a chromosome is a two-dimension table with one row per node where the tasks assigned to the node are recorded. Some improvements to take SOA-Grids and collections into account, presented in [START_REF] Diakité | Comparison of batch scheduling for identical multi-tasks jobs on heterogeneous platforms[END_REF], are added. As these GA coding does not however take communication costs into account, we study their integration in this section.

Communication integration

The main problem we faced is the step of the genetic algorithm where we should integrate the communications.

At first we have worked on inserting communications into the chromosomes, as for executions. We have introduced the notion of "communication task ", between each couple of dependent tasks in the task graph. Then we map them onto the communication links. When integrating "communication tasks" in the chromosomes, there are however issues regarding the crossover procedure. Let us imagine two schedules for one application onto one platform. In each schedule a task is allocated to one node, and its output (a communication) is allocated to a route composed of connected communication links. Now, if we make a crossover with these two schedules, and if we apply the crossover technique on communication tasks with their allocated links, we potentially generate a lot of inconsistent communication routes and we thus produce numerous non feasible schedules. This makes a huge waste in term of computation time.

A more convenient way to introduce communications is at the fitness evaluation step of the genetic algorithm. Indeed the allocations of the communication tasks depend on the allocations of the computation tasks since the possible routes between two nodes are limited. Choosing a good mapping for the computation tasks intuitively involves finding a valid allocation for the communication tasks. So we propose to use the chromosomes only for mapping computation tasks onto the nodes, and in a second step to look for a valid route to send the data according to this mapping and the precedence constraints between the tasks. Then the fitness of each individual can be evaluated by taking both the computations and the communications into account, each individual being valid (see algorithm 1).

Impact of the communication model

Choosing the network links for each communication is complex. Always using the shortest, or fastest, path may lead to a high contention so that we need to take the network load into account. We assess here four communication policies.

Figures 4a and4b show the efficiencies of the GA different communication integrations. This notion of efficiency will be introduced in section 7.1, however, it is necessary to know only that the higher the curve is, the higher the performance of the algorithm is.

• "GA-without-comm" : an arbitrary static route is given for each couple of computation nodes. Chromosome fitness are evaluated without regarding the communication cost.

• "GA 1-port-comm-static-route" : the same the previous policy but with regarding communication costs in the fitness evaluation using the 1-port model.

• "GA 1-route-Bellman-Ford" : the static route for each couple of computation nodes is the fastest one by using the Bellman-Ford algorithm.

• "GA 3-routes-Bellman-Ford" : for each couple of computation nodes, during the evaluation fitness step, the 3 first best routes are tested.

LIFC Algorithm 1: Scheduling tasks according the chromosome ch Input : B: the N DAGs to schedule a(i, j): p a(i,j) is the machine on which T j i is assigned PF = (P, L): the targeted platform R(p k , p i ) = {(p j , p j ) ∈ L}: a route from p k to p i t(i, j): the type of the task T j i w(t(i, j), u): the time to perform T j i onto p u Output: f (ch): the fitness associated to the chromosome ch Data: T = {T j ij , 1 ≤ i j ≤ n j and 1 ≤ j ≤ N }: the set of tasks to schedule T T oSched : the set of remaining tasks to schedule C(T j i ): the completion time of T j i σ(T j i ): the time to start T j i onto p a(i,j) δ(p u ): the next time where p u is idle F j k,i : the file to send between T j k and T j i when (T j k , T j i ) ∈ D j CF (F j k,i ): the time to send F j k,i along the route R(p a(k,j) , p a(i,j) ) T T oSched ← T while T T oSched = ∅ do choose a free task

T j i ∈ T T oSched (EFT heuristic) T pred ← {T j k |(T j k , T j i ) ∈ D j } σ(T j i ) ← 0 foreach task T j k ∈ T pred do σ(T j i ) ← max(σ(T j i ), C(T j k ) + CF (F j k,i )) σ(T j i ) ← max(δ(p a(i,j) ), σ(T j i )) C(T j i ) ← σ(T j i ) + w(t(i, j), a(i, j)) δ(p a(i,j) ) ← C(T j i ) The task T j i is scheduled at the time σ(T j i ) onto p a(i,j) T T oSched ← T T oSched \ {T j i } return f (ch) = C max = max T j i ∈T (C(T k i ))
RR 2011-01

Simulation setup

To assess the performance of the scheduling algorithm we need to implement it on a heterogeneous platform. The context is indeed too complex to be studied with a formal approach and, to get realistic results, the platforms used must integrate the network contention. On the other hand, the implementation on a computation grid can however not give reproducible results as the experimental conditions, as the network load, may change. So, we use a grid simulator to evaluate the performance of the Genetic Algorithm. The simulator is implemented using SimGrid and its MSG API [START_REF] Casanova | Simgrid: A generic framework for large-scale distributed experiments[END_REF].

All the simulations have been made using batch sizes from 1 to 10 000. The platforms and the applications are randomly generated with a uniform distribution. Platforms have between 4 and 10 nodes and are strongly connected. Applications have between 4 and 12 tasks. For the case where workflows are different from each other, presented in 6, 200 platforms and 10 000 DAGs are randomly generated. For each couple (platform, batch size) different applications are randomly chosen among the 10 000. So we generate 1 900 simulations of platform/application scenarios. In the case where workflows are identical, we use 10 platforms and 10 applications, so 100 scenarios for each batch size.

We define the "computation to communication ratio" (CCR) of a simulation as the average computation time divided by the average communication time. To assess the impact of the communications on the algorithm performance, we run simulations with different CCR, from 1/1 000, i.e., communication time is predominant, to 1 000, i.e., communication time is negligible. The speed of the nodes are unrelated. We also assess the impact of the platform heterogeneity on the performance: execution and communication times fluctuate respectively in a range from 1 to 10 and 1 to 4.

For the GA, the population is set to 200 individuals and a generation is set to 100 iterations.

Results with general DAGs

As no optimal value can be computed in a polynomial time for the global execution time of a collection of workflows, we must compare the performance of the GA to another algorithm. So the metric that we use is the makespan improvement relative to a standard list-based scheduling algorithm (LIST). Figure 5 shows the improvement of the makespan when scheduling a set of different workflows on a heterogeneous platform. Each curve shows the percentage of GA experiences whose makespan is improved respectively by more than 0%, 10%, 20% and 30% when compared to the use of the listbased scheduling algorithm (LIST). We notice that more than 80% of the GA experiments have a makespan improved by more than 10%. The 0%curve shows that GA gives an improvement in about 100% of cases. Figure 6 shows the improvement of the makespan when scheduling a set of identical workflows. We can notice that GA gives less important im-LIFC provements relative to LIST in this case. For each 0, 10, 20 and 30 %-curve, GA improvements decrease by about 10% compared to experiments obtained when scheduling different workflows. We can also note that 10% to 20% of the GA schedules are less efficient than the LIST schedules in this case. GA improvements remain however high.

In general, more than 70% of the GA experiments give a makespan with an improvement greater than 10% for almost any size of sets of workflows. The diversity of the workflows promotes the GA algorithm: as GA tries randomly a lot of combinations it can benefit from different workflows while LIST which is directed by greedy choices, cannot.

Results for a set of identical intrees

Comparing two algorithms gives relative information but no absolute information on the quality of the algorithm. For the particular case of batches of intrees it is possible to compute an optimal throughput by using a steadystate algorithm [START_REF] Beaumont | Assessing the impact and limits of steady-state scheduling for mixed task and data parallelism on heterogeneous platforms[END_REF]. In this section we assess how far the GA is from the optimal, so its absolute efficiency, and we compare it to the list scheduling and to the a practical makespan oriented implementation of this algorithm [START_REF] Diakité | Steady-state for batches of identical task graphs[END_REF].

Note that this study is limited to the particular case where the applications are intrees.

Efficiency

Using linear programming the optimal throughput can be computed thanks to the steady-state algorithm. This optimal throughput is used to compute a lower bound for the optimal makespan makespan o which the number N of jobs to process divided by the steady-state throughput (ρ). To evaluate the GA performance, we introduce the notion of efficiency as the ratio between this lower bound makespan o over the makespan of the schedule given by GA makespan r . That is to say if a schedule gives makespan r = makespan o then efficiency = 1.0 and it means that this schedule is optimal. The nearer efficiency is from 1.0, the more efficient the scheduling algorithm is.

efficiency = makespan o makespan r with makespan o ≥ N ρ
So, efficiency ≥ N ρ × makespan r Since we run 100 simulations, for each of the 19 sizes of job sets, we cannot get a simple scalar efficiency value for the overall experiments. A mean value would indeed be not meaningful as the longer simulations will weight more than the sorter ones in this metric. So we introduce an efficiency threshold t for the different sizes of batches SIZES and we compute the percentage of experiments that gives an efficiency greater than t for each size of batches.

In the following we present the distribution of the results depending on this percentage on 3D curves. Two lines are thickened on the surfaces to highlight the efficiency curves for threshold values 0.8 and 0.9.

Fully heterogeneous platforms

In this section we compare the performance of GA, LIST and steady-state to schedule intrees on heterogeneous platforms. 7b show the distribution of the percentage of experiments which give schedules greater than a threshold and for a batch size. The used platforms are fully heterogeneous and CCR ≈ 1 000. For both the algorithms the efficiency increases with the number of jobs. We can notice that for batch sizes greater than 100 almost 100% of GA experiments reach an efficiency greater than 0.8. There is an 100% horizontal line for GA experiments for threshold 0.8 and batch sizes from 100 to 10 000, while for LIST there is a rising curve. It means that GA efficiency increases faster than LIST when batch sizes are large.

Figures 8a and8c show that for batch sizes greater than 100 more than 70% of GA experiments have an efficiency greater than 0.8, while LIST reaches hardly 60%. However for the threshold 0.9 the two experiments have almost the same behavior. On the other hand, the steady-state algorithm gives better results with almost 90% of the simulations that reach an efficiency of 0.8. The GA is however not so far from this curve.

Fully homogeneous platforms

In this section we assess the performance of GA for scheduling intrees on homogeneous platforms.

CCR ≈ 1 000

On the figures 9a, 9b and 9c we see the percentage of experiments which give schedules with efficiencies greater than 0.9 and 0.8 when the platforms have heterogeneous nodes and heterogeneous communication links. For the threshold 0.9, GA is even better than both the Steady-State and the LIST algorithms for batch sizes less than 1 000. For batch sizes greater than 1 000, GA is overtaken. However if threshold 0.8 is taken, GA shows the highest curve.

CCR ≈ 1

With the figures 10a, 10b and 10c we see the percentage of experiments which give schedules with efficiencies greater than 0.9 and 0.8 when the platforms have homogeneous nodes and homogeneous communication links. For the threshold 0.9, GA is even better than both the Steady-State and the LIST algorithms for batch sizes less than 2 500. For batch sizes greater than 2 500, GA is overtaken. However if threshold 0.8 is taken, GA shows the highest curve up to 5 000 jobs. Figure 10a shows that LIST has very poor results even for several thresholds.

Computation times

The figure 11 shows the time spent by the three algorithms to find a schedule for platforms with heterogeneous bandwidths and whose computation costs are 10 times greater than communication costs. The GA and LIST are very time consuming while the computation time spent by the Steady-State algorithm is very low. Nevertheless GA has the best performance in most seen cases for batch sizes less than 1 000. For these sizes the GA computation times is less than 20 minutes only.

The simulations have been run on a cluster with 64 nodes, each node being a 2.8 GHz quad-core Intel Xeon bi-processor. Each simulation runs on one core.

Conclusion and future work

In this paper, we propose a genetic algorithm that solves the problem of scheduling a collection of workflows on a set of heterogeneous nodes inter- connected by heterogeneous communication links. This GA takes the communication costs into account. We show that for a collection of different workflows GA obtains better execution performance than a classical LIST algorithm. For the case where the DAGs are identical intrees we are able to compare the GA results to an optimal lower bound and to show that its results tend towards the optimality for more than 1 000 jobs. The obtained results are moreover comparable to a practical implementation of the Steady-State algorithm. The main idea we keep in mind is that scheduling with GA by taking communications into account is difficult, as for implementing the practical Steady-State solution.

For future work, other communication models should be implemented in the simulator, like the multi-port models and other genetic representations could be explored. [25] H. Zhao and R. Sakellariou. Scheduling multiple DAGs onto heterogeneous systems. In HCW06, Rhodes, Greece, 2006.

LIFC

LIFC

Figure 1 :

 1 Figure 1: Example of a workflow J 1

Figure 2 :

 2 Figure 2: An example of a platform

Figure

  Figure 2 gives an example of a platform where the letters A, B, C and D represent the task types that can be performed onto the nodes. The number above the link is the bandwidth. Figure3gives an example of the capabilities of each machine to perform each task type. The values correspond to the number of time units necessary to carry out the corresponding task type onto a given processor. When the value is infinity, the machine cannot perform the task type. For instance, processor p 1 can perform both the functions A and C but cannot perform neither B nor D.

Figure 3 :

 3 Figure 3: Execution platform performance.

Figure 4 : 10 LIFC

 410 Figure 4: Communication integrations with an efficiency above 0.9 and 0.8, CCR ≈ 10

Figure 5 :

 5 Figure 5: Improvement for batches of different DAGs, fully heterogeneous platforms, CCR ≈ 1

Figure 6 :

 6 Figure 6: Improvement for batches of identical general DAGs, fully heterogeneous platforms, CCR ≈ 1

Figure 7 :

 7 Figure 7: CCR ≈ 1000, fully heterogeneous platforms

Figure 8 :

 8 Figure 8: Simulation with fully heterogeneous platforms, CCR ≈ 1

Figure 9 :

 9 Figure 9: Simulation with fully homogeneous platforms, CCR ≈ 1000

Figure 10 :

 10 Figure 10: Simulation with fully homogeneous platforms, CCR ≈ 1

Figure 11 :

 11 Figure 11: Average Computation time

[

  24] N. Vydyanathan, U.-V. Catalyurek, T.-M. Kurc, P. Sadayappan, and J.-H. Saltz. Toward optimizing latency under throughput constraints for application workflows on clusters. In Springer, editor, Euro-Par 2007 Parallel Processing, volume 4641 of Lecture Notes in Computer Science, pages 173-183, 2007.

Téléphone : +33 (0)3 81 66 64 55 -Télécopie : +33 (0)3 81 66 64 50

RR 2011-01

Acknowledgment

The huge amount of simulations have been run on the cluster of the Mésocentre de Calcul de Franche-Comté in Besançon, France.


Pierre-Christophe Bué

Jacques Julliand
email: julliand@lifc.univ-fcomte.fr

Pierre-Alain Masson
email: masson@lifc.univ-fcomte.fr

Association of Under-Approximation Techniques for Generating Tests From Models

Keywords: Model-Based Testing, Abstraction, Over and under-approximations

In this paper we present a Model-Based Testing approach with which we generate tests from an abstraction of a source behavioural model. We show a new algorithm that computes the abstraction as an under-approximation of the source model. Our first contribution is to combine two previous approaches proposed by Ball and Pasareanu et al. to compute May, Must+ and Must-abstract transition relations. Proof techniques are used to compute these transition relations. The tests obtained by covering the abstract transitions have to be instantiated from the source model. So, following Pasareanu et al., our algorithm additionally computes a concrete transition relation: the tests obtained as sequences of concrete transitions need not be instantiated from the source model. Another contribution is to propose a choice of relevant parameters and heuristics to pilot the tests computation. We experiment our approach and compare it with a previous approach of ours to compute tests from an abstraction that over-approximates the source model.

Motivations

The process of software testing can be automated by means of a Model-Based Testing (MBT) approach [START_REF] Utting | Practical Model-Based Testing[END_REF]. A formal behavioural model is designed from which a set of tests is computed that ensure a given coverage of the model. An adaptation layer fills the gap between the model and the implementation to produce executable tests. The conformance of the implementation to the model is assessed by comparing, modulo the adaptation layer, the outputs of the executable tests with the ones as predicted by the model. A frequent limit to the scalability of this approach is the size of the state space defined by the model: it can be infinite or very large, thus making its coverage impossible in practice.

An abstraction of the behavioural model can be used to overcome this limitation. Abstraction techniques [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF][START_REF] Cousot | Abstract interpretation frameworks[END_REF][START_REF] Pȃsȃreanu | A survey of new trends in symbolic execution for software testing and analysis[END_REF] allow for making finite or drastically reducing the state space representation of a formal specification (or of a program), for example by gathering into one single abstract state several concrete states. Our framework is that of predicate abstraction [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF][START_REF] Cousot | Abstract interpretation frameworks[END_REF], where the states and the transition relation of the abstraction are defined according to a set of predicates over the model variables.

Once computed from the abstraction, the tests have to be instantiated on the concrete model. This may not be possible for some of the tests if the abstraction is an over-approximation of the source model, thus defining execution paths that may not exist concretely. We have previously defined and presented in [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF] a method where this could happen. The abstraction was computed by a theorem-prover that tried to prove the potential feasibility of the transitions rather than their reachability. As a result, time could be spent uselessly to search for an instantiation that does not exist. We adopt another approach in this paper by considering only under-approximations. Since all the paths of an underapproximation exist in the concrete model, it is possible to instantiate every test from it on the concrete model.

We present in this paper a new algorithm, based on previous works from Ball [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF] and Pȃsȃreanu et al. [START_REF] Pȃsȃreanu | Predicate abstraction with underapproximation refinement[END_REF], to compute abstract transition relations based on predicate abstraction for test generation. Our algorithm combines the two approaches of Ball and Pȃsȃreanu et al., and applies to behavioural models instead of programs. We use SAT-solving techniques to compute the transition relations. We also compute a concrete transition relation and try to directly connect concrete states to each other, so as to obtain concrete tests that need not be instantiated from the model. This complements the tests obtained by covering the abstract transition relation, for which an instantiation is required.

But what part of the behavioural model will be covered by tests computed from an under-approximation of it? We have implemented the algorithm, and used it to compute tests for six case studies. These experimental results are compared in terms of coverage of the abstraction with the ones obtained by our over-approximation method of [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF]. We consider a set of optimisations of the concretisation computed by the algorithm, and evaluate experimentally their practical impact on our case studies. We also provide a set of parameters to the user as well as heuristics to improve the method.

The paper is organised as follows. Section 2 presents the process for generating tests from an abstraction. The background required for reading the paper is given in Sec. [START_REF] Cousot | Abstract interpretation frameworks[END_REF]. Two examples to illustrate our approach are described in Sec. [START_REF] Pȃsȃreanu | A survey of new trends in symbolic execution for software testing and analysis[END_REF]. The algorithm for computing the abstraction as well as its properties are described in Sec. 5. Section 6 presents the experimental results. We present in Sec. 7 the works to which ours are related. We conclude and indicate future research directions in Sec. 8.

Test Generation Process from an Abstraction

In a previous work [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF], we have presented a test generation method based on abstraction. The abstraction was computed as an over-approximation of a formal behavioural model M of the system, written by a validation engineer. The engineer also wrote a test purpose, by means of a language proposed in [START_REF] Julliand | Generating security tests in addition to functional tests[END_REF], to describe how he intended to test the system, according to his know-how. A set of abstraction predicates was automatically deduced from the test purpose, from which the abstraction was computed. The tests issued from the over-approximation had to be instantiated afterwards on M, which was not always possible since an overapproximation defines more executions than the concrete model. We improve in this paper the test generation method of [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF] by computing an abstraction that is an under-approximation of M rather than an over-approximation. This guarantees that every test generated from it can be instantiated on M. Also, we now instantiate the tests on-the-fly, and not a posteriori as was done in [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF].

We sketch our process in Fig. 1. Notice that the abstraction predicates on input of the "Predicate Abstraction and Concretisation" box could be obtained from a test purpose, identically to what was proposed in [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF]. We also could synchronise such a test purpose with M before the abstraction computation, to reduce the state space of the resulting abstraction. But we adopt in this paper a more generic presentation of our process. We combine predicate abstraction and SAT-solving for generating the under-approximation. The tests are generated from it by applying a selection criterion that ensures a coverage of the states, of the transitions or of the paths of the abstraction. In our implementation of the process, we have used a chinese postman algorithm to compute tests by covering all the transitions of the abstraction. The tests obtained are valid executions of M, intended to be executed, via the adaptation layer, on the implementation of the system.

Set of Abstraction Predicates

Behavioural

Model M

Predicate Abstraction and Concretisation

Underapproximation A

Test Generation

Structural

Background

Our behavioural models are described as B event systems, for which we provide the necessary background. We also present the concept of predicate abstraction and formalise the abstraction notions by means of Symbolic labelled Transition Systems (STS), that define the semantics of the abstractions of event systems.

Model Syntax

Introduced by J.-R. Abrial [START_REF] Abrial | Modeling in Event-b: System and Software Design[END_REF], a B event system defines a closed specification of a system by a set of events. This syntax is used as an example to present the results in this paper. But these results are generic in the sense that this syntax is a concise form that has the same expressivity as some generic modelling languages as the guarded actions of [START_REF] Dijkstra | Guarded commands, nondeterminacy, and formal derivation of programs[END_REF][START_REF] Dijkstra | A Discipline of Programming[END_REF] or the labelled transition systems. In the sequel, we use the following notations: x, y, z are variables and X, Y , Z are sets of variables. I is an invariant and P is used to denote other predicates. The actions of modification of the variables are called substitutions in B, following [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] where the semantics of an assignment is defined as a substitution. In B, substitutions are generalized, i.e. the semantics of every kind of action is defined by a substitution calculus that allows to compute the weakest precondition of a substitution a to satisfy the predicate P , denoted [a]P in B. We use a, a 1 and a 2 to denote B generalized substitutions, and E and F to denote B expressions.

All the substitutions allowed in B event systems can be rewritten by means of the five B primitive forms of Def. 1. Notice that the multiple assignment can be generalized to n variables and that all the substitutions terminate.

Definition 1 (Substitution). The following five substitutions are primitive:

-single and multiple assignments, denoted as x := E and x, y := E, F -substitution with no effect, denoted as skip -guarded substitution, denoted as P ⇒ a -bounded non-deterministic choice, denoted as a 1 []a 2 -substitution with local variable z, denoted as @z.a.

The substitution with local variable is mainly used to express the unbounded non-deterministic choice denoted by @z.(P ⇒ a). Let us specify that among the usual structures of specification languages, the conditional substitution IF P THEN a 1 ELSE a 2 END is denoted by (P ⇒ a 1 )[](¬P ⇒ a 2 ) with the primitive forms.

Definition 2 defines correct B event systems. The events are defined by an equation e = a where e is the name of an event and a is a generalized substitutions modifying the state variables.

Definition 2 (Correct Event System). A correct B event system is a tuple X, I, Init, EvDef where:

-X is a set of state variables, -I is an invariant predicate over X, -Init is a substitution called initialisation, such that the invariant holds in any initial state, i.e.

[Init]I is valid, -EvDef is a set of event definitions in the shape of e = a such that every event preserves the invariant, i.e. I ⇒ [a]I is valid.

Predicate Abstraction

Predicate abstraction [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF] is a special instance of the framework of abstract interpretation [START_REF] Cousot | Abstract interpretation frameworks[END_REF] that maps the potentially infinite state space C of a transition system onto the finite state space Q of a symbolic transition system via a set of predicates P = {p 1 , p 2 , . . . , p n } over the model variables. A state of C is a valuation of the state variables of the model. The set of abstract states Q contains at most 2 n states. Each state is a tuple q = (q 1 , q 2 , . . . , q n ) with q i being equal either to p i or to ¬p i , and we also consider q as the predicate n i=1 q i . We define an abstraction function α P : C → Q such that α P (c) is an abstract state q where c satisfies q i for all i ∈ 1..n. By a misuse of language, we say that c is in q.

The predicate abstraction is based on five primitive functions denoted as follows. We denote by wp(a, q ′ ) the weakest precondition [START_REF] Dijkstra | A Discipline of Programming[END_REF] of an action a to reach a target state defined by a predicate q ′ . The weakest precondition wp(a, q ′ ) is the largest set of states from which the execution of a necessary leads to a state that satisfies q ′ . In B, wp(a, q ′ ) can be computed by substitution calculus, denoted by [a]q ′ . The weakest conjugate precondition [START_REF] Bert | Construction of finite labelled transistion systems from b abstract systems[END_REF], denoted by wcp(a, q ′ ) is equal to ¬[a]¬q ′ in B, i.e. ¬wp(a, ¬q ′ ). The conjugate weakest precondition wcp(a, q ′ ) is the largest set of states from which the execution of a can lead in a state that satisfies q ′ . Since the events always terminate in B, wcp is identical to wp for the deterministic subset of B. In contrast, for a non deterministic substitution, wp(a, q ′ ) ⇒ wcp(a, q ′ ) because there may exist states for which a non deterministic choice leads to q ′ or not, depending on the chosen branch. These states satisfy wcp(a, q ′ ) but not wp(a, q ′ ). We denote by sp(a, q) the strongest postcondition of an action a from a source state defined by a predicate q. It is the smallest set of states reached by the execution of a from a state that satisfies q. We denote by grd(a) the condition under which the action a is triggerable. It is defined as in B: grd(skip) = true, grd(x, y := E, F ) = true, grd(P ⇒ a) = P ∧ grd(a), grd(a 1 []a 2 ) = grd(a 1 ) ∨ grd(a 2 ), grd(@z.a) = ∃z.grd(a). Last, we denote by SAT (P ) the satisfiability value of a predicate P .

Let us now define the abstract transitions as may-transitions. Consider two abstract states q and q ′ and an event e. There exists a may transition from q to q ′ by e, denoted by q e → q ′ , if and only if there exists a concrete transition c e → c ′ where c and c ′ are concrete states with α P (c) = q and α P (c ′ ) = q ′ . If we assume the event e to be defined by an action a, there is a may transition q e → q ′ iff SAT (wcp(a, q ′ ) ∧ q).

As in [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF], we define two other kinds of abstract transitions: must-and must+. The must+ transitions are may transitions that are triggerable from all the concrete states of the abstract source state. The must-transitions are may transitions that reach all the concrete states of the abstract target state. Let e = a be an event definition. There exists a must+ transition q e → q ′ iff q ⇒ wp(a, q ′ ) ∧ grd(a) is valid, i.e. ¬SAT (¬(wp(a, q ′ ) ∧ grd(a)) ∧ q). That is, for any state c concretising the abstract state q, there is a concrete state c ′ in q ′ such that c e → c ′ . There exists a must-transition q e → q ′ iff q ′ ⇒ sp(a, q) is valid, i.e. ¬SAT (¬sp(a, q) ∧ q ′ ). That is for any concrete state c ′ for which α P (c ′ ) = q ′ , there is a concrete state c for which α P (c) = q and such that c e → c ′ .

Abstraction Formalisation

We define in Def. 3 a kind of STS well suited to represent abstractions. Definition 4 associates an abstraction defined by an STS to an event system. Definition 3 (Symbolic Labelled Transition System (STS)). Let Ev be a finite set of event names. Let A be a finite set of symbolic states on P. Let C be a finite or infinite set of concrete state and α P an abstraction function from

C to A. A tuple Q, Q 0 , C 0 , ∆, ∆ + , ∆ -, Γ, ∆ c is an STS if it satisfies the following conditions: -Q(⊆ A) is a finite set of states, -Q 0 (⊆ Q) is a set of abstract initial states, -C 0 (⊆ C) is a set of concrete initial states, -∆(⊆ Q × Ev × Q) is a may labelled transition relation, -∆ + (⊆ Q×Ev ×Q) is a must+ labelled transition relation such that ∆ + ⊆ ∆, -∆ -(⊆ Q × Ev × Q) is a must-labelled transition relation such that ∆ -⊆ ∆, -Γ (⊆ Q × C) is a concretisation relation that associates concrete states to any abstract state such that (q, c) ∈ Γ ⇒ α P (c) = q, -∆ c (⊆ C × Ev × C) is a concrete transition relation such that c e → c ′ ∈ ∆ c iff c ∈ C ∧ c ′ ∈ C ∧ q e → q ′ ∈ ∆ ∧ (q, c) ∈ Γ ∧ (q ′ , c ′ ) ∈ Γ .
Definition 4 (STS associated to an ES). Let ES = X, Init, {e = a|e ∈ Ev} be an event system and P = {p 1 , p 2 , ..., p n } be a set of n predicates defining a set of 2 n abstract states

A = {p 1 , ¬p 1 } × {p 2 , ¬p 2 } × ... × {p n , ¬p n }. A tuple Q, Q 0 , C 0 , ∆, ∆ + , ∆ -, Γ, ∆ c
is an STS associated to ES and P if it satisfies the following conditions:

-Q 0 = {q|q ∈ A ∧ SAT (sp(Init, true) ∧ q)} , -C 0 = {c|∃q 0 .(q 0 ∈ Q 0 ∧ c ∈ C ∧ c = SAT (wcp(Init, q 0 )))}, -∆ = {q e → q ′ |q ∈ A ∧ q ′ ∈ A ∧ e ∈ Ev ∧ SAT (wcp(a, q ′ ) ∧ q)}, -Q = {q|∃(q ′ , e).(q e → q ′ ∈ ∆ ∨ q ′ e → q ∈ ∆)}, -∆ + = {q e → q ′ |q ∈ A ∧ q ′ ∈ A ∧ e ∈ Ev ∧ ¬SAT (¬(wp(a, q ′ ) ∧ grd(a)) ∧ q)}, -∆ -= {q e → q ′ |q ∈ A ∧ q ′ ∈ A ∧ e ∈ Ev ∧ ¬SAT (¬sp(a, q) ∧ q ′ )}, -∆ c (⊆ C × Ev × C) is such that c e → c ′ ∈ ∆ c ⇒ SAT (wcp(a, c ′ ) ∧ c), -Γ = {(q, c)|q ∈ Q ∧ c ∈ C ∧ α P (c) = q ∧ ∃(e, c ′ ).(c e → c ′ ∈ ∆ c ∨ c ′ e → c ∈ ∆ c )}.

Examples

For the sake of readability, let us now introduce two examples that will be used to illustrate our propositions. Each one is intended to illustrate a different point while remaining small and easy to read. The Electrical System example of Sec. 4.1 is a finite state control and command system that illustrates the various kinds of transition relations ∆, ∆ -and ∆ + , as represented in Fig. 3. The example of Sec. 4.2 is a very simple model, but with an infinite state space. Its aim is to illustrate that combining the two under-approximation techniques gives better transition and path coverage than each one separately (see Sec. 5.3, paragraph "Comparison with the other methods").

(a) Physical Representation A clock H periodically sends a signal that causes a commutation of the closed switch. The system has to meet the following requirements: one switch and only one is closed at a time and a clock signal changes the switch that is closed. The batteries may break down. If it happens to the one that is powering D, an exceptional commutation is triggered. We assume that there is always at least one battery working. When there is only one battery working, the clock signals are ignored. Figure 2(b) models the system by means of three variables. H models the clock and takes two values: tic to ask for a commutation and tac when it has occurred. Sw models the switches by an integer that indicates which one is closed. Bat models the batteries breakdowns by a total function that associates ok or ko (for a broken battery) to each battery. The state changes are described by means of four events: Tic sends a commutation signal, Com changes the closed switch, Fail breaks down a battery and Rep repairs a battery.

X b = {H, Sw, Bat} I b = H ∈ {tic, tac} ∧ Sw ∈ 1..3 ∧ (Bat ∈ 1..3 → {ok, ko}) ∧ Bat(Sw) = ok Init b = H, Sw, Bat := tac, 1, {1 → ok, 2 → ok, 3 → ok} T ic b = H = tac ⇒ H := tic Com b = ∃(i, j).(i ∈ 1..3 ∧ j ∈ 1..3 ∧ i = j ∧ Bat(i) = ok ∧ Bat(j) = ok) ∧ H = tic ⇒ @ns.(ns ∈ 1..3 ∧ Bat(ns) = ok ∧ ns = Sw ⇒ H, Sw := tac, ns) F ail b = ∃(i, j).(i ∈ 1..3 ∧ j ∈ 1..3 ∧ i = j ∧ Bat(i) = ok ∧ Bat(j) = ok) ⇒ @nb.(nb ∈ 1..3 ∧ Bat(nb) = ok) ⇒ (nb = Sw ⇒ @ns.(ns ∈ 1..3 ∧ ns = Sw ∧ Bat(ns) = ok ⇒ Sw, Bat(nb) := ns, ko)) [](nb = Sw ⇒ Bat(nb) := ko)) Rep b = @nb.(nb ∈ 1..3 ∧ Bat(nb) = ko) ⇒ Bat(nb) := ok) (b) Specification
q0 {¬p1, p2} q1 {¬p1, ¬p2} q2 {p1, p2} q3 {p1, ¬p2} T ic, -, + Com, -, + F ail, - Rep, + T ic F ail, - Rep, + Rep F ail Rep F ail
2 = ∃(i, j).(i ∈ 1..3 ∧ j ∈ 1..3 ∧ i = j ∧ Bat(i) = ok ∧ Bat(j) = ok).
All the transitions belong to ∆. Those followed by "-" and/or "+" belong to ∆ - and/or ∆ + . In Fig. 7(a) and Fig. 7(b), we see a fragment of C 0 , Γ and ∆ c .

Simple Illustrative Model

The specification presented in Fig. 4 models a small conditional computation over a variable x. Its semantics is an infinite state transition system for unbounded integers. Our abstraction method computes the finite state symbolic transition system of Fig. 5(a). The variable pc is not abstracted whereas x is abstracted according to the two predicates x < 3 and x ≥ 3.

X b = {pc, x} I b = pc ∈ 0..3 ∧ x ∈ Z Init b = @z.(x ∈ Z ⇒ pc, x := 0, z) e1 b = pc = 0 ∧ x < 3 ⇒ pc, x := 1, x + 1 e2 b = pc = 0 ∧ x ≥ 3 ⇒ pc, x := 1, x -1 e3 b = pc = 1 ∧ x < 3 ⇒ pc, x := 2, x + 1 e4 b = pc = 1 ∧ x ≥ 3 ⇒ pc, x := 2, x -1 e5 b = pc = 2 ⇒ pc := 3 Fig. 4. A Simple Illustrative Model q0, {pc = 0, x < 3} 0 1 2 q1, {pc = 0, x ≥ 3} 3 4 5 q2, {pc = 1, x < 3} 0 1 2 q4, {pc = 2, x < 3} 0 1 2 q6, {pc = 3, x < 3} 0 1 2 q3, {pc = 1, x ≥ 3} 3 4 5 q5, {pc = 2, x ≥ 3}
b = q0.0 e1 → q2.1 e3 → q4.2 e5 → q6.2, t2 b = q0.2 e1 → q3.3 e4 → q4.2 e5 → q6.2, t3 b = q1.3 e2 → q2.2 e3 → q5.3 e5 → q7.3, t4 b = q1.4 e2 → q3.3 e4 → q4.2 e5 → q6.2, t5 b = q1.5 e2 → q3.4 e4 → q5.3 e5 → q7.3.
(b) Concrete Tests The transitions of ∆ -and ∆ + are labelled with "+" and/or "-". A ∆ c relation is represented by the full arrows. All the concrete states in q 0 and q 1 belongs to C 0 .

Abstraction Computation

We first present in Sec. 5.1 the basic algorithm to compute an existential overapproximation defined by ∆. Some implementation-dependent heuristics have been abstracted. This algorithm also computes ∆ + and ∆ -, and we improve it by computing on-the-fly a concrete transition relation ∆ c that is an underapproximation obtained by a partial concretisation of ∆. We improve in Sec. 5.2 the under-approximation computation of ∆ c by taking the union with an under approximation defined in [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF] from ∆ + and ∆ -. Last, we discuss in Sec. 5.3 the properties of this combined approach.

Under-Approximation by Existential Concretisation

The algorithm of Fig. 6 relies on satisfiability evaluations of predicates by means of a SAT -solver. We consider a SAT -procedure as returning either the false value if the predicate is not satisfiable, or a concrete state c otherwise, that is also interpreted as the true value. In practice, SAT -solvers may also return an unknown value when they manage to prove neither the satisfiability nor the unsatisfiability of a predicate. We liken this unknown value to false in our algorithm.

The algorithm computes an abstraction (an STS) in two steps. Lines 1-5 compute the initial abstract and concrete states Q 0 and C 0 while lines 7-33 compute the set Q of reachable abstract states and the transitions of ∆, ∆ + , ∆ - and ∆ c . QR is the set of source states whose successors have to be computed, either because they are initial, or target states of reachable transitions of ∆.

To compute the successors of a state q (lines 9-32), the algorithm enumerates all the possible target states q ′ (line 10) and all the events (line 11) that could lead to q ′ . The transition q e → q ′ is added to ∆ when wcp(a, q ′ ) ∧ q is satisfiable (lines 12-14). Lines 15-19 search for a concretisation c ′ of the target state q ′ , that would be the target of an existing concrete state c of the source state q. If such a c ′ is found (line 20), the transition c e → c ′ is added to ∆ c (line 21), otherwise a transition nc e → c ′ is added (line [START_REF] Sen | CUTE: a concolic unit testing engine for C[END_REF][START_REF] Cadar | EXE: automatically generating inputs of death[END_REF] where nc is the new concretisation of q resulting of the satisfiability condition SAT (wcp(a, q ′ ) ∧ q) that guarantees its existence in lines 12-13. Line 26 stores the concretisation of the target state in Γ . If q ′ was not already known as reachable (q ′ / ∈ Q), it is added to QR (line 27). Then, if there exists a may transition, lines 28-29 complete the must+ and must-transitions when they exist. Finally, this algorithm computes a first under-approximation defined by C 0 and ∆ c by concretising ∆. After that, a second step, described in the next section, completes this under-approximation by concretising ∆ + and ∆ -.

Let C be the set of concrete states of all the abstract states of the set Q Inputs X, Init, EvDef : an Event System where EvDef b = {e b = a|e ∈ Ev} Results Q, Q0, C0, ∆, ∆ + , ∆ -, Γ, ∆ c : a Symbolic Transition System Variables QR : Set of abstract states remaining to be handled CR : Set of concrete states remaining to be handled q, q ′ : source and target abstract states of the current transition c, c ′ : source and target concrete states of respectively q and q ′ e : event name of the current transition nc : other concrete state of the source state q Begin /* Computation of the initial abstract and concrete states and of a concrete instance */ (1)

Q0 := ∅ ; Γ := ∅ ; C0 := ∅ ; (2) ForAll q ∈ A Do (3) c := SAT (sp(Init, true) ∧ q) ; (4) If c Then Q0 := Q0 ∪ {q} ; C0 := C0 ∪ {c} ; Γ := Γ ∪ {(q, c)} EndIf (5)
EndForAll ; [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF] /* Computation of the reachable states Q, the transitions in ∆, ∆ + , ∆ -and the concrete transitions in ∆ c */ (7)

∆ := ∅ ; Q := ∅ ; QR := Q0 ; ∆ c := ∅ ; ∆ + := ∅ ; ∆ -:= ∅ ; (8) While QR = ∅ Do (9)
Choose q in QR ; QR := QR -{q}

; Q := Q ∪ {q} ; (10) ForAll q ′ ∈ A Do (11)
ForAll e ∈ Ev Do /* e b = a in EvDef */ [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] nc := SAT (wcp(a, q ′ ) ∧ q) ; ( 13)

If nc Then /* nc is false if wcp(a, q ′ ) ∧ q is not satisfiable, true otherwise */ ( 14)

∆ := ∆ ∪ {q e → q ′ } ; (15) CR := Γ ({q}) ; c ′ := f alse ; /* Γ (Z) is the relational image of the set Z */ (16) While ¬c ′ ∧ CR = ∅ Do (17) Choose c in CR ; CR := CR -{c} ; (18) c ′ := SAT (sp(a, c) ∧ q ′ ) (19) EndWhile ; (20) If c ′ Then (21) ∆ c := ∆ c ∪ {c e → c ′ } (22)
Else /* There is no concrete target state for the existing concrete source states */ (23) c ′ := SAT (sp(a, nc) ∧ q ′ ) ; /* we compute one from nc */ (24)

Γ := Γ ∪ {(q, nc)}; ∆ c := ∆ c ∪ {nc e → c ′ } (25) EndIf ; (26) Γ := Γ ∪ {(q ′ , c ′ )} ; (27) If q ′ / ∈ Q Then QR := QR ∪ {q ′ } EndIf ; (28)
If ¬SAT (¬(wp(a, q ′ ) ∧ grd(a)) ∧ q) Then ∆

+ := ∆ + ∪ {q e → q ′ } EndIf ; (29) If ¬SAT (¬sp(a, q) ∧ q ′ ) Then ∆ -:= ∆ -∪ {q e → q ′ } EndIf ; (30) EndIf (31) EndForAll (32) EndForAll (33)
EndWhile End Fig. 6. Computation of an Existential Concretisation

Under-Approximation by Universal Concretisation

T. Ball proposes in [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF] a method to compute the ∆, ∆ + and ∆ -transition relations as defined in Sec. 3. An under-approximation L is defined by the set of states that are reachable from the initial ones by a sequence of must-transitions, followed by at most one may transition and a sequence of must+ transitions. Ball defines a reachability function for an STS to formalise L. Let Q be a set of states and ∆ a transition relation. The reachability function on ∆ and

Q ′ ⊆ Q is defined by R[∆](Q ′ ) = µZ.(Q ′ ∪ ∆(Z, Ev))
where µ is the least fix-point and ∆(Z, Ev) is the relational image of the sets Z and Ev by ∆. We adapt the definition of L as:

L = {q ′′ | ∃ (q, e, q ′ ) • (q ∈ R[∆ -] (Γ -1 (R[∆ c ](C 0 )))) ∧ (q ′ = q ∨ q e -→ q ′ ∈ ∆) ∧ q ′′ ∈ R[∆ + ]({q ′ })}.
For example, this process applied to the specifications of Fig. 2(b) and 4, gives the transition relations ∆ -and ∆ + represented respectively by the transitions labelled with "-" and/or "+" in Fig. 3 and in Fig. 5(a).

A contribution of our paper is to combine a concretisation of the underapproximation L with the one computed by our algorithm of Fig. 6. After the existential concretisation performed by our algorithm of Fig. 6, we concretise the longest executions of L that start in a concrete state that is reachable from the initial ones. The concretisation of the sequences of must+ transitions is performed by a forward depth search, detecting the cycles from one concrete state beginning such a sequence. The concretisation of the sequences of musttransitions is performed by a backward depth search detecting the cycles from one of the final concrete states of these sequences. Finally, the relation ∆ c is the union of the relation computed by the algorithm of Fig. 6 with the one computed by this concretisation of L.

For the example of Fig. 5(a), the final ∆ c relation is represented by the full arrows. The transition q 1 .5 e2 → q 3 .4 concretises the first transition of the following sequence in L: q 1 e2,-→ q 3 e4,-→ q 5 e5,+ → q 7 . Notice that this transition does not exist in the concretisation of ∆, but only in that of L. Finally, the whole underapproximation made of all the concrete transitions allows for generating the five test cases shown in Fig 5(b). They cover all the abstract states and all the concrete transitions of the STS of Fig 5(a). But they do not cover all the may executions of the abstract model. For example, the abstract execution q 0 e1 → q 3 e4 → q 5 e5 → q 7 is not covered, but it is not executable. This shows the interest of generating the tests from the under-approximation. This avoids generating non executable tests that give birth to a costly process of searching for an execution that does not exist.

Discussion about the Properties of the Algorithm

In this section, we explain why the algorithm of Fig. 6 terminates and is sound. We then explain that the enumeration order of the states and events in lines 10-11 impacts the accuracy of the computed under-approximation. Last we compare our combined method with the two methods of [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF][START_REF] Pȃsȃreanu | Predicate abstraction with underapproximation refinement[END_REF].

Termination. Since A is a finite set, the external loop terminates in the worst case with Q = A. The loops that compute the initial states (lines 1-5) and the two loops of lines 10-11 terminate because the sets A and Ev are finite. The internal one (lines 16-19) also terminates because the number of concrete states built for all the abstract states is finite. This number is bounded by (|A| × |Ev|) × 2 + 1 in the worst case where, for any state, any event is fireable leading to any other state and is reachable by any event from every other state.

Soundness. The transition relation ∆ c is an under-approximation of the concrete transition system associated to an event system. On the one hand, the algorithm of Fig. 6 computes a subset of the concrete states of the model associated to an event system. On the other hand, all the states verify the correction conditions. For a transition c e → c ′ concretising a transition q e → q ′ , the source state c verifies the condition SAT (wcp(a, q ′ ) ∧ q), and the target state c ′ verifies the condition SAT (sp(a, c) ∧ q ′ ) (see lines 18 and 23).

Search Order and Accuracy of the Abstractions. The number of reachable concrete executions and their size depend on the enumeration order of the events and concrete states, as Figs. 7(a) and 7(b) illustrate. Two test cases with a total of five test steps could be generated from the approximation of Fig. 7(a), while no test could be generated from the one of Fig. 7(b). Indeed, c 5 , the concrete initial and reachable state of Fig. 7(b), is not connected to any concrete transition. There are three reasons for that. Concretising the reflexive transition Rep before F ail generates the state c 4 , because Rep is not fireable in the state c 5 . The Rep transition does not connect c 4 to c 5 because c 4 has been built by the solver with an upper limit choice for the connected battery, i.e. battery 3, while the connected battery in c 5 is battery 1 (Rep doesn't change the connected battery). Consequently, the state c 3 is generated. Then F ail is applied, and as the possible concrete target states are enumerated in reverse order w.r.t their creation, c 3 is connected to c 4 rather than to c 5 . As a result, no transition is reachable from the state c 5 . This illustrates that according to the building order of the abstraction, the under-approximation contains more or less reachable concrete transitions. Notice that our implementation optimises the size of the under-approximation by considering the heuristics and parameters presented in Sec. 6.1.

Comparison with the other Methods. The combined method that we propose generates under-approximations that are more accurate than with any of the two methods presented in [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF][START_REF] Pȃsȃreanu | Predicate abstraction with underapproximation refinement[END_REF]. These two methods are not comparable as illustrated by Fig. 5(a) and shown in [START_REF] Pȃsȃreanu | Predicate abstraction with underapproximation refinement[END_REF]. The concretisation of the existential abstraction, as in [START_REF] Pȃsȃreanu | Predicate abstraction with underapproximation refinement[END_REF], allows for generating the four test cases t 1 to t 4 of Fig. 5(b). Our method additionally generates the test case t 5 thanks to the concretisation of L. In contrast, the method of [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF] would only generate the test cases t 1 and t 5 . Our method finally generates the union of the test cases generated by each of the two methods.

Implementation and Experimentations

We present in this section some optimisations to the algorithm of Fig 6 . Our experimentations show their impact on test generation.

Implementation and Optimisation

We have used the SMT-solver Z3 [START_REF] De Moura | An efficient smt solver[END_REF] to implement the SAT procedure and the B substitution calculus to implement wp, wcp, grd and sp. Our implementation Firstly, we improve its practical complexity by not examining all the triplets (q, e, q ′ ). Secondly, we better connect the concrete transitions to produce longer executions. But the universal concretisation described in Sec. 5.2 has not been implemented yet.

Improvement of the Practical Complexity. The worst case theoretical complexity of our algorithm is |A| 2 × |Ev| when the concretisation is not taken into account. Taking into account the concretisation, i.e. the loop in lines 16-19 of Fig. 6, the complexity is |A| 3 × |Ev| 2 because the maximal size of Γ ({q}) is 2 × |A| × |Ev| when there is one transition for each event towards each abstract state because any abstract transition is concretised by one concrete transition. The number of triplets (q, e, q ′ ) to explore can be reduced by computing on the one hand for each abstract state the events that can be fired on it, independently of the target states, and on the other hand, for each abstract state, the events able to reach it, independently of the source states. Let F ireable be a partial function that maps each abstract state of A to the set of events fireable on it. Let Reaching be a partial function that maps each abstract state of A to the set of events able to reach it. The computation of F ireable and Reaching is in |A| × |Ev| and allows for the following optimisations.

-In the third loop, on line 11, instead of enumerating all the events in Ev, it is possible to enumerate only the events in F ireable(q) ∩ Reaching(q ′ ): they are both fireable on q and able to reach q ′ . -In the second loop (line 10), it is sufficient to enumerate the set of reachable states (domain of Reaching) instead of the set of all the abstract states in A.

Improvement of the Connectivity Between the Concrete Transitions. To get a "good" connectivity of the concrete transitions, the algorithm tries to concretise an abstract transition (q e → q ′ ) by considering all the existing pairs of concrete states of q and q ′ . If it fails, the algorithm asks the solver to find for each concrete state of q a new concrete state of q ′ such that the concrete transition exists. If it fails again, a new pair of concrete states is built by the solver. Indeed, many concrete transitions between two different concrete states are transformed into reflexive may transitions on an abstract state. In practice, to go from an abstract state to another, it is often necessary to apply these reflexive transitions to connect inside an abstract state the concrete target state of the incoming abstract transition to the concrete source state of the outgoing abstract transition. The concretisation could be improved at no supplementary computing cost by two implementation choices and three user parameters.

1. Concretise in priority reflexive transitions so as to increase the number of concrete states of q. 2. Enumerate in priority the concrete states reachable in q (line 17) and unreached in q ′ (line 18). This requires to mark as reachable or not the concrete states during their computation and to arrange Γ in order on-the-fly. 3. Enumerate the events in an order that causes the reflexive transition to chain. For example in the Electrical System, F ail has to be called before Rep since a battery can be repaired only if it is broken. 4. Indicate the number of repetitions of some of the events, that need to be consecutively repeated to effectively make the system progress. 5. Provide a partial concretisation of the numerical variables of some targeted concrete states to guide the global concretisation.

The last three parameters rely on the hypothesis that the tester has a sufficiently good knowledge of the system and its model to be able to provide them. Knowing the "common sense" sequencing order of the events and their number of repetitions seems natural. But a partial concretisation is surely a more difficult thing to know about.

Experimental Results

In the tables, the symbols "♯", "Pot.", "Trans.", "Inst." and "Abs." respectively stand for number of, Potential, Transitions, Instantiated and Abstract. Table 1 compares two processes of test generation from abstraction. We compare test sequences that come from the abstraction algorithm defined in Sec. 5 (Process 1) with previous results obtained with a process (Process 2) in which we generate tests as executions of ∆ and then instantiate them a posteriori. The comparison is based on the coverage of the abstract transitions and the abstract states. For Process 1, we give also the coverage of concrete transitions and concrete states of ∆ c . In Process 2, we have used the theorem prover of Atelier B [START_REF] Atelier | Case tool for developing software proven without default[END_REF] instead of the SMT-solver Z3.

Since the tools used to generate the abstractions are not the same in Process 1 and Process 2, directly comparing their execution times does not make sense. Except for Demoney, these times are small with both processes. We notice however that the computation of the Demoney abstraction took 1381 s. with Process 1 vs. and 12917 s. with Process 2. We have observed that 9522 s. was spent at instantiating the tests a posteriori with Process 2. This indicates that instantiating the tests on-the-fly is more efficient.

Process 1 gives better coverage ratios for the abstract states (up to 40%) and transitions (up to 45%), excepted for the small model of Fig. 4, where Process 2 also covers the test t 5 that should be found by the second step of Process 1 described in Sec. 5.2.

Model

♯Pot.

Process The experimental results of Table 2 are about the impact of the parameters of Sec. 6.1 (items 3, 4 and 5), in terms of number of tests, number of test steps and coverage of the states and the transitions of both the abstraction and its concretisation.

We have observed each parameter variation with the two other parameters fixed at the best value that we found on the examples. The variations are as follows. There are two events sequencing: intuitive or non-intuitive. Each event is repeated either once (default parameter) or the number of times indicated in Table 2. Only Demoney has numerical variables: they are either not at all (default parameter) or partially concretised.

The results show that modifying the sequencing of the events for the Robot and Demoney examples changes the coverage ratios (up to 4 times more) and the number of test and test steps (up to 8 times more) very significantly. Repeating some of the events considerably improves the quality of the results, in terms of abstraction coverage (up to 10 times more) and of number of tests and test steps (up to 26 times more). The partial concretisation of the targeted states also substantially improves the coverage of the abstraction (up to 10 times more) and the number of tests and test steps (up to 26 times more). We have also noticed with Demoney that playing with the three parameters at once could be necessary to better improve the results. Some algorithms that compute over-approximations based on predicate abstraction can be found e.g. in [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF][START_REF] Ball | Automatic predicate abstraction of c programs[END_REF]. Predicate abstraction is also used by Ball in [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF][START_REF] Ball | Abstraction for falsification[END_REF] and Pȃsȃreanu et al. in [START_REF] Pȃsȃreanu | Predicate abstraction with underapproximation refinement[END_REF] to compute program abstractions that are underapproximations for generating tests. Ball computes an under-approximation from the reachable sequences of must-transitions followed by at most one may transition and a sequence of must+ transitions. Pȃsȃreanu et al. also compute an under-approximation, but by concretisation of the may transitions. We combine these two methods in this paper by concretising may transitions and the sequences of must transitions. We do not refine the set of abstraction predicates as in [START_REF] Pȃsȃreanu | Predicate abstraction with underapproximation refinement[END_REF][START_REF] Namjoshi | Syntactic program transformations for automatic abstraction[END_REF] to search for an exact abstraction. But we present a parametrised algorithm and many optimisations by heuristics to improve the concretisation.

We have defined in [START_REF] Bouquet | Test generation based on abstraction and test purposes to complement structural tests[END_REF] a method to extract a set of predicates P from a test purpose and a behavioural model for generating tests in an MBT approach. In [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF], P is made of all the atomic predicates that appear in the control structure of a C program. In [START_REF] Namjoshi | Syntactic program transformations for automatic abstraction[END_REF], the set of predicates is iteratively refined in order to compute a bisimulation of the initial model when it exists. SYNERGY [START_REF] Gulavani | Synergy: a new algorithm for property checking[END_REF] and DASH [START_REF] Beckman | Proofs from tests[END_REF] also combine under-approximation and over-approximation computations to check safety properties on programs. As we aim at proposing an efficient MBT method, our algorithm always terminates because it does not refine the over-approximation. Moreover, it generates on-the-fly the under-approximations by using the witnesses of satisfiability proofs to build the over-approximation.

Other works are about generating tests from abstraction. The tools Agatha [START_REF] Rapin | Behavioral unfolding of formal specifications based on communicating extended automata[END_REF], DART [START_REF] Godefroid | DART: directed automated random testing[END_REF], CUTE [START_REF] Sen | CUTE: a concolic unit testing engine for C[END_REF], EXE [START_REF] Cadar | EXE: automatically generating inputs of death[END_REF] and PEX [START_REF]PEX: Automated exploratory testing for[END_REF] also compute abstractions from models or from programs, but by means of symbolic execution [START_REF] Pȃsȃreanu | A survey of new trends in symbolic execution for software testing and analysis[END_REF]. This data abstraction approach computes an execution graph. Its set of abstract states is possibly infinite whereas it is finite with the predicate abstraction method. The methods of [START_REF] Calamé | Automatic model-based generation of parameterized test cases using data abstraction[END_REF] implemented in STG [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF] use abstractions defined by the user and modelled by IOSTS (Input Output Symbolic Transition System). They use test purposes synchronised with abstractions, both defined as IOSTS. Then, the synchronised product allows for generating tests after an optimisation step, which consists of pruning the unreachable states by abstract interpretation. Our approach is very similar in that we also use test purposes and abstractions, as well as synchronisation. But there are three differences. First, our abstractions are computed from a set of predicates defined from the test purposes, whereas STG uses user-defined abstractions. Second, an optimisation is performed by the abstraction computation by using the invariant properties (that do not exist in an IOSTS) specified in the B models used in our experimentations. It allows, for the weakest precondition computation, to minimise the symbolic state space and the feasible transitions. Third, we use SMT solvers, that combine constraint solving and theories for proof, instead of pure constraint solving to instantiate the symbolic tests.

Similarly to the concolic execution in [START_REF] Sen | CUTE: a concolic unit testing engine for C[END_REF], we combine concrete execution with predicate abstraction. But concolic tools use symbolic execution instead of predicate abstraction. Furthermore, we use a dual combination by performing predicate abstraction and concretising incrementally the abstract transitions, whereas concolic execution performs a concrete execution and at the same time collects the symbolic path constraints. Moreover, hybrid concolic execution [START_REF] Majumdar | Hybrid concolic testing[END_REF] combines random generation of input values.

Conclusion and Further Works

We have presented a method of model-based test generation and an algorithm that combines two under-approximation computations (defined in [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF][START_REF] Pȃsȃreanu | Predicate abstraction with underapproximation refinement[END_REF]) by predicate abstraction. Our contributions are this combination and the design of three adequate parameters to capture the know-how of the tester and the definition of pertinent heuristics for improving the accuracy of the under-approximations. Our experimental results indicate that generating the tests from this underapproximation with an on-the-fly instantiation is more efficient and gives better coverage ratios than an over-approximation based process with afterwards instantiation. Our experimental results also measure the impact of each parameter on the test coverage ratios. This work shows that using under-approximations is decisive for the scalability of the method. This paper also shows that the efficiency of the method depends on capturing of the tester's expertise. We propose three parameters to the tester: the order in which the operations are considered, the number of their consecutive repetition and a subset of the concrete states to target. The practical usability of these parameters by a validation engineer has to be assessed by experimentations on larger case studies. Also, we intend as future works to define better parameters that would depend on the application domains.

We also have to improve the implementation of the concretisation of the under-approximation L defined in Sec. 5.2. Additionally, for the SMT-solvers to be able to deal with our behavioural models, we have by now to restrict our usage of some of the B set operators. To overcome this limitation, it will be necessary either to define new theories for the SMT-solvers, or to automatically rewrite all B predicates as first-order logic formulas.

Fig. 1 .

 1 Fig. 1. Process of Test Generation from Test Purpose by Abstraction

Fig. 2 .

 2 Fig. 2. The Electrical System and its Formal Behavioural Specification

Fig. 3 .

 3 Fig. 3. STS of the Abstract Electrical System

Figure 3

 3 Figure 3 shows the STS without C 0 , Γ and ∆ c that abstracts the model of Fig. 2(b) from the set of abstraction predicates P = {p 1 , p 2 } where p 1 = H = tic and p 2 = ∃(i, j).(i ∈ 1..3 ∧ j ∈ 1..3 ∧ i = j ∧ Bat(i) = ok ∧ Bat(j) = ok).All the transitions belong to ∆. Those followed by "-" and/or "+" belong to ∆ - and/or ∆ + . In Fig.7(a) and Fig.7(b), we see a fragment of C 0 , Γ and ∆ c .

  e5, -, + e5, -, + (a) Abstraction of the Small Model of Fig.4

  t1

Fig. 5 . 4 Figure 5

 545 Fig. 5. Abstraction and Tests for the Small Model of Fig 4

Fig. 7 .

 7 Fig. 7. Concretisations of q0 for the Abstract Electrical System

Table 1 .

 1 Efficiency of the Test Generation Methods

				1 : Concretisation Process	Process 2 : Process with instantiation
	(loc)	states ♯Tests	♯Tests Steps	Abstract Abstract Concrete Concrete ♯Inst. Tests ♯Tests States Trans. States Trans. / ♯ Abs. Tests Steps Coverage Coverage Coverage Coverage	Abstract Abstract States Trans. Coverage Coverage
	Small Model (20)	∞	7	13	8/8 (100%)	8/10 (80%)	11/15 (73%)	8/11 (73%)	4/4 (100%)	12	8/8 (100%)	10/10 (100%)
	SysAlim (100)	36	1	28	4/4 (100%)	11/11 (100%)	8/8 (100%)	15/15 (100%)	4/4 (100%)	21	4/4 (100%)	11/11 (100%)
	QuiDonc (170)	13	2	90	5/5 (100%)	22/22 (100%)	13/13 (100%)	40/40 (100%)	2/5 (40%)	16	3/5 (60%)	14/22 (64%)
	Robot (100)	384	29	224	4/4 (100%)	21/31 (68%)	44/59 (74%)	50/72 (69%)	2/4 (50%)	25	3/4 (75%)	17/31 (55%)
	Partition (80)	∞	5	9	4/7 (57%)	5/23 (22%)	9/41 (22%)	5/28 (18%)	2/14 (14%)	6	3/7 (43%)	5/23 (22%)
	DeMoney (330)	∞	34	591	10/14 (71%)	237/368 (64%)	31/161 499/1669 17/18 (95%) (19%) (30%)	170	9/14 (64%)	197/368 (54%)

Table 2 .

 2 Impact of the Use of Parameters for Test Generation

	Parameter	Model	Parameter Value	♯Tests	♯Tests Steps	Coverage Abstract Abstract Concrete Concrete Coverage States Trans. States Trans.
	Events Enumeration Order	Robot DeMoney	Loading order Inverse loading order Valid credit order Inverse valid credit order	2 1 34 20	16 2 591 422	50% 25% 71% 50%	26% 6% 64% 45%	21% 7% 19% 15%	26% 6% 30% 25%
	Events Multiple Call	Robot DeMoney	Part Arrival: 3 Default parameter Put Data: 4 Default parameter	29 7 34 1	224 35 591 22	100% 75% 71% 7%	68% 35% 64% 6%	74% 34% 19% 2%	69% 42% 30% 6%
	Partial Concrete DeMoney Valuation	A partial concretisation Default parameter	34 1	591 22	71% 7%	64% 6%	19% 2%	30% 6%