Jacques Julliand
email: jjulliand@femto-st.fr

Olga Kouchnarenko

Pierre-Alain Masson
email: pamasson@femto-st.fr

Guillaume Voiron
email: gvoiron@femto-st.fr

Approximating Event System Abstractions by Covering their States and Transitions Version 1

Keywords: Predicate abstraction, under-approximation, event systems Predicate abstraction, under-approximation, event systems

In event systems, contrarily to sequential ones, the control flow is implicit. Consequently, their abstraction may give rise to disconnected and unreachable paths. This paper presents an algorithmic method for computing a reachable and connected under-approximation of the abstraction of a system specified as an event system. We compute the under-approximation with concrete instances of the abstract transitions, that cover all the states and transitions of the predicate-based abstraction. To be of interest, these concrete transitions have to be reachable and connected to each other. We propose an algorithmic method that instantiates each of the abstract transitions, with heuristics to favour their connectivity. The idea is to prolong whenever possible the already reached sequences of concrete transitions, and to parameterize the order in which the states and actions occur. The paper also reports on an implementation, which permits to provide experimental results confirming the interest of the approach with related heuristics.

Introduction

Abstracting a program or its specification allows to control the size of its state space description, at the price of a loss in accuracy. That facilitates their algorithmic exploitation, otherwise limited by the huge if not infinite number of concrete states. The general idea of abstraction is to gather states that share common properties into super-states. In predicate abstraction [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF] the concrete states are mapped onto a finite set of abstract ones, by means of a set of predicates that characterizes each abstract state. An abstract transition links two abstract states when it has at least one concrete instantiation. Such transitions are called may [START_REF] Godefroid | On the expressiveness of 3-valued models[END_REF], meaning that they may be instantiated. Still there is no guarantee that two consecutive may transitions can necessarily be instantiated as two consecutive connected concrete transitions: their respective target and source concrete states may differ.

This paper aims at computing connected and reachable concrete paths from a predicate abstraction of a system formally specified as an event system [START_REF]Modeling in Event-B: System and Software Design[END_REF], which is a special kind of action system [START_REF] Dijkstra | Guarded commands, nondeterminacy, and formal derivation of programs[END_REF][START_REF] Dijkstra | A Discipline of Programming[END_REF]. We propose an algorithmic method for computing an underapproximation that covers all the states and transitions of this abstraction.

An event in an event system specifies state variable modifications by means of a guarded action. The actions are activated whenever their guard becomes true, so that there is no natural control flow as in a program. As a result, paths of the system may become disconnected and even unreachable in the abstraction. Still, we are interested in covering the reachable part of the abstraction as best as possible. This work has been motivated by a testing purpose: our intention is to cover paths of an abstraction by tests. But the method could also apply for example to the model-checking of safety properties. These potential applications are not presented in this paper due to lack of space.

We propose to under-approximate the abstraction by computing concrete instances of the abstract event sequences. The idea behind our method is to favour the connectivity and reachability of the successive concrete instances by prolonging whenever possible the already reached concrete transitions. Our proposal in this paper is as sketched:

• we instantiate each of the abstract transitions by enumerating all the possibilities of connecting two abstract states by any event,

• we use heuristics for controlling the order in which the events and states are enumerated, according to some know-how of the natural flow of the events succession,

• we use concrete state coloration, similarly to [START_REF] Veanes | Combined algorithm for approximating a finite state abstraction of a large system[END_REF], for prolonging preferably the sequences known to be reachable and connected.

Our contributions allow then generating a concrete transition system from an event system. We also report on an implementation, which permits us to provide experimental results confirming the interest of the approach with the related heuristics.

The technical background of our paper regarding event systems, predicate abstraction and may transition systems is given in Sec. 2. Section 3 presents an electrical system as an illustrative example. The algorithm for computing both an abstraction and its approximation is presented in Sec. 4. The heuristics that we propose to enhance the coverage achieved by the algorithm are given in Sec. 5. Our experimental results are presented in Sec. 6. Section 7 describes related work, and Sec. 8 concludes the paper.

Background

In this paper systems are specified by event systems (ES) described in the B syntax [START_REF] Voiron | The B Book[END_REF][START_REF]Modeling in Event-B: System and Software Design[END_REF] 1 . Notice however that our proposals and results are generic since event system semantics is defined by concrete labelled transition systems.

In this section we first present the syntax and the semantics of the B event systems. Then we present the concept of predicate abstraction and formalize the abstraction of event systems by means of May Transition Systems (MTS).

Model Syntax and Semantics

We start by introducing B event systems in Def. 1. The events are defined by means of guarded actions [START_REF] Dijkstra | Guarded commands, nondeterminacy, and formal derivation of programs[END_REF] by composition of five primitive actions where E, F are arithmetic expressions and P , P are predicates: skip an action with no effect, x, y := E, F a multiple assignment, P ⇒ a a guarded action, a 1 []a 2 a bounded non-deterministic choice between a 1 and a 2 , and @z.a an unbounded non-deterministic choice a z 1 []a z 2 [] . . . for all the values of z satisfying the guard of a denoted as grd(a). Here grd is defined on the primitive actions by: grd(skip) Definition 1 (Event System) Let Ev be a set of event names. A B event system is a tuple X, I, Init, EvDef where X is a set of state variables, I is a state invariant, Init is an initialization action such that I holds in any initial state, EvDef is a set of event definitions, each in the shape of e def = a for any e ∈ Ev, and such that every event preserves I.

Figure 1(b) depicts an example of an event system that illustrates Def. 1. Following [START_REF] Bert | Construction of finite labelled transition systems from B abstract systems[END_REF], we use labelled transition systems to define the semantics of event systems.

Let e def = a be an event. It has a weakest precondition [START_REF] Dijkstra | A Discipline of Programming[END_REF] and a weakest conjugate precondition [BC00] w.r.t. a set of target states Q denoted respectively as wp(a, Q ) and wcp(a, Q ). wp(a, Q ) is the largest set of states from which applying a always leads to a state of Q whereas wcp(a, Q ) is the largest set of states from which it is possible to reach a state of Q by applying a. An event also defines a relation between the values of the state variables X before and after the application of the event. It is expressed by the before after predicate of the event e def = a denoted as prd X (a). Let us now formally define wp, wcp and prd X following [START_REF] Bride | Tri-modal underapproximation for test generation[END_REF]. Basically, we directly consider the set of states Q and Q as predicates of the same name. We define the wp w.r.t. the five primitive actions as:

• wp(skip, Q ) def = Q , • wp(x := E, Q ) def = Q [E/x]
that is the usual substitution of x by E as in [START_REF] Hoare | An axiomatic basis for computer programming[END_REF],

• wp(P ⇒ a, Q )

def = P ⇒ wp(a, Q ), • wp(a 1 []a 2 , Q ) def = wp(a 1 , Q ) ∧ wp(a 2 , Q ),
• wp(@z.a, Q ) def = ∀z.wp(a, Q ) where z is not free in Q .

We define the wcp and prd X w.r.t. wp as:

• wcp(a, Q ) def = ¬wp(a, ¬Q ), • prd X (a) def = wcp(a, x 1 = x 1 ∧ . . . ∧ x n = x n ) that
is a predicate on the state variables X = {x 1 , . . . , x n } in the source state before a and the target state variables X = {x 1 , . . . , x n } after a.

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 CTS onto the finite state space A of an abstract transition system via a set of n predicates P def = {p 1 , p 2 , . . . , p n } over the state variables. The set of abstract states A contains 2 n states. Each state is a tuple q def = (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 a total abstraction function α : C → A such that α(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, or that c is a concrete state of q.

Let us now define the abstract transitions as may ones. 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 at least one concrete transition c e → c where c and c are concrete states with α(c) = q and α(c ) = q .

Let us define for any predicate P the solver call SAT (P ), which returns either a model satisfying P or unsat if P is unsatisfiable or unknown if the solver couldn't determine the satisfiability of P. Let e def = a be an event definition, q e → q is a may transition iff SAT (wcp(a, q ) ∧ q). We compute a concrete witness c e → c by using the before after predicate: (c, c ) := SAT (prd X (a) ∧ q [X /X] ∧ q) where q [X /X] is the predicate q in which each state variable x i is substituted by x i .

May Transition Systems

Let us introduce may transition systems (MTS), which are transition systems with abstract states, and abstract may transitions. They are closely related to Modal Transition Systems defined in [START_REF] Guldstrand | A modal process logic[END_REF][START_REF] Godefroid | Abstraction-based model checking using modal transition systems[END_REF][START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF].

Definition 2 (May Transition System) Let Ev be a finite set of event names and P def = {p 1 , p 2 , . . . , p n } be a set of predicates. Let A be a finite set of abstract states defined by

{p 1 , ¬p 1 }× {p 2 , ¬p 2 } × . . . × {p n , ¬p n }. A tuple Q, Q 0 , ∆ is an MTS if it satisfies the following conditions: • Q(⊆ A) is a finite set of states, • Q 0 (⊆ Q) is a set of abstract initial states, • ∆(⊆ Q × Ev × Q) is a may labelled transition relation.

Now, Definition 3 associates an abstraction defined by an MTS with an event system.

Definition 3 (MTS associated with an ES) Let ES def = X, I, Init, EvDef be an event system and P def = {p 1 , p 2 , ..., p n } be a set of n predicates over variables of X defining a set of

2 n abstract states A def = {p 1 , ¬p 1 } × {p 2 , ¬p 2 } × ... × {p n , ¬p n }. A tuple Q, Q 0 ,
∆ is an MTS associated to ES and P if it satisfies the following conditions:

• Q def = {q ∈ A|∃(q , e).(q e → q ∈ ∆ ∨ q e → q ∈ ∆)}, • Q 0 def = {q|q ∈ A ∧ SAT (sp(Init, I) ∧ q)} , • ∆ def = {q e → q |q ∈ A ∧ q ∈ A ∧ e def = a ∈ EvDef ∧ SAT (wcp(a, q ) ∧ q)}.
An example of an MTS, whose ES is described in Fig. 1(b), can be seen in Fig. 2 (in dashed lines). The four abstract states named q 0 to q 3 appear as rounded rectangular dashed boxes. The predicates p 1 and p 2 from which they are defined are explicitly given in Sec. 3. The abstract transitions of ∆ are represented as dashed arrows labelled by event names.

Illustrative Example: an Electrical System

To illustrate our approach, this section describes an electrical (EL) system example. It is a finite state control and command system that illustrates the MTS, as represented in Fig. 2.

Figure 1(a) shows a device D powered via a switch to one of three batteries B 1 , B 2 , and B 3 . A clock H periodically sends a signal that causes a commutation of the closed switch. The system has to meet the following requirements: one and only one switch 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

(a) Physical Representation X def = {H, Sw, Bat} I def = H ∈ {tic, tac} ∧ Sw ∈ 1..3 ∧ (Bat ∈ 1..3 → {ok, ko}) ∧ Bat(Sw) = ok Init def = H, Sw, Bat := tac, 1, {1 → ok, 2 → ok, 3 → ok} T ic def = H = tac ⇒ H := tic Com def = ∃(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 def = ∃(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 def = @nb.(nb ∈ 1..3 ∧ Bat(nb) = ko) ⇒ Bat(nb) := ok) (b) Specification
= ∃(i, j).(i ∈ 1..3 ∧ j ∈ 1..3 ∧ i = j ∧ Bat(i) = ok ∧ Bat(j) = ok).

Abstraction and Approximated Transition System Computation

This section presents an algorithm used to compute both an abstraction that is an MTS, and an under-approximation. The reunion of both is called an Approximated Transition System (see Def. 4), in which C, C 0 , ∆ c is an under-approximation of the labelled transition system that is the semantics of the event system from which the MTS is deduced. In the rest of the paper, for the abstract states, we distinguish between the may-reachability and the reachability.

The former is the reachability by the abstract may transition relation ∆, and the latter is the reachability by the concrete transition relation ∆ c in the ATS. We say that an abstract state q is reachable if there exists at least one concrete instance of q that is reachable thanks to the transition relation ∆ c . By extension, an abstract transition is reachable if there exists at least one concrete instance in ∆ c whose source state is reachable. The concretization of the may transitions is performed on the fly during the computation of the MTS. This algorithm guarantees that every may transition between two abstract states is concretized. A total abstraction function α maps each concrete state of C to an abstract state of Q.

The algorithm comes in two versions, both of them being presented in the same figure due to a lack of room. The first version is the one presented in this section. It is referred to as Alg. 1. The second version, referred to as Alg. 2, is enhanced by heuristics that are explained in Sec. 5. The differences between Alg. 1 and Alg. 2 are highlighted and enclosed in square brackets. Read the left hand highlighted parts for Alg. 1, and replace them with the right hand ones for Alg. 2. Notice that since Alg. 2 computes more things than Alg. 1, some fictive empty parts (the empty highlighted square brackets [ ]) have been added in Alg. 1.

Definition 4 (Approximated Transition System) Let Q, Q 0 , ∆ be an MTS. A tuple Q, Q 0 , ∆, C, C 0 , α, ∆ c is an ATS whose C, C 0 , α, ∆ c is a concretization of the MTS Q, Q 0 , ∆ where:
• C, C 0 are sets of respectively concrete states and concrete initial states,

• α is a total abstraction function from C to Q,

• ∆ c (⊆ C × Ev × C) is a concrete labelled transition relation.
Figure 2 shows the ATS computed by Alg. 2 for the electrical system of Fig. 1(a) with predicates P 0 (see Sec. 3). The MTS appears in dashed lines while the full lines represent its concretization. The concrete states are showed as big dots numbered according to their order of discovery by Alg. 2. Lines 1 to 8 of Alg. 1 compute the set of initial abstract states Q 0 , an instance of each being recorded as a concrete witness in C 0 with its association in α. Lines 9 to 34 compute the may transition relation ∆. Each abstract transition is concretized by a witness {c w e → c w }, and the concrete states c w and c w are recorded in C with their associations in α. For that it computes in the set RQ the set of may-reachable states. For each may-reachable source state, it checks for each potential abstract state (line 12) and for each event (line 13) if a may transition exists (line 14). When it is the case, the algorithm records the witness transition (see lines 16 and 27), but also possibly another concrete transition (see lines 17 to 26) whose source state is one of the existing concrete states of the current source state q when it exists. This last transition is computed first to improve the reachability of the concrete transition relation. Indeed, the existing concrete states are more likely to be connected to the initial states than the witness source state provided by the solver in line 14. Last, line 30 adds q as a may-reachable state that has not been taken into account yet to compute the may transition relation.

Output : Q, Q 0 , ∆, C, C 0 , α, ∆ c , [ ] : [κ] an ATS [ ]
[provided with a coloration function κ ∈ C → {green, blue}] Variables : RQ: the set of abstract states remaining to be handled q, q : the source and target abstract states of the current transition c, c : the concrete source and target states of respectively q and q cw, c w : the witness concrete source and target states of a may-transition GC: the set of [already known] concrete states of q

[green C-reachable] [ ]
[BC: the set of blue concrete states of q]

1 Q := ∅; Q 0 := ∅; ∆ := ∅; C 0 := ∅; α := ∅; ∆ c := ∅; [ ] [κ := ∅;] 2 foreach q ∈ A do 3 c := (SAT (prd X (Init) ∧ q[X /X]))[X/X ] 4 if c / ∈ {unsat, unknown} then 5 Q 0 := Q 0 ∪ {q}; C 0 := 0 ∪ {c}; α(c) := q 6 [ ] [κ(c) := green;] 7 end 8 end 9 C := C 0 ; RQ := Q 0 ; 10 while RQ = ∅ do 11 choose q ∈ RQ; RQ := RQ -{q}; Q := Q ∪ {q} 12 foreach q ∈ [A] do [list orderStates(A, q)] 13 foreach (e def = a) ∈ [EvDef] do [list oEv] 14 (cw, c w ) := SAT (prd X (a) ∧ q [X /X] ∧ q) 15 if (cw, c w ) / ∈ {unsat, unknown} then 16 ∆ := ∆ ∪ {q e → q }; 17 GC := {s | α(s) = q [ ]} [ ∧ κ(s) = green] 18 (c, c ) := SAT (prd X (a) ∧ q [X /X] ∧ s∈GC s)

Heuristics for Better Abstraction Coverage

Using Alg. 1, the connectivity and the reachability of the computed ATS might be weak, since it strongly depends on the solver's choices. This section provides two heuristics, integrated into Alg. 2, for improving both the connectivity and the reachability. The first heuristic addresses this problem by allowing the engineer to firstly define an order for the set of events of Ev in an ordered list oEv (line 13) and, secondly, a custom function ordering the set of abstract states A (line 12). The second heuristic, exposed in Sec. 5.2, adapts the partial computation of reachability proposed in [START_REF] Veanes | Combined algorithm for approximating a finite state abstraction of a large system[END_REF] to our purpose for integrating it into Alg. 2. The resulting new algorithm's complexity is the same as the previous one.

Events and States Ordering

Our first heuristic consists of providing means to control the order in which the events and abstract target states are handled by the algorithm.

Indeed, usually in reactive systems, some events can only be fired after other events have previously been executed. Let us consider the EL system where no battery repairing (modelled by the Rep event) can occur unless at least one battery has broken down first (modelled by the F ail event). Since Alg. 1 currently uses an unordered set of events EvDef , it might attempt to concretize a Rep transition before trying to concretize any F ail transition. In this case, the concrete source state of the Rep transition would not be a reachable one. To fix we introduce the ordered list of events oEv as an input in Alg. 2. To compute a complete abstraction, i.e. covering all events and all states, oEv must contain at least one occurrence of each event of the set EvDef . For example, for the EL system, in all judicious orders, F ail must precede Rep for the aforementioned reason, and T ic must precede Com because Com is a response to the event T ic.

Similarly, the orderStates function parameterizes Alg. 2. Thanks to this function, the order in which the abstract target states are handled can be controlled. To compute a complete abstraction, the list returned by orderStates must contain at least all the abstract states of A. While being completely customizable by the engineer, the function used in our experiments presented in Sec. 6 gives better results for an order in which the first target abstract state handled is the source abstract state (state q in line 11) and the other states are ordered arbitrarily. Indeed, treating reflexive abstract transitions first tends to increase the number of reachable concrete states within the source abstract state. As a result, the chances that the next abstract transitions can be concretized from a reachable source state are increased.

When applying Alg. 1 to the EL system with a set of abstraction predicates (first AP in Table 1), 33.33% of the abstract states and 11.11% (see line 1) of the abstract transitions are covered by the ATS. Integrating the event and state ordering without coloration improved these ratios respectively to 66.67% and 44.44%.

These ordering heuristics are integrated into Alg. 2, along with the concrete states coloration discussed in Sec. 5.2. Even though our results did not focus on that point, an interesting perspective could be to consider the concretization of a same abstract transition multiple times. This could be useful for instance for systems requiring initialization steps that repetitively apply the same event, such as a credit card system for example. In fact, this behaviour can already be implemented using our algorithm by adding the same event to oEv several times, and by adding the target state of the abstract transition several times to the list returned by the orderStates function.

Concrete States Coloration

The reachability of the concrete states of the under-approximation is improved and computed on the fly in Alg. 2 without increasing its complexity w.r.t. Alg. 1. The principle is to associate a colour with each concrete state. A reachable state is coloured in green and a state whose reachability is unknown is coloured in blue. While Alg. 1 tried to concretize the abstract transitions from an already known concrete state, Alg. 2 uses the reachability information when concretizing the abstract transitions. It first tries to concretize an abstract transition from any known and reachable state (see lines 17 and 18). If it is indeed possible (line 19), the solver returns a first reachable concrete transition, added to the ATS, whose concrete target state becomes green (see lines 20 and 21). To improve the connectivity, the algorithm also tries to join a green source concrete state to a target blue one, whose reachability is thus currently unknown (line 22). If it is possible (line 23), its colour becomes green (line 24) since it is a FEMTO-ST Institute target of a concrete transition starting from a reachable (green) concrete state. Even if the concretization from a known green concrete state is not possible, the abstract transition is still concretized. The corresponding concrete source and target states may already be known. In this case, their reachability remain the same. Otherwise, since we have no information about their reachability, they are coloured in blue (see lines 28 and 29).

When Alg. 2 with coloration and without events and states ordering to the EL system with the first set of abstraction predicates in Table 1, 100% of the abstract states and 77.78% of the abstract transitions are covered by the ATS. This is better than with Alg. 1 that gives respectively 33.33% and 11.11%. Moreover, integrating the two heuristics seen in Sec. 5.1 into Alg. 1 improved these two ratios to 100%.

These heuristics allow improving the reachability of the ATS for all the systems that we use in our experiments (see Sec. 6.2).

Implementation and Experimentation

This section introduces in Sec. 6.1 our proof-of-concept tool developed to evaluate the effects of the heuristics. The experimental results on four examples in Table 1 are presented in Sec. 6.2. Then, in Sec. 6.3 we analyse these results and conclude on the contributions of the heuristics presented in this paper.

About the Tool

The developed tool can be seen as a library for handling abstract and concrete transition systems as well as event systems. It embeds an event-B parser and allows to manipulate most event-B systems. The two algorithms are implemented and can be applied to them. The library also provides the user with many facilities for dealing with event systems. For instance, pre-implemented functions allow to easily compute an abstraction of a model from a set of abstraction predicates, as well as the wp, wcp and before-after predicates prd X of events defined by guarded actions. The library also contains functions to check the modality of abstract transitions and to find a concretization of an abstract state or an abstract transition. It can also be seen as a simple API for multiple SMT-solvers since the tool automatically generates SMT-Lib2 code for checking the satisfiability of any first order boolean formula. The tool is constituted of more than 5000 lines of JAVA code (version 8) and uses Z3 [START_REF] De Moura | An efficient SMT solver[END_REF] as default SMT-solver. The library can be downloaded at https: // github. com/ stratosphr/ stratest/ wiki . This website also gives information on how to use the tool.

Experimental Results

This section provides the results obtained when applying Alg. 1 and Alg. 2 to a set of four realistic event systems of increasing size. These event systems were taken back from various previous work without modification so as not to influence the experiment and threaten the validity of the results.

The set of examples contains the electrical system (EL) presented in Sec. 3, a phone book service (PH), a coffee machine system (CM), and a car alarm system (CA). For each of them, two different sets of abstraction predicates have been used (see the AP column).

The following column names appear in Table 1: Sys for the system studied and an upper approximation of its size between parentheses, #Ev for the number of events in the event system, AP for an identification of the set of abstraction predicates used, #AP for the number of abstraction predicates in AP, Alg. for the algorithm applied, #AS for the number of mayreachable abstract states, #AS reach for the number of reachable abstract states computed, τ AS for the abstract state coverage that is the ratio #AS reach #AS , #AT for the number of abstract transitions, #AT reach for the number of reachable abstract transitions computed. Note that we say that an abstract transition is reachable if there exists a concrete instance of it in the ATS that is reachable. Next, there are the following column names: τ AT for the abstract transition coverage that is the ratio #AT reach #AT , #CT for the number of concrete transitions computed, ρ CT for the ratio #CT #AT reach which measures the efficiency of the method, by indicating in average how many concrete transitions have been computed for making an abstract transition reachable, and finally Time for the ATS computation runtime (in minutes). The connectivity between transitions is indirectly measured via the coverage and efficiency rates, since a reachable state or transition is necessarily connected to a concrete initial state.

The main results of our method are the coverage ratios of abstract states (τ AS ) and abstract transitions (τ AT ). For almost identical computation time(s), an improvement of these ratios indicates a better performance of the method. For ρ CT , a value between 3 and 1 indicates that the algorithm covers one abstract transition per iteration step. When this ratio decreases that indicates an improvement of the efficiency. Indeed, for each abstract transition, each iteration step computes one up to three transitions according to the conditions in lines 19 and 23. For the EL system, with the first set of abstraction predicates, ρ CT decreases from 13 to 2, meaning that the heuristic allowed to compute more interesting concrete transitions, increasing the abstraction transition coverage from 11.11% to 100%.

Analysis of the Obtained Results

This section gives some conclusions and insights about the results exposed in Table 1.

As expected, the ATS computation times are nearly identical, no matter which version of the algorithm has been used. Note that for two cases out of eight the ATS computation time with Alg. 2 is on average slightly faster than with Alg. 1. Since the formulas whose satisfiability is checked are different between the two algorithms, the solver may be faster to provide an answer for the formulas in Alg. 2 than in Alg. 1.

We observe that Alg. 2 improves both the abstraction coverage rates and the efficiency ρ CT compared to Alg. 1. In particular, we point out the CM case with the first AP where the transition coverage and the efficiency achieved by Alg. 2 is about respectively five and four times better than by Alg. 1.

For all systems and all sets of abstraction predicates, the abstraction coverage is improved by Alg. 2. Depending on the set of predicates used, the coverages for states and transitions can reach up to 100%. On most examples however, Alg. 1 covers less than half of the abstract states and transitions. Note for example the CM case with the second set of abstraction predicates where the abstract states and transitions coverage(s) are respectively twice and three times better using the heuristics. All these results empirically confirm the interest of the proposed heuristics to improve the abstraction coverage.

The heuristics also produced good results concerning the efficiency rate ρ CT . For most cases, its value is decreased by Alg. 2 thanks to the heuristics, which means that they generally help concretizing abstract transitions by useful transitions improving the abstraction coverage. For the CM system with the second AP and Alg. 1 for example, an average of 11.86 concrete transitions need to be computed in order to cover one abstract transition. When the heuristics are used however, an average of only 3.08 concrete transitions computation is needed to cover one abstract transition.

The ordering heuristic alone does not necessarily improve the abstraction coverage w.r.t. Alg. 1, whereas the coloration heuristic alone always improves the results. Nevertheless, for four cases out of the eight presented in this paper, combining the ordering and coloration heuristics improves the abstraction coverage compared to coloration only. For the CM system with the first AP for example, the ordering heuristic alone covers two abstract states compared to three with Alg. 1, and six abstract transitions compared to five. The coloration heuristics alone covered all of the four abstract states, and twenty-two out of the thirty abstract transitions. When combining both heuristics, the four abstract states and twenty-four abstract transitions are covered.

Related Work

In [START_REF] Namjoshi | Syntactic program transformations for automatic abstraction[END_REF] and in [START_REF] Pȃsȃreanu | Predicate abstraction with under-approximation refinement[END_REF], the set of abstraction predicates is iteratively refined in order to compute a bisimulation of the semantics of the model when it exists. None of these two methods is guaranteed to terminate, because of the refinement step that sometimes needs to be repeated endlessly. SYNERGY [GHK + 06] and DASH [BNR + 10] combine under-approximation and overapproximation computations to check safety properties on programs. As we aim at proposing an efficient method to build a reachable under-approximation of a system that covers all abstract states and all abstract transitions w.r.t. a specification and a set of predicates, our algorithm does not refine the approximation and so always terminates.

The closest methods to ours are those that are proposed in [START_REF] Grieskamp | Generating finite state machines from abstract state machines[END_REF] and in [START_REF] Veanes | Combined algorithm for approximating a finite state abstraction of a large system[END_REF]. These approaches propose algorithms that compute an under approximated concretization of a predicate abstraction covering its abstract states and transitions. Both these methods are exploited for generating tests. The algorithm in [START_REF] Grieskamp | Generating finite state machines from abstract state machines[END_REF] does not traverse nor compute the may abstraction. It builds a partial concretization of the abstract states that are reached from an initial concrete state by a forward walk. To improve this method, the algorithm in [START_REF] Veanes | Combined algorithm for approximating a finite state abstraction of a large system[END_REF] computes exhaustively the may abstraction by random abstract state generation. Therefore, some generated concrete states are not reached. Then Veanes and al. [START_REF] Veanes | Combined algorithm for approximating a finite state abstraction of a large system[END_REF] propose to distinguish between four kinds of abstract transitions: green transitions when there exists an instance that is reached from an initial concrete state, blue transitions when there exists instances, but none known to be reachable from an initial state, red transitions when there does not exist any instance, and grey transitions for the transitions that have not been concretized yet. In our method, we compute and concretize only the part of the may abstraction that is may-reachable by an abstract transition from an initial abstract state. We do not record the red transitions that are non-existing transitions in the MTS, and we do not need the grey transitions that are the ones which remain to be treated. In contrast with [START_REF] Veanes | Combined algorithm for approximating a finite state abstraction of a large system[END_REF], our method colours the concrete states instead of the abstract transitions. This allows us to distinguish between the reached states (green) and the states for which we do not know whether they are reached (blue) or not. So for improving the method, Alg. 2 connects in priority a green source state s to a blue target state t. That has a "domino effect" because all the blue reached states from t remain blue, but become reachable.

Other works are about generating an under approximation to generate 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 [CGP + 06] and PEX [START_REF] Tillmann | Pex-white box test generation for .net[END_REF] also compute abstractions from models or programs, but only by means of symbolic executions [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 our method.

Our method can be applied to generate tests as the concolic execution in [START_REF] Sen | CUTE: a concolic unit testing engine for C[END_REF]. The concolic method allows to generate structural tests of systems covering partially the control flow that must be explicited. Our approach allows to generate tests covering the paths defined by the set of abstraction predicates for systems whose control flow is implicitly defined.

Conclusion and Further Work

This paper has presented an algorithmic method for computing a concrete approximation of the predicate abstraction of an event system. All of the abstract states and transitions are covered, but as the control flow is implicit in an event system, our method focuses on computing concrete sequences that are connected and reachable. We have presented two heuristics allowing us to better reach and connect these sequences. One heuristic colours the states that are known to be reachable, and the other takes a user defined order on the events and abstract states enumeration as parameters. Experimental results on four case studies are exhibited to confirm the practical interest of our approach.

As future work, we intend to define other means for guiding the sequences instantiation, in addition to the events ordering. We could introduce a relevance function on concrete states, as is done in [START_REF] Grieskamp | Generating finite state machines from abstract state machines[END_REF], for targeting peculiar concrete states considered as more relevant. Also, our intention is to use the concrete sequences that we compute as model-based tests issued from a formal model of the specification. Abstracting this model would allow selection criteria such as paths selection to be used, when the size of the explicit model would prevent it.

  def = true, grd(x, y := E, F ) def = true, grd(P ⇒ a) def = P ∧ grd(a), grd(a 1 []a 2 ) def = grd(a 1 ) ∨ grd(a 2 ) and grd(@z.a) def = ∃z • grd(a).

Figure 1 :

 1 Figure 1: Electrical system and its specification

Figure 2 :

 2 Figure2: Example MTS and ATS of the Electrical System. The values of the concrete states are indicated in parentheses right by them. For example with state c 8 , (2, 011) means that battery 2 is used, and that battery 1 is ko while batteries 2 and 3 are ok. The value of h is given globally in the abstract states.

27 C

 27 19 if (c, c ) / ∈ {unsat, unknown} then 20 C := C ∪ {c }; α(c ) := q ; ∆ c := ∆ c ∪ {c e c ) := green; BC := {s | α(s ) = q ∧ κ(s ) = blue};] 22 [ ] [(c, c ) := SAT (prd X (a) ∧ ( s ∈BC s )[X /X] ∧ s∈GC s);] 23 [ ] [if (c, c ) / ∈ {unsat, unknown}then 24 ∆ c := ∆ c ∪ {c e → c }; κ(c ) := green; := C ∪ {cw, c w }; ∆ c := ∆ c ∪ {cw e → c w }; α(cw) := q; α(c w ) := q ; 28 [ ] [if cw ∈ domain(κ) then κ(cw) := blue end ] 29 [ ] [if c w ∈ domain(κ) ∨ κ(cw) = green then κ(c w ) := κ(cw) end ] 30 if q ∈ Q then RQ := RQ ∪ {q } end

  Approximation d'abstractions de systèmes d'événements en couvrant leurs états et transitions Résumé : Dans les systèmes d'événements, contrairement aux systèmes séquentiels, le flot de contrôle est implicite. En conséquence, leur abstraction peut conduire à des chemins non connexes et innateignables. Ce papier présente une méthode algorithmique permettant le calcul d'une sousapproximation, connexe et atteignable, de l'abstraction d'un système d'événements. Notre sousapproximation est constituée d'instances concrètes des transitions abstraites, et couvre tous les états et transitions d'une abstraction par prédicats. Pour être exploitables, ces instances concrètes doivent être atteignables et connexes entre elles. Nous proposons un algorithme qui instancie chaque transition abstraite, avec des heuristiques visant à favoriser leur connexité. Le principe est de prolonger chaque fois que c'est possible les séquences d'instances concrètes déjà atteintes, et de paramétrer l'ordre dans lequel les états et les événements sont considérés. Ce papier décrit aussi une implantation de la méthode, qui nous a permis d'obtenir des résultats expérimentaux confirmant l'intérêt de la méthode.

	Version 1

Mots-clés : Abstraction par prédicats; sous-approximation; systèmes d'événements FEMTO-ST Institute, DISC research department UFR Sciences -Route de Gray -F-25030 BESANC ¸ON cedex FRANCE

Table 1 :

 1 ATS Computation ResultsSys #Ev AP #AP Alg. #AS #AS reach τ AS (%) #AT #AT reach τ AT (%) #CT ρ CT

	Time

Tel: (33 3) 81 66 65 15 -Fax: (33 3) 81 66 64 50 -e-mail: fvernill@femto-st.fr

RR -FEMTO-ST-2496

We could alternatively use a syntax with guarded commands[START_REF] Dijkstra | Guarded commands, nondeterminacy, and formal derivation of programs[END_REF], such as Abstract State Machines[START_REF] Gurevich | Abstract State Machines, Theory and Applications[END_REF][START_REF] Gurevich | Sequential abstract-state machines capture sequential algorithms[END_REF].

FEMTO-ST Institute