Peter Schrammel

Bertrand Jeannet

Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs

Keywords: Verification, Static Analysis, Abstract Interpretation, Abstract Acceleration, Control Flow Graph Partitioning vérification, analyse statique, interprétation abstraite, accélération abstraite, partitionnement de graphe de contrôle

Acceleration methods are commonly used for speeding up the convergence of loops in reachability analysis of counter machine models. Applying these methods to synchronous data-flow programs with Boolean and numerical variables, e.g., Lustre programs, requires the enumeration of the Boolean states in order to obtain a control flow graph (CFG) with numerical variables only. Our goal is to apply acceleration techniques to data-flow programs without resorting to this exhaustive enumeration. To this end, we present (1) logico-numerical abstract acceleration methods for CFGs with Boolean and numerical variables and (2) partitioning techniques that make logicalnumerical abstract acceleration effective. Experimental results show that incorporating these methods in a verification tool based on abstract interpretation provides not only significant advantage in terms of accuracy, but also a gain in performance in comparison to standard techniques.

Introduction

This paper deals with the verification of safety properties about logico-numerical data-flow programs, i.e., programs manipulating Boolean and numerical variables. Verification of such properties amounts to checking whether the reachable state space stays within the invariant specified by the property.

Classical applications are safety-critical controllers as found in modern transport systems, as well as static checking of high-level simulation models, e.g. a model of a production line as depicted in Fig. 1. In such systems the properties to be proved, like throughput and workload, depend essentially on the relationships between the numerical variables of the system. Yet, there is an important observation that we are going to exploit: In many of these control systems large parts of the program simply count time or events, or, more generally, they perform rather regular linear arithmetic operations. Hence, it is appropriate to take advantage of a specialized analysis method that exploits this regularity in order to improve verification performance and precision. In this paper, we will consider abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] for this purpose, which aims at computing in one step the effect of an unbounded number of loop iterations. However, at the same time, we are confronted with a huge Boolean state space in the applications we want to verify. Our contribution is therefore to extend abstract acceleration from purely numerical programs to logico-numerical programs in an efficient way.

Verifying logico-numerical data-flow programs by abstract interpretation. The reachability problem is not decidable for this class of programs, so analysis methods are incomplete. Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] is a classical method with guaranteed termination for the price of an approximate analysis result. The key idea is to approximate sets of states S by elements S ♯ of an abstract domain. A classical abstract domain for numerical invariants in ℘(R n ) is the domain of convex polyhedra P ol(R n ) [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. An approximation S ♯ of the reachable set S is then computed by iteratively solving the fixed point equation characterizing S in the abstract domain. To ensure termination when the abstract domain contains infinitely increasing chains, one applies an extrapolation operator called widening, which induces additional approximations.

Since the analysis with a single abstract value gives only coarse results, it is usually conducted over a control flow graph (CFG) of the program. In the case of imperative programs, such a control graph can be obtained easily by associating control points with programming constructs as if-then-else or while. Data-flow programs do not have such constructs; yet, one can use finite-type variables such as Booleans to generate a control structure. Thus, the classical approach is to explicitly unfold the Boolean control structure by enumerating the Boolean state space and to analyze the numerical variables on the obtained CFG using a numerical abstract domain. The problem is that the analysis becomes intractable with larger programs because the number of control locations grows exponentially with the number of Boolean states.

Jeannet [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF] proposed a method for iteratively refining the control structure and analyzing the system using a logico-numerical abstract domain, making it possible to deal with Boolean variables symbolically. We want to complement this approach with new partitioning techniques and analysis methods.

Abstract acceleration. Acceleration [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF] refers to a set of techniques aiming at exactly computing the effects of loops in numerical transition systems like counter machines, and ultimately at computing the exact reachability set of such systems, usually using Presburger arithmetic. Abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] reformulates these concepts within an abstract interpretation approach: it aims at computing the best correct approximation of the effect of loops in a given abstract domain (currently only convex polyhedra have been considered).

These techniques can analyze only purely numerical programs with a given CFG, of which the size often becomes prohibitively large. Furthermore, they do not consider numerical inputs. In a previous paper [START_REF] Schrammel | Extending abstract acceleration to data-flow programs with numerical inputs[END_REF], we already extended abstract acceleration to numerical inputs.

Contributions. The missing link in the application of abstract acceleration to logico-numerical programs, such as Lustre programs, is an efficient method for (i) building an appropriate CFG without resorting to Boolean state space enumeration, and (ii) analyzing it using abstract acceleration. Our methods allow us to treat these two problems independently of each other.

Inria

Our contributions can be summarized as follows:

1. We propose methods for accelerating self-loops in the CFG of logico-numerical data-flow programs. 2. We define Boolean partitioning heuristics that favor the applicability of abstract acceleration and enable a reasonably precise reachability analysis. 3. We provide experimental results on the use of abstract acceleration enhancing the analysis of logico-numerical programs.

Compared to other approaches, the partitioning heuristics that we propose are based on structural properties of the program, namely the numerical transitions, and thus, they are complementary to most common techniques based on abstract or concrete counter-example refinement. In this paper we consider only partitions of the Boolean state space, in contrast to the tool NBac [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF], which in addition partitions according to numerical constraints.

Organisation of the article. §2 gives an introduction to the abstract interpretation of logico-numerical programs, partitioning, and abstract acceleration.

§3 and §4 describe our contributions on logico-numerical abtract acceleration methods, §5 presents our experimental results, and finally §6 discusses related work and concludes.

       I(b, x) = ¬b ∧ (x = 0) 1 ≤ ξ ≤ 3 →   b ′ x ′   =   (b ∧ x ≤ 5) ∨ β x + ξ if b ∧ x ≤ 5 0 otherwise  
An execution of such a system is a sequence

s 0 i 0 -→ s 1 i 1 -→ . . . s k i k -→ . . . such that I(s 0 ) and for any k ≥ 0, A(s k , i k ) ∧ s k+1 = f (s k , i k )).
The front-end compilation of synchronous data-flow programs, like Lustre, produces such a program model, that also includes various models of counter automata (by emulating locations using Boolean variables) [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF].

We will use the following notations: s = (b, x) : state variable vector, with b Boolean and x numerical subvectors i = (β, ξ) : input variable vector, with β Boolean and ξ numerical subvectors C(x, ξ) : constraints over numerical variables, seen as a vector of Boolean decisions (for short C)

Transitions are written in the form A(b, β, C) → b ′ x ′ = f b (b, β, C) f x (b, β, C, x, ξ)
.

Numerical transition functions are written as a disjunction of guarded actions:

f x (b, β, C, x, ξ) = i g i (b, β, C) → a x i (x, ξ)
with ¬(g i ∧ g j ) for i = j. The program example above conforms to these notations.

Abstract interpretation

The state space induced by logico-numerical programs has the structure E = B m ×R n . As mentioned in the introduction, we adopt the abstract interpretation framework so as to abstract the equation S = S 0 ∪ post (S), S ∈ ℘(E) in an abstract domain and to solve it iteratively, using widening to ensure convergence.

We consider the domain A = ℘(B m ) × P ol(R n ) of convex states [START_REF] Jeannet | Partitionnement Dynamique dans l'Analyse de Relations Linéaires et Application à la Vérification de Programmes Synchrones[END_REF], which approximates a set of states coarsely by a conjunction of a Boolean formula and a single convex polyhedron. For instance the formula

(b ∧ x ≤ 2) ∨ (¬b ∧ x ≤ 4) is abstracted by true ∧ x ≤ 4.
Partitioning the state space. We use state space partitioning to obtain a CFG in which each equivalence class of the partition corresponds to a location. Definition 1. A symbolic control flow graph (CFG) of a symbolic transition system is a directed graph Π, Π 0 , where -Π is the set of locations; each location ℓ ∈ Π is characterized by its location invariant ϕ ℓ (s), such that {ϕ ℓ (s) | ℓ ∈ Π} forms a partition of E. -Π 0 is the set of initial locations with I(s) = ℓ∈Π0 ϕ ℓ (s) -defines arcs between locations according to the transition relation:

∃s, i : ϕ ℓ (s) ∧ A(s, i) ∧ s ′ = f (s, i) ∧ ϕ ℓ ′ (s ′ ) ⇒ ℓ ℓ ′
There are several ways to define a partition inducing such a CFG. In predicate abstraction for instance, the partition is generated by considering the truth value of a finite set of predicates [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF]. Here, we consider partitions defined by equivalence relations on Boolean state variables. For example, the fully partitioned CFG obtained by enumerating all Boolean states is characterized by the relation b

1 ∼ b 2 ⇔ b 1 = b 2 .
Simplifying a CFG. In practice, partitioning is done by incrementally dividing the locations. Furthermore arcs between locations that are proved to be infeasible are removed. This can be done, e.g. by checking the satisfiability of the transition relation, e.g. using an SMT solver. At last, transition functions are simplified by partial evaluation (using a generalized cofactor operator, see [START_REF] Coudert | Verification of synchronous sequential machines based on symbolic execution[END_REF]).

Analyzing a CFG. In the context of analysis by abstract interpretation, considering a CFG allows to apply widening in a more restrictive way, e.g. on loop heads only [START_REF] Bourdoncle | Efficient chaotic iteration strategies with widenings[END_REF]. Also the information loss due to the convex union is limited, because we assign an abstract value to each location: We consider the compound abstract domain (Π → A) where the concrete states S are connected to their abstract counterparts S ♯ by the Galois connection:

Inria c τ =⇒ c ′ c ′′ τ ⊗
S ♯ = α(S) = λℓ . α(S ⊓ ϕ ℓ ) S = γ(S ♯ ) = ℓ∈Π γ(S ♯ ℓ )
Analyzing the partitioned system amounts to computing the least fixed point S ♯ = S ♯,0 ⊔ λℓ .

ℓ ′ ∈Π post (S ♯ ℓ ′ ) ⊓ ϕ ℓ where S ♯ , S ♯,0 ∈ (Π → A).

Abstract acceleration

As mentioned in the introduction, acceleration [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF] aims at computing exactly (or precisely in the case of abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF]) the effect of a self-loop. The basic idea is to replace a loop transition by its transitive closure (Fig. 2) by providing a formula τ ⊗ (X) computing τ * (X) = k≥0 τ k (X).

Basic concepts. A loop transition τ has the structure: g → a meaning "while guard g do action a". Our extension of abstract acceleration to numerical inputs [START_REF] Schrammel | Extending abstract acceleration to data-flow programs with numerical inputs[END_REF] deals with loop transitions of the form

A L 0 J x ξ ≤ v k Ax+Lξ≤v ∧ Jξ≤k → x ′ = C T x ξ + u Cx+Tξ+u (1)
Existing acceleration methods can deal with transitions where the matrix C is a diagonal matrix with zeros and ones only or when it is periodic (∃p > 0, l > 0 : C p+l = C p ). Throughout this paper, we will call such numerical transition functions accelerable, whereas we regard general affine transformations (with an arbitrary C) as non-accelerable.

Widening and acceleration. Acceleration gives us a formula for computing the transitive closure of accelerable loop transitions. Widening is still needed in the case of non-accelerable transitions, outer loops of nested loops and to guarantee convergence when there are multiple self-loops in the same control location (see the concept of flat systems in [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]). The main advantages of abstract acceleration in comparison with widening result from two properties:

-Idempotency (τ ⊗ (X) = τ ⊗ (τ ⊗ (X)))
, which simplifies the fixed point computation (widening usually requires more than one step to stabilize);

-Monotonicity X 1 ⊑ X 2 ⇒ τ ⊗ (X 1 ) ⊑ τ ⊗ (X 2 )
, that makes the analysis more robust and predictible (whereas widening operators are not monotonic).

Classical application of abstract acceleration

We describe now the classical way to apply abstract acceleration to the analysis of logico-numerical programs, for which this paper proposes major enhancements.

b 1 ¬b 1 b 0 ∧ x 1 = 0∧ x 2 = 0 x 1 ≤ 9 → x 1 + +; x 2 + + x 1 ≤ 9 → x 1 + +; x 2 + +; b 2 := ¬b 2 x 1 > 9 → x 1 := 0; b 1 := ¬b 1 x 1 > 9 → x 1 := 0; x 2 := 0; b 1 := ¬b 1
Fig. 3: Self-loop ready to be accelerated (left). Acceleration not applicable (right). Example 1. We will try to infer invariants on the following running example:

b 0 ∨ ¬b 1 τ (a) Initial CFG ¬b 0 ∧ ¬b 1 b 0 ∧ ¬b 1 b 0 ∧ b 1 x 0 ≤ 10 → x ′ 0 = x 0 + 1; x ′ 2 = x 2 + 1 x 1 ≤ 10 → x ′ 1 = x 1 + 1; x ′ 2 = x 2 + 1 x 0 > 10 ∧ x 1 > 10 → x ′ 0 = 0 x 0 ≤ 20 → x ′ 0 = x 0 + 1; x ′ 2 = x 2 + 1 x 0 > 20 → x ′ 2 = x 2 + 1 (
I(b, x) = ¬b0 ∧ ¬b1 ∧ x0 = 0 ∧ x1 = 0 ∧ x2 = 0 true →                            b ′ 0 = b0 ∨ (¬b0 ∧ x0 > 10 ∧ x1 > 10) b ′ 1 = b1 ∨ (¬b1 ∧ x0 > 20) x ′ 0 =    x0 + 1 if (¬b0 ∧ ¬b1 ∧ x0 ≤ 10 ∧ β) ∨ (b0 ∧ ¬b1 ∧ x0 ≤ 20) 0 if ¬b0 ∧ ¬b1 ∧ x0 > 10 ∧ x1 > 10 x0 otherwise x ′ 1 = x1 + 1 if ¬b0 ∧ ¬b1 ∧ x1 ≤ 10 ∧ ¬β x1 otherwise x ′ 2 = x2 + 1 if (¬b0 ∧ ¬b1 ∧ (x0 ≤ 10 ∧ β ∨ x1 ≤ 10 ∧ ¬β)) ∨ (b0 ∧ ¬b1) x2 otherwise
The counting patterns of this example (see Fig. 4b) are representative of the production line benchmarks presented in Section 5.

Numerical acceleration can be applied to self-loops where the numerical state evolves while the Boolean state does not, i.e. the Boolean part of the transition function is the identity (see Fig. 3 for an example and a counterexample):

Definition 2 (Accelerable logico-numerical transition). A transition τ is accelerable if it has the form g b (b, β) ∧ g x (C) → b ′ x ′ = b a(x, ξ) , where g x (C) → x ′ = a(x, ξ) is accelerable.
Generating a numerical CFG. At first, one performs a Boolean reachability analysis in order to reduce the state space of interest (b 0 ∨ ¬b 1 in the case of our Inria running example). Starting from the most simple CFG of the program consisting of a single location with a self-loop (see Fig. 4a), standard techniques are used for (1) enumerating the Boolean state space and (2) simplifying the transitions by source and destination location using partial evaluation. Afterwards, (3) the Boolean input variables are replaced by explicit non-deterministic transitions (see Fig. 4b). This CFG is purely numerical, but the guards of the loop transitions might still be non-convex. Transforming the guard into a minimal DNF and splitting the transition into several transitions, one for each conjunct, yields a CFG with self-loops compatible with the transition scheme of §2.2. A single selfloop like in location b 0 ∧ ¬b 1 in Fig. 4b can now be "flattened" into a transitive closure transition (cf. Fig. 2).

Multiple self-loops. However, the obtained CFG usually contains multiple self-loops like in location ¬b 0 ∧ ¬b 1 in Fig. 4b. In this case a simple "flattening" as in Fig. 2 is not possible: For the fixed point computation we must take into account all sequences of self-loop transitions in this location. Actually, the idempotency of accelerated transitions can be exploited in order reduce these sequences to those where the same transition is never taken twice successively: For the two accelerable loops we have to compute:

τ ⊗ 1 (X)⊔τ ⊗ 2 (X)⊔τ ⊗ 2 •τ ⊗ 1 (X)⊔τ ⊗ 1 •τ ⊗ 2 (X)⊔τ ⊗ 1 •τ ⊗ 2 •τ ⊗ 1 (X)⊔τ ⊗ 2 •τ ⊗ 1 •τ ⊗ 2 (X)⊔.
. . This infinite sequence may not converge, thus in general, widening is necessary to guarantee termination. However, in practice the sequence often converges after the first few elements (see [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]).

The technique implemented in Aspic consists in expanding multiple selfloops into a graph of which the paths represent these sequences, as shown in Fig. 5 in the case of three self-loops, and to solve iteratively the fixed point equations induced by the CFG as sketched in §2.1, using widening if necessary. Moreover, Aspic implements methods to accelerate circuits of length greater than one.

Logico-Numerical Abstract Acceleration

Our goal is to exploit abstract acceleration techniques without resorting to a Boolean state space enumeration in order to overcome the limitations of current tools (e.g. [START_REF] Gonnord | The ASPIC tool: Accelerated symbolic polyhedral invariant computation[END_REF]) w.r.t. the analysis of logico-numerical programs.

In this section, we will first discuss some related issues in order to motivate our approach, before presenting methods that make abstract acceleration applicable to a CFG that now may contain loops with operations on both, Boolean and numerical, variables.

Motivations for Our Approach

A first observation is that identifying self-loops is more complex when Boolean state variables are not fully encoded in the CFG. Indeed, if a CFG contains a "syntactic" self-loop (ℓ, τ, ℓ) with τ : g(b, x, ξ) → (b ′ , x ′ ) = f (b, x, ξ), there is an "effective" self-loop only for those Boolean states b ∈ ϕ ℓ in location ℓ such

i 1 2 3 o τ i τ i τ i τ o τ o τ o τ ⊗ 1 τ ⊗ 2 τ ⊗ 1 τ ⊗ 3 τ ⊗ 2 τ ⊗ 3
Fig. 5: Computation of three accelerable self-loops τ 1 , τ 2 and τ 3 . τ i and τ o are the incoming resp. outgoing transitions of the location.

b 0 ∨ ¬b 1 τ 1 : ¬b 0 ∧ ¬b 1 ∧ x 0 ≤ 10 → x ′ 0 = x 0 + 1; x ′ 2 = x 2 + 1 τ 2 : ¬b 0 ∧ ¬b 1 ∧ x 1 ≤ 10 → x ′ 1 = x 1 + 1; x ′ 2 = x 2 + 1 τ 3 : b 0 ∧ ¬b 1 ∧ x 0 ≤ 20 → x ′ 0 = x 0 + 1; x ′ 2 = x 2 + 1 τ r
Fig. 6: Acceleration of Ex. 1 in a CFG with a single location: The upper three self-loops are accelerable. The rest of the system is summarized in the transition τ r where the Boolean equations are not the identity. that g(b, x, ξ) ∧ b = f b (b, x, ξ) is satisfiable1 . For instance, the self-loop around location ¬b 1 in Fig. 3 is not an "effective" self-loop. This observation also applies to circuits, where, moreover, numerical inputs have to be duplicated

: If there is a circuit (ℓ, τ 1 , ℓ ′ ) and (ℓ ′ , τ 2 , ℓ) with τ i : g i (s, ξ) → s ′ = f i (s, ξ) for i = 1, 2, the composed transition has the form τ : g(s, ξ, ξ ′ ) → s ′′ = f (s, ξ, ξ ′ ).
This limits in practice the length of circuits that can be accelerated. Here, we will not deal with such circuits and we focus on self-loops.

A naive approach to our problem could be to partition the system into sufficiently many locations, until we get self-loops that correspond to Def. 2. This approach is simple-minded for two reasons: (i) There might be no such Boolean states in the program at all; (ii) in the case of Fig. 3, simply ignoring the Boolean variable b 2 would make the (syntactic) self-loop accelerable without impacting the precision. More generally, it may pay off to slightly abstract the behavior of self-loops in order to benefit from precise acceleration techniques rather than relying on widening which may lose much more information in the end.

Another important remark is that we do not necessarily need to partition the system into locations to apply acceleration: it is sufficient to decompose the selfloops: Starting from the basic CFG with a single location and a single self-loop, we could split the loop into self-loops where the numerical transition function can be accelerated and the Boolean transition is the identity and a last self-loop where this is not the case. Fig. 6 shows the result of the application of this idea to our running example of Fig. 4. This allows us to separate the issue of accelerating self-loops in a symbolic CFG, addressed in this section, from the issue of finding a suitable CFG, addressed in §4.

τ ⊆ τ * x π • τ b (Prop. 1) ⊆ π • τ * x • π π • τ b (Prop. 2)
Fig. 7: Decoupling numerical and Boolean transitions

Decoupling Numerical and Boolean Transition Functions

We consider self-loops (ℓ, τ, ℓ) with τ :

g(s, i) → b ′ x ′ = f b (s, i) f x (s, i) without
any restriction on f b . We use the abstraction

℘(E) = ℘(B m ×R n ) ---→ ← --- π id ℘(B m )× ℘(R n ),
where π is the function that approximates a set S ∈ E by a Cartesian product, e.g. π((

B 1 ×X 1 )∪(B 2 ×X 2 )) = (B 1 ∪B 2 )×(X 1 ∪X 2 ). If τ is accelerable in the sense of abstract acceleration, then π • τ * ⊆ τ ⊗ .
Our logico-numerical abstract acceleration method relies on decoupling the numerical and Boolean parts of the transition function τ with

τ b : g(s, i) → b ′ x ′ = f b (s, i) λ(s, i). x and τ x : g(s, i) → b ′ x ′ = λ(s, i). b f x (s, i) .
We can approximate τ * as follows (Fig. 7):

Proposition 1. τ * ⊆ (π • τ b • τ * x ) * . Proof. We prove first τ ⊆ π • τ b • (id ∪ τ x ): Let S = {(b, x)}, then τ b (S) = {(b ′ , x)}, τ x (S) = {(b, x ′ )}, and τ (S) = {(b ′ , x ′ )}: {(b, x), (b, x ′ )} ⊆ (id ∪ τ x )(S) = S ′ ⇒ {(b ′ , x), (b ′′ , x ′ )} ⊆ τ b (S ′ ) = S ′′ with {(b ′′ , x ′ )} = τ b ({(b, x ′ )}) ⇒ {(b ′ , x ′ )} ⊆ π(S ′′ ) = S ′′′
The graphical intuition of these steps is depicted in Fig. 8. We conclude by

τ ⊆ π • τ b • (id ∪ τ x ) ⇒ τ ⊆ π • τ b • τ * x (because of (id ∪ τ x ) ⊆ τ * x ) ⇒ τ * ⊆ (π • τ b • τ * x ) *
Now, we assume that τ x is accelerable in the sense of Def. 2, which implies that g(s, i) = g b (b, β) ∧ g x (x, ξ) and f x (s, i) = a(x, ξ). By applying Prop. 1, we obtain that (π

• τ b • τ ⊗
x ) * is a sound over-approximation of τ * . However, this formula still involves Kleene iteration and thus widening is required.

But, there exists an alternative in which numerical and Boolean parts are computed in sequence, so that numerical acceleration is applied only once (Fig. 7): If τ x is accelerable, then

x b x ′ b ′ b ′′ τ (S) S ′ S ′′ S ′′′
(1) (π • τ b ) * • π • τ * x • π is idempotent, and (2) τ * ⊆ (π • τ b ) * • π • τ * x • π
Proof. The intuition for (1) is the following: If the guard g x ∧ g b is satisfied, i.e., the transition can be taken, then we compute first the transitive closure w.r.t. the numerical states before saturating the Boolean states. The application of τ b does not enable "more" behavior of the numerical variables; hence, re-applying the τ * x has no effect. We first compute (π

• τ b ) * • π • τ * x • π(S): π(S) = B ×X τ * x • π(S) = (B ×X) ∪ (B ∩ (∃β : g b ))×X ′ with X ′ s.t. (∃ξ : a((X ∪X ′ ) ∩ g x )) ⊆ X ′ (i) S ′ = π • τ * x • π(S) = B ×(X ∪X ′ ) (π • τ b ) * • π • τ * x • π(S) = S ′ ∪ S ′′ B ′ ×((X ∪X ′ ) ∩ (∃ξ : g x )) where B ′ = k≥1 τ k b (B, (X ∪ X ′ ) ∩ (∃ξ : g x ))
and with the property

(π • τ b )(S ′ ∪ S ′′ ) ⊆ S ′′ (ii) S ′′′ = (π • τ b ) * • π • τ * x • π(S) = (B ∪B ′ )×(X ∪X ′ )
Fig. 9 illustrates the sets S, S ′ , and S ′′′ . S ′′′ is obviously stable by application of π. We show that it is also stable by application of τ x and π • τ b , which allows to conclude that (π

• τ b ) * • π • τ * x • π(S ′′′ ) = S ′′′
, hence the idempotency of the function:

τ x (S ′′′ ) = ((B ∪B ′ ) ∩ (∃β : g b ))×X ′′ with X ′′ ⊆ X ′ because of property (i) above, hence τ x (S ′′′ ) ⊆ S ′′′ , and π • τ * x (S ′′′ ) = S ′′′ π • τ b (S ′′′ ) = π • τ b (S ′′′ ∩ (B m ×(∃ξ : g x ))) = π • τ b ((B ∪B ′ ) × ((X ∪X ′ ) ∩ (∃ξ : g x ))) ⊆ π • τ b (S ′ ∪S ′′ ) ⊆ S ′′′ according to property (ii). Inria b ′ 1 ∧ b ′ 2 ∧ x ′ = 0 x ≥ 2 → id τ : x < 2 →    x ′ = x+1 b ′ 1 = (b2 ∧ x = 0) b ′ 2 = (b1 ∧ ¬b2 ∧ x = 1) ¬b 1 b 1 ¬b 2 / x = 0 b 2 x = 1 x = 2
τ * ⊆ (π • τ b • τ * x ) * = ((π • τ b ) * • τ * x ) * ⊆ ((π • τ b ) * • π • τ * x • π) * = (π • τ b ) * • π • τ * x • π.
For the last step, we use the idempotency of the function and the fact that it includes the identity.

⊓ ⊔ Remark 1 (Why not τ * b ?). We cannot compute Boolean iterations exactly using τ * b instead of (π•τ b ) * . Fig. 10 gives a counterexample where τ * π•τ * b •π•τ * x •π, which shows that using exact iterations τ * b would not give a sound decoupling.

The following theorem implements Prop. 2 in the logico-numerical product domain A with the Galois connection

℘(B m × R n ) ---→ ← --- α id ℘(B m ) × P ol(R n ).
Theorem 1 (Logico-numerical abstract acceleration). If a transition τ is such that τ x is accelerable, then τ * can be approximated in the logico-numerical product domain A with

τ ⊗ (B, X) = τ b b X ⊗ * (B) , X ⊗ where -X ⊗ = (τ x x ) ⊗ (X) -(τ x x ) ⊗ is the abstract acceleration of τ x x : g x (x, ξ) → x ′ = a(x, ξ) -τ b b [X](B) = τ b (B, X ⊗ ⊓ g (∃ξ : g x )) -(τ b b [X]) * (B) = lfp(λB ′ . B ∪ τ b b [X](B ′ )). (τ b b [X]
) * converges in a finite number of iterations as it is the least fixed point of a monotonic function in the finite lattice ℘(B m ).

In other words, we compute the reflexive and transitive closure X ⊗ of τ x using numerical abstract acceleration and saturate τ b partially evaluated over X ⊗ .

Proof. We prove that τ ⊗ (S) over-approximates the result of the formula of Prop. 2, i.e. ((π

• τ b ) * • π • τ * x • π)(S) ⊆ τ ⊗ • α(S) with S ⊆ ℘(B m × R n ).
This over-approximation is due to the convex approximations by the numerical abstract domain

Pol (R n ). (π • τ b ) * • π • τ * x • π(S) = ( k≥0 τ k b (B, (X ∪ X ′ ) ∩ (∃ξ : g x )) , X ∪ X ′ ) with π(S) = (B, X) and X ′ s.t. (∃ξ : a((X ∪X ′ ) ∩ g x )) ⊆ X ′ (see proof of Prop. 2) ⊆ λ(B, X). k≥0 τ k b (B, X ⊗ ⊓ g (∃ξ : g x )) , X ⊗ ) • α(S)
with τ x x = λX.∃ξ : a(X ∩ g x ) due to the soundness of numerical abstract acceleration:

(X ∪ X ′ ) ⊆ (τ x x ) ⊗ • α(X) = X ⊗ = λ(B, X).((τ b b [X ⊗ ](B)) * , X ⊗ ) • α(S) with the notation τ b b [X](B) = τ b (B, X ⊓ g (∃ξ : g x ))
Then, by τ * (S) ⊆ ((π

• τ b ) * • π • τ * x • π)(S) (Prop. 2), we conclude τ * (S) ⊆ τ ⊗ • α(S). ⊓ ⊔
Mind that, due to the convex approximation of the numerical sets, τ ⊗ is not idempotent in general (cf. [START_REF] Leroux | Acceleration in convex data-flow analysis[END_REF]).

Discussion

At the first glance, the approximations induced by this partial decoupling seem to be rather coarse. However, this is not severe in our context for two reasons:

1. The relations between Boolean and numerical variables that are lost by our method are mostly not representable in the abstract domain A anyway. For example, consider the loop x ≤ 4 → (b ′ = ¬b; x ′ = x+1), where b could be the least significant bit of a binary counter for instance: starting from (b, x) ∈ {(true, 0)} the exact reachable set is {true} × {0, 2, 4} ∪ {false} × {1, 3, 5}; its abstraction in A is {⊤} × {0 ≤ x ≤ 5}. Hence, these relations will also be lost in a standard analysis merely relying on widening. Yet, due to numerical acceleration, we can even expect a better precision with our method. 2. We will apply this method to CFGs (see §4) in which the Boolean states defining a location exhibit the same numerical behavior and thus, decoupling is supposed not to seriously affect the precision.

Until now we studied the case of a single self-loop. In the presence of multiple self-loops, we expand the graph in the same way as with purely numerical transitions, e.g., as shown in Fig. 5, and we apply Thm. 1 to each loop. As in the purely numerical case, widening must be applied in order to guarantee convergence.

Example 2. We give the results obtained for Ex. 1: Analyzing the enumerated CFG in Fig. 4b using abstract acceleration gives 0

≤ x 0 ≤ 21∧ 0 ≤ x 1 ≤ 11∧ Inria x 0 + x 1 ≤ x 2 ≤
44 bounding all variables2 . Analyzing the system on a CFG with a single location using decoupling and abstract acceleration still bounds two variables (0 ≤ x 0 ≤ 21 ∧ 0 ≤ x 1 ≤ 11 ∧ x 0 + x 1 ≤ x 2 ), whereas, even on the enumerated CFG a standard analysis does not find any upper bound at all:

0 ≤ x 0 ∧ 0 ≤ x 1 ∧ x 0 + x 1 ≤ x 2 .

Variants

Decoupling accelerable from non-accelerable and Boolean transition functions. Theorem 1 applies only if the numerical transition functions are accelerable. If this is not the case, we can reuse the idea of Prop. 1, but now by decoupling the accelerable numerical functions (marked by the sub/superscript a) from Boolean and non-accelerable numerical functions (sub/superscripts b and n respectively):

τ a : g(s, i) →   b ′ x ′ n x ′ a   =   λ(s, i). b λ(s, i). x n a(x, ξ)   , τ n,b : g(s, i) →   b ′ x ′ n x ′ a   =   f b (s, i) f n (s, i) λ(s, i).
τ * ⊆ (π • τ n,b • τ * a ) * ⊆ (π • τ n,b • τ ⊗ a ) *
However, we cannot remove the Kleene iteration as in Prop. 2, because the function τ a depends on non-accelerated numerical variables updated by τ n,b , and hence, widening is needed.

Using inputization techniques. Inputization (see [START_REF] Bres | State abstraction techniques for the verification of reactive circuits[END_REF] for instance) is a technique that treats some state variables as input variables. This method is useful to cut dependencies between the state variables, and thus, to remove loops. For example, it can be employed to reduce (π

• τ b ) * • π to π • τ ′ b • π in Prop. 2,
τ b : b ′ 0 = ¬b0 b ′ 1 = b1 b ′ 2 = b2 ∧ x ≥ 0 τ ′ b : b ′ 0 = β0 b ′ 1 = b1 b ′ 2 = β2 ∧ x ≥ 0
In our experiments ( §5) we observed that the speed-up gained often pays off in comparison to the approximations it brings about.

Partitioning Techniques

The logico-numerical acceleration method described in the previous section can be applied to any CFG. However, in order to make it effective we apply it to a CFG obtained by a partitioning technique that aims at alleviating the impact of decoupling Boolean and numerical transition functions on the precision. This section proposes such partitioning techniques that generate CFGs in which those Boolean states that exhibit the same numerical behavior ("numerical modes") are grouped in the same locations.

Basic technique. In order to implement this idea we generate a CFG that is characterized by the following equivalence relation:

Definition 3 (Numerical modes). b 1 ∼ b 2 ⇔        ∀β 1 , C : A(b 1 , β 1 , C) ⇒ ∃β 2 : A(b 2 , β 2 , C) ∧ f x (b 1 , β 1 , C) = f x (b 2 , β 2 , C) ∧∀β 2 , C : A(b 2 , β 2 , C) ⇒ ∃β 1 : A(b 1 , β 1 , C) ∧ f x (b 1 , β 1 , C) = f x (b 2 , β 2 , C)
The intuition of this heuristics is to make equivalent the Boolean states that can execute the same set of numerical actions, guarded by the same numerical constraints.

Example 4 (Numerical modes). We illustrate the application of this method to Example 1. We first factorize the numerical transition functions by actions:

(x ′ 0 , x ′ 1 , x ′ 2 ) =            (x 0 +1 , x 1 , x 2 +1) if (¬b 0 ∧ ¬b 1 ∧ x 0 ≤ 10) ∨ (b 0 ∧ ¬b 1 ∧ x 0 ≤ 20) ( x 0 , x 1 +1 , x 2 +1) if ¬b 0 ∧ ¬b 1 ∧ x 1 ≤ 10 ( 0 , x 1 , x 2 ) if ¬b 0 ∧ ¬b 1 ∧ x 0 > 10 ∧ x 1 > 10 ( x 0 , x 1 , x 2 +1) if b 0 ∧ ¬b 1 ∧ x 0 > 20 ( x 0 , x 1 , x 2 ) otherwise
Then by applying Def. 3, we get the equivalence classes

{¬b 0 ∧ ¬b 1 , b 0 ∧ ¬b 1 , b 0 ∧ b 1 }: the obtained CFG is the one of Fig. 4b.
In the worst case, as in Ex. 4 above, a different set of actions can be executed in each Boolean state, thus the Boolean states will be enumerated. In the other extreme case, in all Boolean states the same set of actions can be executed, which induces a single equivalence class. Both cases are unlikely to occur in larger, real systems.

From an algorithmic point, we vectorize the numerical actions and factorize their common guards, which is equivalent to computing the product of the MtBdds representing the numerical transition functions:

f x (b, β, C, x, ξ) = 1≤i≤m g i (b, β, C) → a i (x, ξ)
Then we eliminate the Boolean inputs β, and we decompose the results as follows

(∃β : g i (b, β, C)) = 1≤j≤ni g b ij (b) ∧ g x ij (C)
Inria where g x ij (C) may be non-convex. The equivalence relation ∼ of Def. 3 can be reformulated as

b 1 ∼ b 2 ⇐⇒ ∀i∀j : g b ij (b 1 ) ⇔ g b ij (b 2
). This last formulation reflects the fact that, in the resulting CFG, the numerical function f x specialized on a location ℓ does not depend any more on b, and hence, the precision loss is supposed to be limited.

Reducing the size of the partition. An option for having a less discriminating equivalence relation is to make equivalent the Boolean states that can execute the same set of numerical actions regardless of the numerical constraints guarding them.

Definition 4 (Numerical modes (forgetting numerical guards)).

b 1 ≈ b 2 ⇔    ∀β 1 , C 1 : A(b 1 , β 1 , C 1 ) ⇒ ∃β 2 , C 2 : A(b 2 , β 2 , C 2 ) ∧ f x (b 1 , β 1 , C 1 ) = f x (b 2 , β 2 , C 2 )

and vice versa

We clearly have ∼⊆≈. For example, if we have two guarded actions b ∧ x ≤ 10 → x ′ = x + 1 and ¬b ∧ x ≤ 20 → x ′ = x + 1, ∼ will separate the Boolean states satisfying resp. b and ¬b, whereas ≈ will keep them together.

Another option is to consider only a subset of the numerical actions, that is, we ignore the transition functions of some numerical variables in Defs. 3 or 4. One can typically focus only on variables involved in the property. According to our experiments, this method is very efficient, but it relies on manual intervention.

Refining the partition by backward bisimulation. Given a partition, it can be refined by Boolean backward bisimulation (cf. [START_REF] Bouajjani | Minimal model generation[END_REF]).

Definition 5 (Boolean backward bisimulation). Given an equivalence relation ∼, its backward Boolean bisimulation equivalence ∼ ∞ is defined by

b 1 ∼ 0 b 2 ⇔ b 1 ∼ b 2 ∧ (I(b 1 ) = I(b 2 )) b 1 ∼ k+1 b 2 ⇔    ∀β 1 , C 1 , b ′ 1 such that A(b ′ 1 , β 1 , C 1 ) ∧ b 1 = f b (b ′ 1 , β 1 , C 1 ) : ∃b ′ 2 , β 2 , C 2 : A(b ′ 2 , β 2 , C 2 ) ∧ b 2 = f b (b ′ 2 , β 2 , C 2 ) ∧ b ′ 1 ∼ k b ′ 2

and vice versa

The rationale behind this refinement is that partitioning the state space with Def. 3 (∼) and stabilizing it by backward bisimulation yields a CFG with locations that group together states that are reachable (in the graph sense) by the same sequence of numerical actions from an initial state.

Experimental Evaluation

We have implemented the proposed methods in our experimentation tool ReaVer3 on the basis of the logico-numerical abstract domain library BddApron.

Benchmarks. Besides some small, but difficult benchmarks, we used primarily benchmarks that are simulations of production lines (see Fig. 1), as modeled with the library Quest for the LCM language4 , for evaluating scalability. These models consist of building blocks like sources, buffers, machines, routers for splitting and combining flows of material and sinks, that synchronize via handshakes. The properties we want to prove depend on numerical variables, e.g. (1) maximal throughput time of the first element passing the production line, or (2) minimal throughput of the production line. Inputs could model non-deterministic processing and arrival times, but we did not choose benchmarks with numerical inputs in order to enable a comparison with Aspic [START_REF] Gonnord | The ASPIC tool: Accelerated symbolic polyhedral invariant computation[END_REF].

Results. We compared our tool ReaVer with NBac [START_REF] Jeannet | Dynamic partitioning in analyses of numerical properties[END_REF][START_REF] Jeannet | Partitionnement Dynamique dans l'Analyse de Relations Linéaires et Application à la Vérification de Programmes Synchrones[END_REF][START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF] and Aspic.

The results are summarized in Table 1. The tools where launched with the default options; for ReaVer we use the partitioning heuristics of Def. 4 and the inputization technique of §3.4. We do not need the decoupling technique of Prop. 3 for our examples.

Discussion. The experimental comparison gives evidence about the advantages of abstract acceleration, but also some potential for future improvement:

-ReaVer can prove a lot of examples where NBac fails: this is due to the fact that abstract acceleration improves precision, especially in nested loops where the innermost loop can be "flattened", which makes it possible to recover more information in descending iterations. -ReaVer seems to scale better than NBac: First, abstract acceleration reduces the number of iterations and fixed point checks. Second, our heuristics generates a partition that is well-suited for analysis -though, for some of the larger benchmarks, e.g. LCM quest 4-1, the dynamic partitioning of NBac starts to pay off, whereas our static partition is more fine-grained than necessary, which makes us waste time during analysis. -Once provided with an enumerated CFG, Aspic is very fast on the smaller benchmarks. However, the current version (3.1) cannot deal with CFGs larger than a few hundred locations. We were surprised that some of the small examples were not proved by Aspic. We found out that this is due to our fixed point iteration strategy that uses a higher widening delay in strongly connected components resulting from the unfolding of multiple self-loops. -The analysis using logico-numerical acceleration proved twice as many benchmarks and turned out to be 20% faster than a standard analysis of the same CFG with widening with delay 2 and two descending iterations. -Applying the more refined partition of Def. 3 to our benchmarks had only a minor influence on performance and precision, and not applying inputization had no impact on the verification of properties, but it slowed down the analysis by 25% on average. -Generally, for the benchmarks LCM quest 1 to 4, property 2 was not proved by the tools. Here, the combination of our heuristics with dynamic partitioning for further refining the critical parts of the CFG could help.

Conclusions

We proposed techniques for accelerating logico-numerical transitions, that allow us to benefit from the precision gain by numerical abstract acceleration as used in the tool Aspic, while tackling the Boolean state space explosion problem encountered when analyzing logico-numerical programs. Experimentally, our tool ReaVer is often able to prove properties for the larger benchmarks, unlike the two other tools we tested -and this on CFGs that are ten times smaller than the CFGs obtained by enumeration of the reachable Boolean state space.

Although our method is based on the partial decoupling of the Boolean and numerical transitions, the experiments confirm our intuition that our method generally improves the precision. We attribute this to the following observations: first, numerical abstract acceleration reduces the need for widening; second, the information that we might lose by decoupling would often not be captured by the abstract domain anyway; and at last, the CFG obtained by our partitioning method particularly favors the application of our logico-numerical acceleration method.

Perspectives. Regarding abstract acceleration, the acceleration of multiple self-loops deserves additional investigation: We explained that, in case of nested loops, we have to resort to widening in order to guarantee convergence. Multiple self-loops, i.e. several self-loops around one location, are a special case of nested loops. Gonnord et al [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF] developed abstract acceleration formulas for some special cases of multiple self-loops. In the general case, they apply a graph transformation method based on a partial unfolding (see §2.3) in order to compute more precise fixed points of multiple self-loops. However, this graph transformation is costly since it transforms 1 location with n self-loops into n locations with n(n-1) arcs.

In the context of applying Presburger-based acceleration to program parallelization, Beletska et al. [START_REF] Beletska | Computing the transitive closure of a union of affine integer tuple relations[END_REF] propose an interesting approach which avoids this problem: for multiple self-loops τ i = g i → a i , they do not compute ( i τ i (X)) * , but they use the more efficient, though less precise formula: i τ i j a j (X) *

. This computation scheme resembles the one of the derivative closure method of Ancourt et al. [START_REF] Ancourt | A modular static analysis approach to affine loop invariants detection[END_REF]. This approach could be considered to improve the abstract acceleration of multiple self-loops. Concerning partition refinement, the combination of our approach with dynamic partitioning à la [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF] seems to be worth pursuing. In particular, partitioning according to numerical constraints is mandatory for proving properties relying on non-convex invariants -our partitioning techniques partition only the Boolean state space. Such improvements should allow a wider range of benchmarks to be tackled.

Related Work. To our knowledge there is no work about the application of abstract acceleration to logical-numerical data-flow programs, but there is work on related methods that we tailored to fit our purpose. In §2 we already discussed in detail the concepts of abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF], on which our work is based, and that we extended in [START_REF] Schrammel | Extending abstract acceleration to data-flow programs with numerical inputs[END_REF].

Jeannet [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF] uses in the tool Nbac partitioning heuristics that are based on the property being analyzed in order to cut paths between initial and bad states. The tool interleaves partitioning steps with analysis (dynamic partitioning), thus the "dangerous" state space is reduced in each step. Bouajjani et al. [START_REF] Bouajjani | Minimal model generation[END_REF] describe a partition refinement algorithm for the Lustre compiler using bisimulation. We think that we could exploit it to refine our CFG, when we fail to prove the property.

Alternative approaches for verifying properties about data-flow programs rely on bounded model-checking or k-induction techniques, which both exploit the efficiency of modern SMT solvers. Hagen and Tinelli [START_REF] Hagen | Scaling up the formal verification of Lustre programs with SMT-based techniques[END_REF] describe the application of these two approaches to the verification of Lustre programs. Another example is the HySat tool [START_REF] Fränzle | Hysat: An efficient proof engine for bounded model checking of hybrid systems[END_REF], a bounded model-checker for hybrid systems with piecewise linear behavior -our methods allow to analyze discretizations of such systems. HySat relies on the integration of linear constraint solving with SAT solving. The interesting point is that they deal implicitly with large Boolean control structures by encoding them into linear pseudo-Boolean constraints.

Fig. 1 :

 1 Fig. 1: Example of a production line with buffers, machines, and splitting and combining material flows.

Fig. 2 :

 2 Fig. 2: Self-loop transition (left) and accelerated transition (right).

Fig. 4 :

 4 Fig. 4: Transformation of the program of Example 1. τ is the global transition. The guards are already convex in the obtained CFG.

Fig. 8 :Fig. 9 :

 89 Fig. 8: Illustration of the proof of Prop. 1

Fig. 10 :

 10 Fig. 10: CFG of a counterexample (left-hand side) to show why the Boolean iterations cannot be computed exactly: the state (false, true, 2) contained in τ * ({(true, true, 0)}) = {(true, true, 0), (true, false, 1), (false, true, 2)} (dots in the right-hand side figure) is not part of π • τ * b • π • τ * x • π({(true, true, 0)}) = {(true, true), (true, false), (false, false)} × {0, 1, 2}.

Proposition 3 (

 3 Decoupling accelerable and non-accelerable transitions).

  where τ ′ b is obtained by inputizing in τ b those Boolean state variables that have a transition function that is neither the identity nor constant. Example 3 (Inputization). The loop τ b can be approximated by the transition τ ′ b where β 0 and β 2 correspond to b 0 and b 2 manipulated as Boolean inputs:

Table 1 :

 1 -1 7/2/0 7 0.04 (0.01) 5 0.04 5 0.05 LCM Quest 0a-2 7/3/0 6 0.05 (0.01) 4 0.05 8 0.19 LCM Quest 0b-1 10/3/0 19 0.08 (0.01) 12 0.08 9 ? LCM Quest 0b-2 10/4/0 17 0.09 (0.01) 11 0.20 33 ? LCM Quest 0c-1 15/4/0 28 0.17 (0.01) 16 0.16 8 0.86 LCM Quest 0c-2 15/5/0 25 0.20 (0.05) 14 0.24 50 14.8 LCM Quest 1-1 16/5/0 114 1.99 (0.48) 42 0.92 6 Experimental comparison between Aspic, ReaVer and Nbac.

			Aspic	ReaVer	Nbac
			vars size	time	size time size time
		Gate 1	4/4/2 7	?	5 0.73 24	?
		Escalator 1	5/4/2 12 0.14 (0.04) 9 0.49 22	?
		Traffic 1	4/6/0 18 0.14 (0.01) 16 0.19	5	3.49
		Traffic 2	4/8/0 18	?	16 0.35 28	?
		LCM Quest 0a2.45
		LCM Quest 1-2 16/6/0 100	?	34 ? >156 >
		LCM Quest 1b-1 16/5/0 55 0.92 (0.04) 29 0.37 15	?
		LCM Quest 1b-2 16/5/0 45 0.76 (0.12) 23 0.47 61	?
		LCM Quest 2-1 17/6/0 247	c	82 7.84 9	12.8
		LCM Quest 2-2 17/7/0 198	>	62 ?	>76 >
		LCM Quest 3-1 25/5/0 483 26.5 (14.4) 58 8.49 12 3.76
		LCM Quest 3-2 25/6/0 481	c	54 ? >1173 >
		LCM Quest 3b-1 26/6/0 1724	>	170 43.8 14 19.1
		LCM Quest 3b-2 26/7/0 1710	>	162 > >32 >
		LCM Quest 3c-1 26/6/0 1319	>	130 34.2 9	?
		LCM Quest 3c-2 26/7/0 1056	c	98 > >70 >
		LCM Quest 3d-1 26/6/0 281	>	81 5.43 49	?
		LCM Quest 3d-2 26/7/0 266	c	73 ?	446	?
		LCM Quest 3e-1 27/7/0 638	>	140 20.6 49	?
		LCM Quest 3e-2 27/8/0 514	>	110 6.46 >28 >
		LCM Quest 4-1 27/7/0 4482	>	386 186	9 50.1
		LCM Quest 4-2 27/8/0 3586	>	290 >	>6	>
	vars : Boolean state variables / numerical state variables / Boolean inputs
	size : number of locations of the CFG
	time : in seconds (Aspic: total time (time for analysis))
	?	: "don't know" (property not proved)
	>	: timed out after 600s
	c	: out of memory or crashed

Inria

RESEARCH CENTRE GRENOBLE -RHÔNE-ALPES

Inovallée 655 avenue de l'Europe Montbonnot 38334 Saint Ismier Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr

RR n°7630-v2

We assume here that Boolean inputs β have been encoded by non-determinism.Inria

This is an over-approximated result: the actual polyhedron has more constraints.RR n°7630-v2

A first version of the tool which implemented only logico-numerical abstract acceleration methods was called nbACCel[START_REF] Schrammel | Logico-numerical abstract acceleration and application to the verification of data-flow programs[END_REF].RR n°7630-v2

http://www.3ds.com Inria

⋆ This work was supported by the INRIA large-scale initiative Synchronics


Mouaiad Alras

Paul Caspi

Alain Girault

Pascal Raymond

Model-Based Design of Embedded Control Systems by means of a Synchronous Intermediate Model

Model-based design (MBD) involves designing a model of a control system, simulating and debugging it with dedicated tools, and finally generating automatically code corresponding to this model. In the domain of embedded systems, it offers the huge advantage of avoiding the timeconsuming and error-prone final coding phase. The main issue raised by MBD is the faithfulness of the generated code with respect to the initial model, the latter being defined by the simulation semantics. To bridge the gap between the high-level model and the low-level implementation, we use the synchronous programming language Lustre as an intermediate formal model. Concretely, starting from a highlevel model specified in the de-facto standard Simulink, we first generate Lustre code along with some structured "glue code", and then we generate embedded real-time code for the Xenomai RTOS. Thanks to Lustre's clean mathematical semantics, we are able to guarantee the faithfulness of the generated multi-tasked real-time code.

Introduction 1.Overview

A classical automatic control application consists of a software controller interacting with the physical device/environment via dedicated input and output drivers. Accordingly, engineers use a design environment both to model the physical environment, using continuous domain paradigms (e.g., differential equations), and to design the controller, using sampled discrete time paradigms (e.g., periodic clocks, multi-tasking, priorities). They simulate and debug their application and, once satisfied with it, they implement it over a target architecture consisting of a distributed hardware platform and a real-time operating system (RTOS). One of the most popular such design environment is Simulink, a de-facto standard in industry (automo-tive, robotics and automation, consumer electronics,...), and our work is based on it.

For lack of adequate tools, past common practice in industry was to implement manually the controller, an operation that is both time-consuming and error-prone. Modelbased design (MBD) precisely attempts at replacing the manual coding phase by an automatic code generation one. MBD is a very active area of research, both in academia and in private companies. The main assumptions it relies on are that the designer is satisfied with his/her controller (thanks to simulation and testing), that the software paradigms can be implemented on the architecture, and that the libraries of drivers are consistent with the physical device. Some MBD solutions exist today, for instance in avionics with SCADE [START_REF] Brière | Methods and specifications tools for Airbus on-board systems[END_REF], in automotive with Simulink-RTW [START_REF]Automatic Code Generation Technology For Embedded Control Applications[END_REF], and in robotics with Orccad [START_REF] Borrelly | The Orccad architecture[END_REF][START_REF] Simon | Synchronous programming of automatic control applications using Orccad and Esterel[END_REF].

The core principle of MBD is that the designer wants to obtain code that is faithful to his/her design; in other words, what he/she simulates under Simulink must execute exactly in the same manner on the target architecture. As a consequence, MBD must derive as automatically as possible code that is faithful to the design of the controller, and that can be implemented on the target architecture. Of course, since Simulink does not have a denotational semantics, it is impossible to prove formally this faithfulness.

The main issue that stems from the faithfulness requirement is that the semantics of a Simulink model depends on the chosen simulation parameters. For instance, some Simulink models may be accepted if one chooses discrete-step simulation, and rejected if one chooses variable-step, auto, or multi-threaded simulation. We call those simulation artifacts.

This is why we propose to use an intermediate formal model, to bridge the gap between the high-level Simulink model (i.e., the automatic control world) and the low-level implementation (i.e., the computer science world). We choose Lustre [START_REF] Halbwachs | The synchronous data-flow programming language Lustre[END_REF] to express formally the intermediate model, because both Lustre and Simulink are data-flow language that implement the synchronous model of computation, and because Lustre is equipped with a clean mathe-matical semantics. Our workflow is therefore: Simulink → Lustre → multiple tasks over a RTOS Our target RTOS is Xenomai, chosen for usability, maintainability, and portability reasons.

We also generate some structured "glue code", necessary to express features of Simulink that do not exist in Lustre. This is the case, for instance, of periodic clocks and sporadic events.

Contribution

Our goal is to develop a complete multi-tier MBD tool that goes from a high-level Simulink model to a low-level real-time implementation for the Xenomai RTOS. We involve as well an early conformity analyzing stage.

We extend existing MBD methods also based on Simulink and Lustre [START_REF] Caspi | From Simulink to Scade/Lustre to TTA: A layered approach for distributed embedded applications[END_REF][START_REF] Caspi | Semanticspreserving multitask implementation of synchronous programs[END_REF][START_REF] Scaife | Integrating model-based design and preemptive scheduling in mixed time-and event-triggered systems[END_REF][START_REF] Tripakis | Translating discrete-time simulink to Lustre[END_REF] to integrate more features of the high-level model. We extend Lustre with specific meta-operators, which are used to subsume these features on the one hand, and to incarnate on the other hand the real-time and system-level items of the Xenomai library. We call the extended language Lustre++.

In addition to high-level restrictions that prevent unsafe behaviors of Simulink, and in order to produce better code, we propose some confinements and user guidelines in two directions: Grouping tasks to generate the minimum number of RTOS tasks, and using exclusive modes with data sharing to generate more efficient and better structured code.

Our translation is modular and preserves the hierarchical structure of the Simulink model. It is implemented in a prototype tool consisting of two steps. First, our tool translates the Simulink model into our intermediate model Lustre++.

Then, this intermediate model can be used in two ways (see Section 4): On the one hand it can be compiled into embedded RTOS code, and on the other hand it can translated into pure Lustre code for the simulation and validation of the behavioral part of the system. Some existing approaches in industry only handle the mono-processor and mono-task case [START_REF]Automatic Code Generation Technology For Embedded Control Applications[END_REF][START_REF] Tripakis | Translating discrete-time simulink to Lustre[END_REF]. Extensions have been proposed for the multi-task case [START_REF] Camus | A verifiable architecture for multi-task, multi-rate synchronous software[END_REF][START_REF] Simon | Design of real-time periodic control systems through synchronisation and fixed priorities[END_REF], but they are limited to periodic tasks where all the periods are a multiple of the smallest period. The method we present here extends [START_REF] Tripakis | Translating discrete-time simulink to Lustre[END_REF] in two directions: on the one hand we handle sporadic tasks and arbitrary periodic tasks, and on the other hand we generate embedded real-time code while [START_REF] Tripakis | Translating discrete-time simulink to Lustre[END_REF] stopped at the Lustre level. We use previously developed theoretical results for the inter-task communication protocols [START_REF] Caspi | Semanticspreserving multitask implementation of synchronous programs[END_REF][START_REF] Scaife | Integrating model-based design and preemptive scheduling in mixed time-and event-triggered systems[END_REF].

The Intermediate Model 2.1 From a Simulink model to a synchronous program

Between the high-level Simulink model and the actual implementation, we use an intermediate model, based on the synchronous programming language Lustre [START_REF] Halbwachs | The synchronous data-flow programming language Lustre[END_REF]. This translation is hierarchical, that is, the structure of the resulting synchronous model reflects the one of the Simulink model. In order to obtain this structure, we must extract from the Simulink model the following information:

• Subsystems involving features related to asynchronous concepts, such as multi-tasking, periodic clocks, priorities etc. We call this part of the hierarchy the asynchronous architecture, and it is intended to be implemented by using features of the target RTOS. This part corresponds to the tree-like structure of the intermediate model.

• Subsystems that can be considered as "functional": they correspond to synchronous tasks, which can be straightforwardly translated into Lustre, and then into classical sequential programs using the Lustre code generator. Those subsystems are considered as atomic in our framwork: they are the leaves of the intermediate model structure.

Figure ?? shows an example of a hierachical Simulink model, together with the corresponding intermediate model structure. In this example, the top-level is made of three concurrent subsystems: the H and G blocks have been identified as "functional" (typically because they only involve simple computations, not detailed here). On the contrary, the F block contains non-purely functional features: a Data Store, and two subsystems triggered by a clock-enable condition: F is then identified as a non-functional node in the intermediate structure. Finally, F is itself made of two systems that are identified as atomic.

Indeed, the distinction between atomic and non-atomic subsystems is not always obvious, this is why we propose guidelines for the design of Simulink models: those guidelines, presented in Sections 2.3 and 2.4 are intended to help the extraction of the intermediate structure. If the Simulink model does not obey the guidelines, we are still able to generate faithful, but less efficient, code.

Since Lustre is notsuited to the expression of the asynchronous features of Simulink (clocks, priorities, and so on), we introduce a set of meta-operators to keep track of these informations in the intermediary nodes of the tree structure. In previous solutions, we used to encode thses features with non-structured annotations (e.g., pragmas); we find the meta-operators solution better structured and more elegant.

Meta-operators

Meta-operators are introduced in order to extend the Lustre language with the most common features one can find in a classical RTOS: triggered tasks, triggers, data buffers. Each meta-operator has a set of static parameters (given between << and >>) for expressing extra-functional information. We call Lustre++ the language extended with metaoperators.

Figure 3 shows the Lustre++ nodes generated for the example of Figure 1. It uses three different meta-operators:

• clock has two static parameters called p and h; it creates a periodic clock of period p and phase h.

• condact has three static parameters called f, c, and d; it invokes the function f at each tick of the clock c; the parameter d is the default value of f's output

• switch is a structured collection of condact operators, where the clocks are guaranteed to be exclusive.

The meta-operators are designed in order to allow the generation of RTOS code. They can also be translated into pure Lustre code as shown in Figure 4: this program corresponds to the node main of the example in Figure 3. The pure Lustre code is not used for embedded code generation because it abstracts away the real-time features. We only use it for testing and model-checking purpose.

Atomic subsystem guideline

The default heuristic is to consider that a Simulink subsystem triggered by a clock-enable condition must be implemented by an RTOS task. However, this is not always a good solution, since it may lead to a large number of context switches during the execution that may dramatically slow down the system.

However, we also propose a guideline that allows the user to choose how to regroup computation into a single RTOS task. This is achieved by labeling a block as a Simulink Atomic Subsystem. For instance in Figure 1, the subsystem H is marked as an Atomic Subsystem: this will enforce the code generator to group all hierarchical subsystems contained in H into single RTOS task.

Exclusive modes guideline

The notion of multi-modes is particularly important in control system design: it corresponds to the case where a state variable is computed according to different controllaws (called the modes) depending on the state of the system.

Muli-mode programming is not a built-in paradigm in Simulink, but rather an (expected) consequence of the design. The system F in Figure 1 is a typical example of multimodes design: F1 and F2 are triggered by exclusive conditions, and their outputs are merged into a single variable "out".

Recognizing this kind of organization in the simulink model is very important in our approach, since it allows to produce better implementation:

• it is not necessary to protect the access to shared variables, since these accesses are guaranteed to be exclusive,

• instead of generating a system task for each mode, we can produce a single task that dynamically select the right mode.

We propose a guideline that guarantees efficient generated code; a set of n blocks are recognized as exclusive modes of computation if:

1. Each block is triggered by an activation condition and the n activation conditions are produced by a single switch block.

2. Each output of these n block that is common to at least two blocks must be common to the n blocks and must be combined into a merge block.

We illustrate this guideline in the next section by a complete example.

Example

The example in Figure 5 is based on the controller part of the automotive power train model designed at Ford Motors Company [START_REF]Hybrid Models for Automotive Powertrain System -Revisiting a Vision[END_REF][START_REF] Motor | Structured Analysis Using Matlab/Simulink/Stateflow -Modeling Style Guidelines[END_REF] to study the 1-2 gearshift. This Simulink model contains five triggered subsystems (first, second, change of mind, torque 12, and inertia 12) witch all read the same input T t to calculate differently the same outputs tc1 and tc2. Some subsystems need additional inputs and may also be connected internally to other subsystems. For instance, the inertia 12 subsystem receives its last torque and last omega inputs from torque 12.

The merge operator is used in Simulink when the same variable is computed by different modes of computation. We restrict the usage of the merge operator to exlusive modes of computation (Section 2.4).

Goto/From Tags are used in Simulink as connectors to avoid crossing signal lines . For instance in Figure 5, this is the case of the reset inertia output of block mode control that is connected to the inertia 12 block. We restrict the use of such tags to be scoped only locally (in other words, Goto/From Tags that span over hierarchy levels are forbidden). Figure 6 shows the Lustre++ code corresponding to this example.

Another way to share variables between subsystems could be achieved by the use of Data Stores. We chose to take into account only local Data Stores declared explicitly using the Memory Block of the Simulink Library (see, e.g, the Data Store A in Figure 1, block F). [w_cr]

1 [reset] 3 [do_t] [tc2_t] [tc1_i] [tc2_i] [do_i] [w_t] [w_cr] [reset] [do_1] [tc1_1] [tc2_1] [do_2] [tc1_2] [tc2_2] [do_c] [tc1_c] [tc2_c] [tc1_t] [do_1] [do_2] [do_c] [do_t] [do_i]
case [START_REF] Audsley | Hard Real-Time Scheduling: The Deadline Monotonic Approach[END_REF] case [START_REF] Borrelly | The Orccad architecture[END_REF] case [START_REF] Brière | Methods and specifications tools for Airbus on-board systems[END_REF] case [START_REF] Camus | A verifiable architecture for multi-task, multi-rate synchronous software[END_REF] case [START_REF] Audsley | Applying New Scheduling Theory to Static Priority Preemptive Scheduling[END_REF] switch mode

5

[w_t]

[l_tc2] [tc2_t]

[tc2_i]

[tc1_2]

[tc1_1]

[tc1_c]

[tc1_t]

[tc2_1]

[tc2_2]

[tc2_c]

[l_tc2]

The Xenomai Real-Time Operating System

Several RTOS have been considered: Xenomai1 , RTLinux2 , and PaRTiKle3 . For usability, maintainability, and portability reasons, we have chosen Xenomai, running on top of RTAI 4 . We use it as a platform for implementing the embedded code generated from the Simulink models. This RTOS provides a considerably useful set of services for the implementation of real-time systems.

In Xenomai, the basic object performing actions is a task, a logically complete piece of application code. The Xenomai scheduler ensures that concurrent tasks are run according to some chosen scheduling policy. The two supported scheduling policies are the fixed priority-based FIFO and the round-robin policies.

Any Xenomai task may create any number of watchdog timers, called alarms: once the specified delay has elapsed, a user-defined handler is run. An alarm can be either periodic or "one-shot"; in the former case, the real-time kernel automatically reprograms the alarm for the next iteration, according to the user-defined interval value.

To insure the synchronization between tasks, Xenomai offers condition variables, which allow tasks to suspend their execution until some predicate on condition variables is satisfied. A condition variable must always be associated with a mutex (mutual exclusion section), to avoid race conditions occurring when one task is waiting for a condition variable while another task signals the condition just before the first task waits for it.

For instance, a portion of the Xenomai real-time code generated for the model of Figure 1 is shown in Figure 7. The information required to set the task parameters is assumed to be known from the high level model and given by the user.

The ck 40 object is created (rt alarm create) to be triggered every 40 milliseconds and is started (rt alarm start) without any offset. It will fire the task object task G created (rt task create) and associated to the corresponding body function calc G which can be seen as a wrapper of G's step function. This portion of code corresponds to the meta-operator condact<<G,ck_40,1>>(in2). The step function is a C code function generated automatically from the corresponding functional Lustre node by the tool lus2C (Figure 8).

Xenomai implements the notion of time base, by which timers may be clocked separately according to distinct frequencies given in number of ticks; the duration of a tick is specified by the time base. Such a periodic time base is managed to be compatible with the timing mechanisms of When generating real-time code for automatic control systems, one of the difficult issues concerns blocks that have different periods and that communicate together. Accordingly, there are three cases for a given pair of communicating tasks: high to low priority, high to low priority with unit delay, and low to high priority with unit delay 5 [START_REF] Scaife | Integrating model-based design and preemptive scheduling in mixed time-and event-triggered systems[END_REF]. The difficulty is to guarantee the zero-delay semantics of Simulink. This is achieved thanks to a set of buffers and pointers to these buffers [START_REF] Caspi | Semanticspreserving multitask implementation of synchronous programs[END_REF]. The principle is that the pointers to the buffers are manipulated upon the arrival of the events triggering the tasks instead of during the execution of the tasks. In that way, the order of arrivals can be memorized and the original Simulink semantics can be preserved [START_REF] Scaife | Integrating model-based design and preemptive scheduling in mixed time-and event-triggered systems[END_REF]. 5 The low to high priority without unit delay is impossible.

Work flow

Our MBD approach is based on a three-phase process. First, Simulink models are parsed thanks to the translator MDL2XML. It extends the existing similar compiler from Sofronis [START_REF] Tripakis | Translating discrete-time simulink to Lustre[END_REF] to handle periodic clocks, data stores, atomic subsystems, and exclusive modes of computation.

The MDL2XML translator first involves a filtering and checking stage. Models that contain global data stores or global connectors will be rejected. The output of this stage is a transformed XML file, which is the entry point of the backend code generation.

Second, this XML-encoded Simulink model is translated into an intermediate formal model thanks to the tool XML2LUS. It performs the clock inference, type inference, and conformity analysis. The purpose of this analysis is twofold: to detect combinatorial loops and nondeterministic behaviors (non exclusive data sharing), and to recognize patterns respecting the guidelines in order to generate more efficient code (exclusive modes and tasks grouping).

The XML2LUS tool then generates, for each Simulink block and subsystem, the corresponding Lustre node, and external function code for every "unknown" and "userdefined" block. In addition, glue-code is generated for the meta-operators by retrieving information from the highlevel model.

Third, the intermediate model is compiled into actual RTOS code thanks to the tool LUS2XEN. It generates, for each Lustre node, the corresponding real-time task or system call, and for each meta-operator the corresponding realtime object from the native library of Xenomai. Periodic tasks are triggered by alarm objects, sporadic tasks are triggered by event objects, buffers are implemented by condition variables and mutex services. Additional Xenomai glue code is generated to manage the master time base, which serves as the specification basis for delays and timeouts. Moreover, the intermediate model can also be translated into a purely functional model that can be used for formal validation (model-checking, test case generation ...). This is a distinctive feature of our approach and would not be achievable with a direct C code generation such as Simulink-RTW [START_REF]Automatic Code Generation Technology For Embedded Control Applications[END_REF].

Conclusion and Future Work

We have presented a Model-Based Design (MBD) method for embedded control systems specified in Simulink. Once the model has been simulated and the designer is satisfied with it, we transform it into an intermediate formal model, for which we have chosen the synchronous programming language Lustre. Lustre and Simulink are both synchronous data-flow programming languages, so this choice is natural. Besides, Lustre is equipped with a clean mathematical semantics, so our intermediate model allows the designer to use formal validation tools, e.g., model-checkers and test-case generators, to validate his/her Simulink model. More importantly, our intermediate formal model serves as a starting point to generate multi-task real-time code to be executed on the Xenomai RTOS. Thanks to the formal semantics of Lustre, the low-level RTOS code is faithful to the high-level Simulink model. This faithfulness is the central feature of our MBD method.

Our intermediate formal model consists of two parts: on the one hand classical Lustre nodes that encode the purely functional part of the Simulink model, and on the other hand ad-hoc meta-operators that encode the asynchronous features of the Simulink model, such as the periodic clocks, the priorities, and so on. The meta-operators are structured hierarchically to reflect the hierarchical structure of the Simulink model. During the real-time code generation phase, the functional part (i.e., the classical Lustre nodes) are translated into RTOS tasks whose C code is directly obtained via the usual Lustre to C compiler. Concerning the meta-operators, they are translated into RTOS code thanks to the services offered by Xenomai (i.e., tasks, alarms, condition variables, mutexes, and so on).

Even if we don't address, in this paper, classical realtime problems (WCET analysis, scheduling feasibility, etc...), we are aware of these orthogonal problems. Faithful translation can be guaranteed only under the condition that all real-time constraints are satisfied [START_REF] Audsley | Hard Real-Time Scheduling: The Deadline Monotonic Approach[END_REF][START_REF] Audsley | Applying New Scheduling Theory to Static Priority Preemptive Scheduling[END_REF].

In future work, we will generalize our MBD method to a wider class of meta-operators to cover more RTOS sevices, and we will enhance the intermediate model with fault tolerance and distribution annotations.

Figure 1 .

 1 Figure 1. A hierarchical Simulink model.

Figure 2 .

 2 Figure 2. The intermediate model structure corresponding to the Simulink model of Figure 1.

Figure 3 .

 3 Figure 3. Lustre++ code for the model of Figure 1.

Figure 4 .

 4 Figure 4. Lustre code for the model of Figure 3.

Figure 6 .

 6 Figure 6. Lustre++ code for the model of Figure 5.

Figure 7 .Figure 8 .

 78 Figure 7. Xenomai code for the Simulink model of Figure 1.

Figure 9 .

 9 Figure 9. Our work flow with the intermediate model.

http://www.xenomai.org

http://www.rtlinuxfree.com

http://www.e-rtl.org/partikle

https://www.rtai.org