Influence of Cavitation on Textural Atomization

F. Abuzahra (1) ; C. Dumouchel (1) ; JB. Blaisot (1) ; A. Sou (2) ; G. Godard (1) (1) CNRS-UMR 6614 CORIA, Saint-Etienne du Rouvray, France; (2) Kobe University, Japan <Fakhry Abuzahra> <UMR 6614 CORIA> Email: Fakhry.Abuzahra@coria.fr Website: http://haos-itn.eu/ Contact 1. He, L., Riz, F., "Effect of cavitation on flow and turbulence in plain orifices for high-speed atomization." Atomization and Sprays 5 (1995) 569-584 2. Sou, A., Hosokawa, S., Tomiyama, A., "Effects of cavitation in a nozzle on liquid jet atomization." Int. Journ Heat and Mass Transfer 50 (2007)

Textural atomization designates the production of liquid drops from the peeling off of liquid gas interfaces. This mechanism is usually observed in the near nozzle region and is often associated with a significant level of turbulence in the flow issuing from the injector. Cavitating internal flows are known to promote the level of turbulence of the issuing flow [1] and indeed textural atomization processes have been reported on such flows [2]. This work characterizes the textural atomization of a flow issuing from a so-called 2D atomizer in which cavitation develops as the flow rate increases. The experimental work shows visualizations of the flow inside the discharge orifice and the textural atomization process in the near nozzle region. Internal velocity fields obtained by LDV measurements are presented. A multi-scale analyzing tool [3] is applied to describe the textural atomization process. This analysis reports an evolution of the textural atomization liquid structures and of their deformation as cavitation effects increase. It also opens a way to the prediction of the droplets produced by the textural atomization process whose diameter distributions have been measured and are also presented.

  3575-3582 3. Dumouchel, C., "Liquid atomization and spray: A multi-scale description." Keynote Lecture ASME-FEDSM, FEDSM2017-69590, July 30-August 3 (2017) 1-12 4. Sou, A., Pratama, R.H., Tomisaka, T. Kibayashi, Y. "Caviatation flow in nozzle of liquid injector", ICLASS 2012, Heidelberg, Germany September 2-6, 2012 5. Dumouchel, C., Blaisot, J.B., Bouche, E., Ménard , T., Vu, T.T. "Multi-scale analysis of atomizing liquid ligaments. Int. Journ. Multiphase Flows 73 (2015) 251-263 6. Fdida, N., Blaisot, J.B. "Drop size distribution measured by imaging: determination of the measurement volume by the calibration of the point spread function." Measurement Science and Technology 21 (2009): 025501. 7. Dumouchel, C. "A New Formulation of the Maximum Entropy Formalism to Model Liquid Spray Drop-Size Distribution." Particle & Particle Systems Characterization 23 (2006) 468-479.

•••••

  1. To characterize the textural atomization in cavitating flow conditions 2. To describe the evolution of the liquid structures developing in the textural atomization 3. To explore a possible connection with the diameter distribution of the produced droplets Objectives Abstract The multi-scale analysis of the liquid-gas interface provides a quantified representation of the structures involved in the textural atomization process • These structures depend on cavitation • A correlation between the textural perturbations and the initial spray droplets is recognized Conclusions This project has received funding from the European Union Horizon-2020 Research and Innovation Programme. Grant Agreement No 675676 Water in air 𝜎 = 0.07 N/m 𝜌 𝑔 = 1.204 kg/m 3 γ = 1.1*10 -6 m 2 /s 𝑝 𝑣 =2339 Pa Injector thickness (ℎ) = 1 mm • Measurement of the scale distribution e 2 (d) • It is defined by: • For a smooth cylinder, it is a step function • For a deformed cylinder, it is depending on the scale Scale d Application on the cavitating side only • The scale distribution is mathematically separated in two parts to isolate the textural structure scale distribution e 2,1 (d) [5] • The scale distribution e 2,1 (d): the textural atomization As CN decreases: • the interface length per unit surface increases: the atomizing structures are thinner (left) • The atomizing structures are more and more deformed at small scales (right) The e 2,1 (d) parameter evolutions indicate a modification of the perturbation size distribution • Correlations between e 2,1 (d) and f 2 (D) parameters are established Surface-based diameter distributions of initial drops are measured on images [6] and mathematically represented by a combination of two 3-parameter Gamma distributions [7] 2D atomizer from A. Sou [4] • Transmission images show four cavitation regimes • LDV measurements show that the cavitation zone is associated with high recirculation except for the last cavitation regime • The textrural atomization process shows ligaments • The ligaments strongly depend on the cavitation Liquid Atomization and Spray Systems, Chicago USA, July 22-26, 2018


Ben Souha

Lacramioara Rayana

Saddek Astefanoaei

Marius Bensalem
email: saddek.bensalem@imag.fr

Ȃmioara Ȃcr

¸tef As

Saddek Ȃnoaei

Jacques Combaz
email: jacques.combaz@imag.fr

Compositional Verification for Timed Systems Based on Automatic Invariant Generation

Keywords: 1998 ACM Subject Classification: D.2.4 Software/Program Verification, F.3.1 Specifying and Verifying and Reasoning about Programs compositional verification, timed automata, invariants, component invariants, interaction invariants, interactions

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Compositional methods in verification have been developed to cope with state space explosion. Generally based on divide et impera principles, these methods attempt to break monolithic verification problems into smaller sub-problems by exploiting either the structure of the system or the property or both. Compositional reasoning can be used in different manners e.g., for deductive verification, assume-guarantee, contract-based verification, compositional generation, etc.

The development of compositional verification for timed systems remains however challenging. State-of-the-art tools [START_REF] Behrmann | UPPAAL 4.0[END_REF][START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF][START_REF] Wang | Redlib for the formal verification of embedded systems[END_REF][START_REF] Gardey | ROMEO: A tool for analyzing time Petri nets[END_REF] for the verification of such systems are mostly based on symbolic state space exploration, using efficient data structures and particularly involved exploration techniques. In the timed context, the use of compositional reasoning is inherently difficult due to the synchronous model of time. Time progress is an action that synchronises continuously all the components of the system. Getting rid of the time synchronisation is necessary for analysing independently different parts of the system (or of the property) but becomes problematic when attempting to re-compose the partial verification results. Nonetheless, compositional verification is actively investigated and several approaches have been recently developed and employed in timed interfaces [START_REF] Alfaro | Timed interfaces[END_REF] and contractbased assume-guarantee reasoning [START_REF] David | Compositional verification of real-time systems using Ecdar[END_REF][START_REF] Lin | Automatic generation of provably correct embedded systems[END_REF].

In this paper, we propose a different approach for exploiting compositionality for analysis of timed systems. The driving principle is to use invariants as approximations to exact reachability analysis, the default technique in model-checking. We show that rather precise invariants can be computed compositionally, from the separate analysis of the components in the system and from their composition glue. This method is proved to be sound for the verification of safety state properties. However, it is not complete.

The starting point is the verification method of [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF], summarised in Figure 1. The method exploits compositionality as explained next. Consider a system consisting of components B i interacting by means of a set γ of multi-party interactions, and let ϕ be a system property of interest. Assume that all B i as well as the composition through γ can be independently characterised by means of component invariants CI (B i ), respectively interaction invariant II (γ). The connection between the invariants and the system property ϕ can be intuitively understood as follows: if ϕ can be proved to be a logical consequence of the conjunction of components and interaction invariants, then ϕ holds for the system. In the rule (V R) the symbol " " is used to underline that the logical implication can be effectively proved (for instance with an SMT solver) and the notation " γ B i |= ϕ" is to be read as "ϕ holds in every reachable state of γ B i ".

i CI (B i ) ∧ II (γ) → ϕ γ B i |= ϕ (VR)
The verification rule (VR) in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] has been developed for untimed systems. Its direct application to timed systems may be weak as interaction invariants do not capture global timings of interactions between components. The key contribution of this paper is to improve the invariant generation method so to better track such global timings by means of auxiliary history clocks for actions and interactions. At component level, history clocks expose the local timing constraints relevant to the interactions of the participating components. At composition level, extra constraints on history clocks are enforced due to the simultaneity of interactions and to the synchrony of time progress.

As an illustration, let us consider as running example the timed system in Figure 2 which depicts a "controller" component serving n "worker" components, one at a time. The interactions between the controller and the workers are defined by the set of synchronisations {(a | b i ), (c | d i ) | i ≤ n}. Periodically, after every 4 units of time, the controller synchronises its action a with the action b i of any worker i whose clock shows at least 4n units of time. Initially, such a worker exists because the controller waits for 4n units of time before interacting with workers. The cycle repeats forever because there is always a worker "willing" to do b, that is, the system is deadlock-free. Proving deadlock-freedom of the system requires to establish that when the controller is at location lc 1 there is at least one worker such that y i -x ≥ 4n -4. Unfortunately, this property cannot be shown if we use (VR) as it is in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]. Intuitively, this is because the proposed invariants are too weak to infer cross constraints relating the clocks of the controller and those of the workers: interaction invariants II (γ) relates only locations of components and thus at most eliminates unreachable configurations like (lc 1 , . . . , l 2i , . . . ), while the component invariants can only state local conditions on clocks such as x ≤ 4 at lc 1 . Using history clocks allows to recover additional constraints. For example, after the controller returns from lc 2 to lc 1 for the first time, whenever it reaches lc 1 again, there exists a worker i whose clock has an equal value as that of the controller. Similarly, history clocks allow to infer that different (a | b i ) interactions are separated by at least 4 time units. These constraints altogether are sufficient to prove the deadlock freedom property. Organisation of the paper. This paper is essentially an extended version of the conference paper [START_REF] Astefanoaei | Compositional invariant generation for timed systems[END_REF]. The extension is threefold with respect to (1) incorporating proofs, [START_REF] Alfaro | Timed interfaces[END_REF] detailing technicalities about handling initial states, and (3) formalising three heuristics to speed up and simplify invariant generation. Section 2 recalls the needed definitions for modelling timed systems and their properties. Section 3 presents our method for compositional generation of invariants. Section 4 describes the heuristics while Section 5 shows their use in the case studies we experimented with in our implementation. Section 6 concludes.

Timed Systems and Properties

In the framework of the present paper, components are timed automata and systems are compositions of timed automata with respect to multi-party interactions. The timed automata we use are essentially the ones from [START_REF] Alur | A theory of timed automata[END_REF], however, slightly adapted to embrace a uniform notation throughout the paper.

Definition 2.1 (Syntax). A component is a timed automaton (L, A, X , T, tpc, s 0 ) where L is a finite set of locations, A a finite set of actions, X is a finite set of local 1 clocks, T ⊆ L × (A × C × 2 X ) × L
is a set of edges labelled with an action, a guard, and a set of clocks to be reset, tpc : L → C assigns a time progress condition 2 to each location. C is the set of clock constraints and s 0 ∈ L × C provides the initial configuration. A clock constraint is defined by the grammar:

C ::= true | x#ct | x -y#ct | C ∧ C
with x, y ∈ X , # ∈ {<, ≤, =, ≥, >} and ct ∈ Z. Time progress conditions are restricted to conjunctions of constraints as x ≤ ct. 1 Locality is essential for avoiding side effects which would break compositionality and local analysis. 2 To avoid confusion with invariant properties, we prefer to adopt the terminology of "time progress condition" from [START_REF] Bornot | An algebraic framework for urgency[END_REF] instead of "location invariants".

Before recalling the semantics of a component, we first fix some notation. Let V be the set of all clock valuation functions v : X → R ≥0 . For a clock constraint C, v |= C denotes the evaluation of C in v. The notation v + δ represents a new v defined as v (x) = v(x) + δ while v[r] represents a new v which assigns any x in r to 0 and otherwise preserves the values from v. Definition 2.2 (Semantics). The semantics of a component B = (L, A, X , T, tpc, s 0 ) is given by the labelled transition system (Q, A, →, Q 0 ) where

Q ⊆ L × V denotes the states of B, → ⊆ Q × (A ∪ R ≥0 ) × Q denotes the
transitions according to the rules:

• (l, v) δ → (l, v + δ) if ∀δ ∈ [0, δ] .(tpc(l)(v + δ )) (time progress); • (l, v) a → (l , v[r]) if l, (a, g, r), l ∈ T , g(v) ∧ tpc(l )(v[r]) (action step). and Q 0 = {(l 0 , v 0 )|s 0 = (l 0 , c 0 ) ∧ c 0 (v 0 )} denotes the initial states.
Because the semantics defined above is in general infinite, we work with the so called zone graph [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF] as a finite symbolic representation. The symbolic states in a zone graph are pairs (l, ζ) where l is a location of B and ζ is a zone, a set of clock valuations defined by clock constraints. The initial configuration s 0 = (l 0 , c 0 ) corresponds trivially to a symbolic state (l 0 , ζ 0 ). Given a symbolic state (l, ζ), its successor with respect to a transition t of B is denoted as succ(t, (l, ζ)) and defined by means of its timed and its discrete successor:

• time succ((l, ζ)) = (l, ζ ∩ tpc(l)) • disc succ(t, (l, ζ)) = (l , (ζ ∩ g)[r] ∩ tpc(l )) if t = l, ( , g, r), l • succ(t, (l, ζ)) = norm(time succ(disc succ(t, (l, ζ))))
where , [r], norm are usual operations on zones:

ζ is the forward diagonal projection of ζ, i.e., it contains any valuation v for which there exists a real δ such that v -δ is in ζ; ζ[r] is the set of all valuations in ζ after applying the resets in r; norm(ζ) corresponds to normalising ζ such that all bounds on clocks and clock differences are either bounded by some finite value or infinite. Since our use of invariants is only as over-approximations of the reachable states, a more thorough discussion on normalisation is not relevant for the present paper. The interested reader may refer to [START_REF] Bengtsson | On clock difference constraints and termination in reachability analysis of timed automata[END_REF][START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF] for more precise definitions.

A symbolic execution of B is a sequence of symbolic states s 0 , . . . , s i , . . . 3 such that for any i > 0, there exists a transition t for which s i is succ(t, s i-1 ). The set of reachable symbolic states of B is Reach B (s 0 ) where Reach B is defined recursively as:

Reach B (s) = {s} ∪ t∈T Reach B (succ(t, s))
for an arbitrary s and T the set of transitions in B . We remind that the set Reach B (s 0 ) can be shown finite knowing that the number of normalised zones is finite. In general, the symbolic zone graph provides an over-approximation of the set of reachable states. This over-approximation is exact only for timed automata without diagonal constraints [START_REF] Bengtsson | On clock difference constraints and termination in reachability analysis of timed automata[END_REF][START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF].

In our framework, components communicate by means of interactions, which are synchronisations between actions. Given n components (B i ) i=1,...,n , with disjoint sets of actions A i , an interaction is a subset α ⊆ ∪ i A i containing at most one action per component. We denote interactions α as sets {a i } i∈I , with a i ∈ A i for all i ∈ I ⊆ {1, . . . , n}. For readability, in examples, we use the alternative notation (a

1 | a 2 | • • • | a i ) instead.
Given a set of interactions γ, we denote by Act(γ) the set of actions involved in γ, that is, Act(γ) = ∪ α∈γ α. 3 We tacitly assume that s0 is such that s0 = time succ(s0). If this is not the case, one can always consider time succ(s0) instead of s0 for the definition of symbolic executions and reachable states. Definition 2.3 (Timed System). For a given n and i ∈ {1, . . . , n} let B i = (L i , A i , X i , T i , tpc i , s 0i ) be n components with disjoint sets of actions and initial states s 0i = (l 0i , c 0i ). Let γ be a set of interactions constructed from ∪ i A i . The timed system γ B i is defined as the component (L, γ, X , T γ , tpc, s 0 ) where L = × i L i , X = ∪ i X i , tpc( l) = i tpc(l i ), s 0 = ((l 01 , ..., l 0n ), i c 0i ) and

T γ =    ( l, (α, g, r), l ) l = (l 1 , ..., l n ) ∈ L, l = (l 1 , ..., l n ) ∈ L α = {a i } i∈I ∈ γ, ∀i ∈ I.(l i , (a i , g i , r i ), l i ) ∈ T i , ∀i ∈ I.l i = l i g = i∈I g i , r = i∈I r i   
In the timed system γ B i , a component B i can execute an action a i only as part of an interaction α, a i ∈ α, that is, along with the execution of all other actions a j ∈ α 4 . This corresponds to the usual notion of multi-party interaction. We note that interactions can only restrict the behaviour of components, i.e., the states reached by B i in γ B i belong to Reach B i (s 0i ). This is a property which is exploited in the verification rule (VR) in Figure 1.

To give a logical characterisation of components and their properties, we use invariants. An invariant Φ is a state predicate which holds in every reachable state of B , in symbols, B |= Φ. We use CI (B ) and II (γ), to denote component, respectively interaction invariants. For component invariants, our choice is to work with their reachable symbolic set. More precisely, for component B , its associated component invariant CI (B ) is the disjunction of (l ∧ ζ) for all symbolic states (l, ζ) in Reach B (s 0 ). To ease the reading, we abuse of notation and use l as a place holder for a state predicate "at(l)" which holds in any symbolic state with location l, that is, the semantics of at(l) is given by (l, ζ) |= at(l). As an example, the component invariants for the example in Figure 2 with one worker are:

CI (Controller ) = (lc 0 ∧ x ≥ 0) ∨ (lc 1 ∧ 4 ≥ x ≥ 0) ∨ (lc 2 ∧ x ≥ 0) CI (Worker 1 ) = (l 11 ∧ y 1 ≥ 0) ∨ (l 21 ∧ y 1 ≥ 4).
The interaction invariants are computed by the method explained in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]. Interaction invariants are over-approximations of the global state space allowing us to disregard certain tuples of local states as unreachable. As an illustration, consider the interactions invariant for the running example when the controller is interacting with one worker:

II {(a | b 1 ), (c | d 1 )} = (l 11 ∨ lc 2 ) ∧ (l 21 ∨ lc 0 ∨ lc 1 ).
The invariant is given in conjunctive normal form to stick to the formalism in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]. Every disjunction corresponds to the so called notion of "initially marked traps" in an underlying Petri net associated to our model. Intuitively, a trap in Petri nets is a set of places which always contains tokens if they have tokens initially.

We note that the proposed 5 component and interaction invariants are inductive invariants. A state predicate is called inductive for a component or system B if, whenever it holds for a state s of B it equally holds for any of its successors s . That is, the validity of an inductive predicate is preserved by executing any transition, timed or discrete. An inductive predicate which moreover holds at initial states is an (inductive) invariant. Trivially, such a predicate holds in all reachable states. 4 To simplify the notation, we omit unary interactions and the actions for transitions involved in them.

For example, in Figure 2, the initial transition in Controller does not have an explicit action associated. 5 The rule (VR) is generic enough to work with other types of invariants. For example, one could use any over-approximation of the reachable set in the case of component invariants, however, this comes at the price of losing precision.

As for component properties, we are interested in arbitrary invariant state properties that can be expressed as boolean combinations of "at(l)" predicates and clock constraints. Invariant properties include generic properties such as mutual exclusion, absence of deadlock, unreachability of "bad" states, etc. As a simple illustration consider the property lc 1 → i (y i -x ≥ 4n -4), discussed for our running example introduced in Section 1. As a more sophisticated example, consider absence of deadlock. Intuitively, a timed system with a set of interactions γ is deadlocked when no interaction in γ is enabled. Absence of deadlock is therefore expressed as the disjunction ∨ α∈γ enabled(α). As for the enabledness predicate, we borrow it from [START_REF] Tripakis | Verifying progress in timed systems[END_REF] where it is essentially constructed from the syntactic definition of the timed system. More precisely, for an interaction α, enabled (α) is ∨ t enabled (t), with t being a transition triggered by α. In turn, for t = l, (α, g, r), l , enabled (t) is defined using elementary operations on zones as l∧ (g

∩ [r]tpc( l ) ∩ tpc( l)), where ζ is the backward diagonal projection of ζ, [r]ζ is the set of valuations v such that v[r] is in ζ.

Timed Invariant Generation

As explained in the introduction, a direct application of the compositional verification rule (VR) may not be useful in itself in the sense that the component and the interaction invariants alone are usually not enough to prove global properties, especially when such properties involve relations between clocks in different components. More precisely, though component invariants encode timings of local clocks, there is no direct way -the interaction invariant is orthogonal to timing aspects -to constrain the bounds on the differences between clocks in different components. To give a concrete illustration, consider the property ϕ S af e = (lc 1 ∧ l 11 → x ≤ y 1 ) that holds in the running example with one worker. We note that if this property is satisfied, it is guaranteed that the global system is not deadlocked when the controller is at location lc 1 and the worker is at location l 11 . It is not difficult to see that ϕ S af e cannot be deduced from CI (Controller ) ∧ CI (Worker 1 ) ∧ II {(a | b 1 ), (c | d 1 )} as no relation can be established between x and y 1 .

3.1. History Clocks for Actions. In this section, we show how we can, by means of some auxiliary constructions, apply (VR) more successfully. To this end, we "equip" components (and later, interactions) with history clocks, a clock per action; then, at interaction time, the clocks corresponding to the actions participating in the interaction are reset. This basic transformation allows us to automatically compute a new invariant of the system with history clocks. This new invariant, together with the component and interaction invariants, is shown to be, after projection of history clocks, an invariant of the initial system. Definition 3.1 (Components with History Clocks). Given component B = (L, A, X , T , tpc, s 0 ), its extension with history clocks is the component

B h = (L, A, X ∪ H A , T h , tpc, s h 0 ) where • H A = {h 0 } ∪ {h a | a ∈ A} is the set of history clocks, • T h = l, (a, g, r ∪ {h a }), l | l, (a, g, r), l ∈ T , • s h 0 = (l 0 , c h 0 ), where c h 0 = (c 0 ∧ h 0 = 0 ∧ a∈A h a > 0), given s 0 = (l 0 , c 0 ).
The clock h 0 measures the time from the initialisation. This clock equals 0 in s h 0 and is never tested or reset. Due to this very restricted use, the same clock h 0 can be consistently used (shared) by all components B h and consequently, allows to capture clock constraints derived from the common system initialisation time.

Every history clock h a measures the time passed from the last occurrence of action a. These history clocks are initially strictly greater than 0 and are reset when the corresponding action is executed. As a side effect, whenever h a is strictly bigger than h 0 , we can infer that the action a has not been (yet) executed. This initialisation scheme allows a more refined analysis precisely because we can distinguish between actions which were executed and those which were not.

Since there is no timing constraint involving history clocks, these have no influence on the behaviour. The extended model is, in fact, bisimilar to the original model. Moreover, any invariant of the extended model of B h corresponds to an invariant of original component. By abuse of notation, given set of actions A = {a 1 , ..., a m } use ∃H A to stand for ∃h a 1 ∃h a 2 . . . ∃h am ∃h 0 . Proposition 3.2.

(

) If Φ h is an invariant of B h then Φ = ∃H A .Φ h is an invariant of B. (2) If Φ h is an invariant of B h and Ψ h an inductive assertion of B h expressed on history clocks H A \ {h 0 } then Φ = ∃H A .(Φ h ∧ Ψ h ) is an invariant of B. 1
Proof.

(1) It suffices to notice that any symbolic state (l,

ζ h ) in the reachable set Reach B h (s h 0 ) corresponds to a symbolic state (l, ζ) in the reachable set Reach B (s 0 ) such that ζ is the projection of ζ h to clocks in X , that is ζ ≡ ∃H A .ζ h . Henceforth, ∃H A .Reach B h (s h 0 ) ≡ Reach B (s 0 ). Moreover, for any invariant Φ h of B h it holds ∃H A .Reach B h (s h 0 ) ⊆ ∃H A .Φ h
. By combining the two facts, we obtain that Φ is an invariant of B .

(2) Consider the modified component with history clocks B h Ψ defined as B h but with initial configuration (l 0 , c h 0 ∧ Ψ h ). This initial configuration is valid, as Ψ h constrain exclusively clocks in H A whereas c h 0 leaves all of them unconstrained. Now, it can be easily shown that Φ h ∧ Ψ h is an invariant of B h Ψ . Then, following the same reasoning as for point (1) we obtain that

∃H A .(Φ h ∧ Ψ h ) is an invariant of B .
The only operation acting on history clocks is reset. Its effect is that immediately after an interaction takes place, all history clocks involved in the interaction are equal to zero. All the remaining ones preserve their previous values, thus they are greater than or equal to those being reset. This basic observation is exploited in the following definition, which builds, recursively, all the inequalities that could hold given an interaction set γ. Definition 3.3 (Interaction Inequalities for History Clocks). Given an interaction set γ, we define the following interaction inequalities E(γ):

E(γ) = α∈γ a i ,a j ∈α a k ∈Act(γ α) h a i = h a j ≤ h a k ∧ E(γ α) .
where

γ α = {β \ α | β ∈ γ ∧ β ⊆ α} and E(∅) = true.
The mechanism of history clocks is as follows. When an interaction α takes place, the history clocks h a associated to any action a ∈ α are reset. Thus they are all equal and smaller than any other clocks and measure the time passed from the last occurrence of a.

The operation γ α eliminates in any interaction β the actions from α. As an illustration, for

β = (a | a 1 | a 2 ), α = (a 1 | a 2 ), γ = {α, β}, γ α = {a}.
We can use the interpreted function "min" as syntactic sugar to have a slightly more compact expression for E(γ) as follows:

E(γ) = α∈γ a i ,a j ∈α h a i = h a j ≤ min a k ∈Act(γ α) h a k ∧ E(γ α) .
As an example, for γ = {(a | b 1 ), (c | d 1 )} corresponding to the interactions between the controller and one worker in Figure 2, the compact form is:

h a = h b 1 ≤ min(h c , h d 1 ) ∧ h c = h d 1 ∨ h c = h d 1 ≤ min(h a , h b 1 ) ∧ h a = h b 1 .
E(γ) characterises the relations between history clocks during any possible execution. It can be shown that this characterisation is, in fact, an inductive predicate of the extended system with history clocks.

Proposition 3.4. E(γ) is an inductive predicate of γ B h i . Proof. Assume E(γ) holds in some arbitrary state s of γ B h i .
We have two categories of successor states for s, namely time successors and discrete successors. Obviously E(γ) holds for all time successors s , as all clocks progress uniformly and henceforth all the relations between them are preserved. Let now s be a discrete successor of s by an arbitrary interaction α. As all the history clocks for actions in α have just been reset, s satisfies

a i ,a j ∈α a k ∈Act(γ α) 0 = h a i = h a j ≤ h a k (3.1)
To conclude the proof, we need to show that moreover, for the remaining clocks of actions in Act(γ α), they satisfy E(γ α) in s . Actually, we can show the additional fact that for any set of interactions γ and for any interaction α the implication E(γ) → E(γ α) is valid in any reachable state. This fact can be simply proven by induction on the size of the set interactions γ following the definition of E. Consequently, assuming that E(γ) holds at s, it follows that E(γ α) holds at s. Then E(γ α) also holds at s because α does not modify any clock involved in γ α and this concludes the proof.

By using Proposition 3.4 and Proposition 3.2, we can safely combine the component and interaction invariants of the system with history clocks with the interaction inequalities. We can eliminate the history clocks from i CI (B h i ) ∧ II (γ) ∧ E(γ) and obtain an invariant of the original system. This invariant is usually stronger than i CI (B i ) ∧ II (γ) and yields more successful applications of the rule (VR).

Corollary 3.5. Φ = ∃H A .( i CI (B h i ) ∧ II (γ) ∧ E(γ)) is an invariant of γ B i . Example 3.6.
We reconsider the model of a controller and a worker from Figure 2. We show how the generated invariants are enough to prove the safety property ϕ Safe = (lc 1 ∧ l 11 → x ≤ y 1 ) from Section 1. The invariants for the components with history clocks are computed precisely as illustrated in Section 1, that is, they represent zone graphs:

CI (Controller h ) =(lc 0 ∧ x = h 0 < h a ∧ h 0 < h c ) ∨ (lc 1 ∧ x ≤ h 0 -4 ∧ x ≤ 4 ∧ h 0 < h a ∧ h 0 < h c ) ∨ (lc 1 ∧ x ≤ 4 ∧ x = h c ≤ h a ≤ h 0 -8) ∨ (lc 2 ∧ x ≤ h 0 -8 ∧ h a = x ∧ h 0 < h c ) ∨ (lc 2 ∧ x = h a ∧ h c = h a + 4 ≤ h 0 -8) CI (Worker h 1 ) =(l 11 ∧ y 1 = h 0 < h d 1 ∧ h 0 < h b 1 ) ∨ (l 11 ∧ y 1 = h d 1 ≤ h b 1 ≤ h 0 -4) ∨ (l 21 ∧ h b 1 + 4 ≤ y 1 = h 0 < h d 1 )) ∨ (l 21 ∧ y 1 = h d 1 ≤ h 0 -4 ∧ h b 1 ≤ h d 1 -4)
By using the interaction invariant described in Section 2 and the inequality constraints

E((a | b 1 ), (c | d 1 )
), after the elimination of the existential quantifiers in

∃h a .∃h b 1 .∃h c .∃h d 1 .∃h 0 CI (Controller h ) ∧ CI (Worker h 1 ) ∧ II (γ) ∧ E(γ) we obtain the following invariant Φ : Φ =(l 11 ∧ lc 0 ∧ x = y 1 )∨ l 11 ∧ lc 1 ∧ (y 1 = x ∨ x + 4 ≤ y 1 ) ∨ l 21 ∧ lc 2 ∧ (y 1 = x + 4 ∨ x + 8 ≤ y 1 ) .
We used bold fonts in Φ to highlight relations between x and y 1 which are not in CI (Controller ) ∧ CI (Worker 1 ) ∧ II (γ). It can be easily checked now that Φ → ϕ Saf e holds and consequently, this proves that ϕ Saf e holds for the system.

To sum up, the basic steps of our invariant generation method described so far are:

(1) compute the interaction invariant II (γ);

(2) extend the components B i to components with history clocks B h i ; (3) compute component invariants CI (B h i ); (4) compute inequality constraints E(γ) for interactions γ;

(5) finally, eliminate the history clocks in i CI (B h i ) ∧ II (γ) ∧ E(γ). We note that, due to the combination of recursion and disjunction, E(γ) can be large. Much more compact formulae can be obtained by exploiting non-conflicting interactions, i.e., interactions that do not share actions.

Proposition 3.7. If γ = γ 1 ∪ γ 2 such that Act(γ 1 ) ∩ Act(γ 2 ) = ∅ then E(γ) ≡ E(γ 1 ) ∧ E(γ 2 ).
Proof. By induction on the number of interactions in γ. In the base case, γ has a single interaction and the property trivially holds. For the induction step, for the ease of reading, we introduce eq(α) and leq(α, γ) to denote respectively a i ,a j ∈α h a i = h a j and

a i ∈α a k ∈Act(γ α) h a i ≤ h a k . E(γ)
can be rewritten as follows:

E(γ) = α∈γ 1 eq(α) ∧ leq(α, γ) ∧ E((γ 1 ∪ γ 2 ) α) ∨ α∈γ 2 eq(α) ∧ leq(α, γ) ∧ E((γ 1 ∪ γ 2 ) α) using γ 2 α = γ 2 for α ∈ γ 1 and by ind. for γ = (γ 1 α) ∪ γ 2 ≡ α∈γ 1 eq(α) ∧ leq(α, γ) ∧ E(γ 1 α) ∧ E(γ 2 ) ∨ α∈γ 2 eq(α) ∧ leq(α, γ) ∧ E(γ 1 ) ∧ E(γ 2 α) using α∈γ i eq(α) ∧ leq(α, γ i ) ∧ E(γ i α) = E(γ i ) for i ∈ {1, 2} ≡ E(γ 1 ) ∧ E(γ 2 ) ∧ α∈γ 1 leq(α, γ 2 ) ∨ α∈γ 2 leq(α, γ 1 ))
(using totality of "≤" and disjointness of γ i )

≡ E(γ 1 ) ∧ E(γ 2 )
The following corollary is an immediate consequence of Proposition 3.7.

Corollary 3.8. If the interaction model γ has only disjoint interactions, i.e., for any

α 1 , α 2 ∈ γ, α 1 ∩ α 2 = ∅, then E(γ) ≡ α∈γ a i ,a j ∈α h a i = h a j .
The two interactions in γ = {(a | b 1 ), (c | d 1 )} are disjoint. Thus, we can simplify the expression of E(γ) to (h a = h b 1 ) ∧ (h c = h d 1 ).

3.2.

History Clocks for Interactions. The equality constraints on history clocks allow to relate the local constraints obtained individually on components. In the case of nonconflicting interactions, the relation is rather "tight", that is, expressed as conjunction of equalities on history clocks. In contrast, the presence of conflicts lead to a significantly weaker form. Intuitively, every action in conflict can be potentially used in different interactions. The uncertainty on its exact use leads to a disjunctive expression as well as to more restricted equalities and inequalities amongst history clocks.

Nonetheless, the presence of conflicts themselves can be additionally exploited for the generation of new invariants. That is, in contrast to equality constraints obtained from interactions, the presence of conflicting actions enforce disequalities (or separation) constraints between all interactions using them. In what follows, we show a generic way of automatically computing such invariants enforcing differences between the timings of the interactions themselves. To effectively implement this, we proceed in a similar manner as in the previous section: we again make use of history clocks and corresponding resets but this time we associate them to interactions, at the system level. Definition 3.9 (System with Interaction History Clocks). Given a timed system γ B i , its extension with history clocks for interactions is the timed system B * γ h B h i where: • B * is an auxiliary component ({l * }, A γ , H γ , T, (l * → true), (l * , true)) where:

the set of actions

A γ = {a α | α ∈ γ} -the set of interaction history clocks H γ = {h α | α ∈ γ} -the set of transitions T = {(l * , (a α , true, {h α }), l * ) | α ∈ γ} • γ h = {(a α | α) | α ∈ γ} with (a α | α) denoting {a α } ∪ {a | a ∈ α}.
As before, it can be shown that any invariant of B * γ h B h i corresponds to an invariant of γ B i . The history clocks for interactions do not impact the behaviour and henceforth the two systems are bisimilar. Proposition 3.10.

(

) If Φ h is an invariant of B * γ h B h i , then Φ = ∃H A ∃H γ .Φ h is an invariant of γ B i . (2) If Φ h is an invariant of B * γ h B h i and Ψ h an inductive predicate of B * γ h B h i ex 1

pressed on history clocks for actions and interactions H

γ ∪ H A \ {h 0 } then Φ = ∃H A ∃H γ .(Φ h ∧ Ψ h ) is an invariant of γ B i .
Proof. Similar to Proposition 3.2.

We use history clocks for interactions to express additional constraints on their timing. The starting point is the observation that when two conflicting interactions compete for the same action a, no matter which one is first, the latter must wait until the component which owns a is again able to execute a. This is referred to as a "separation constraint" for conflicting interactions. Definition 3.11 (Separation Constraints for Interaction Clocks). Given an interaction set γ, the induced separation constraints, S(γ), are defined as follows:

S(γ) = a∈Act(γ) α =β∈γ a∈α∩β | h α -h β |≥ k a
where | x | denotes the absolute value of x and k a is a constant computed locally on the component executing a, and representing the minimum elapsed time between two consecutive executions of a.

In our running example the only conflicting actions are a and c within the controller, and both k a and k c are equal to 4. The expression of the separation constraints reduces to:

S((a | b i ) i , (c | d i ) i ) ≡ i =j |h c|d i -h c|d j | ≥ 4 ∧ i =j |h a|b i -h a|b j | ≥ 4. Proposition 3.12. Let S * (γ) = a∈Act(γ) α =β∈γ a∈α∩β (h a ≤ h α ≤ h β -k a ∨ h a ≤ h β ≤ h α -k a )
We have that:

(1) S * (γ) is an inductive predicate of B * γ h B h i .

(2) The equivalence S(γ) ≡ ∃H A .S * (γ) is a valid formula.

Proof. (1) Let us fix an arbitrary term S(a, α, β) defined as

S(a, α, β) = (h a ≤ h α ≤ h β -k a ∨ h a ≤ h β ≤ h α -k a )
Assume S(a, α, β) holds in an arbitrary state s of B * γ h B h i . Then, it obviously holds for any time successors as well as for any discrete successors by interactions not containing the action a. For an interaction involving a, but different than α and β, h a is reset to zero whereas h α and h β are unchanged. Henceforth, S(a, α, β) remains valid as only h a changes to 0. Let consider the situation α is executed (the case of β is perfectly dual). In this case, both h a and h α are reset to 0, whereas h β is unchanged. Two situations can happen:

(a) h a ≤ h α ≤ h β -k a holds in s. Then, obviously, the same holds in s where h a and h α are reset. (b) h a ≤ h β ≤ h α -k a holds in s. This is the interesting case where we need the assumption about the separation time k a . As consecutive executions of a are separated by k a , to execute α it must actually hold that h a ≥ k a in s. Consequently, h β ≥ k a in s, as well as in s (because h β does not change from s to s ). Then, knowing that h a = h α = 0 in s we have that h a ≤ h α ≤ h β -k a in s . (2) We can equivalently write

S * (γ) ≡ a∈Act(γ) α =β∈γ a∈α∩β (h a ≤ h α ∧ h a ≤ h β ∧ | h α -h β |≤ k a ) ≡ S(γ) ∧ a∈Act(γ) α =β∈γ a∈α∩β (h a ≤ h α ∧ h a ≤ h β )
and this concludes our proof.

The predicate S(γ) is expressed over history clocks for interactions. Component invariants CI (B h i ) are however expressed using history clocks for actions. In order to "glue" them together in a meaningful way, we need some tighter connection between action and interaction history clocks. This aspect is addressed by the constraints E * defined below. Definition 3.13 (E * ). Given an interaction set γ, we define E * (γ) as follows:

E * (γ) = a∈Act(γ) h a = min α∈γ,a∈α h α .
By a similar argument as the one in Proposition 3.4, it can be shown that E * (γ) is an inductive predicate of the extended system B * γ h B h i . Moreover, there exists a tight connection between E and E * as given in Proposition 3.14.

Proposition 3.14.

(

) E * (γ) is an inductive predicate of B * γ h B h i . (2) The equivalence ∃H γ .E * (γ) ≡ E(γ) is a valid formula. 1
Proof. [START_REF] Abdellatif | Model-based implementation of real-time applications[END_REF] To see that E * (γ) is an inductive predicate it suffices to note that the predicate is preserved by time progress transitions and for any discrete action a, there is always an interaction α containing a such that h a and h α are both reset in the same time.

(2) The proof follows directly from the definitions of E(γ) and E * (γ). Consider that γ = {α 1 , α 2 , ..., α m }. We have the following equivalences:

∃H γ .E * (γ) ≡ ∃H γ . α k 1 ≺α k 2 ≺...≺α km h α k 1 ≤ h α k 2 ≤ ... ≤ h α km ∧ E * (γ)
(by choosing an arbitrary ordering ≺ on interactions)

≡ ∃H γ . α k 1 ≺α k 2 ≺...≺α km h α k 1 ≤ h α k 2 ≤ ... ≤ h α km ∧ a∈α k 1 (h a = h α k 1 ) ∧ a∈α k 2 \α k 1 (h a = h α k 2 ) ∧ ... a∈α km \α k 1 ...α k m-1 (h a = h α km )
(by expanding the definition of E * (γ) along the chosen order)

≡ ∃H γ . α k 1 ≺α k 2 ≺...≺α km h α k 1 ≤ h α k 2 ≤ ... ≤ h α km ∧ m =1 a∈α k \α k 1 ...α k -1 (h a = h α k )
(by rewriting to a more compact form)

≡ α k 1 ≺α k 2 ≺...≺α km ∃H γ . h α k 1 ≤ h α k 2 ≤ ... ≤ h α km ∧ m =1 a∈α k \α k 1 ...α k -1 (h a = h α k )
(by distributing the existential quantifiers over the disjunction)

≡ α k 1 ≺α k 2 ≺...≺α km m =1 a i ,a j ∈α k \α k 1 ...α k -1 a k ∈α k 1 ...α k (h a i = h a j ≤ h a k ) ≡ E(γ)
(by eliminating the existential quantifiers)

From Propositions 3.14, 3.10, and 3.12, it follows that

∃H A ∃H γ .( i CI (B h i ) ∧ II (γ) ∧ E * (γ) ∧ S(γ)) is an invariant of γ B i . This new invariant is in general stronger than ∃H A .( i CI (B h i ) ∧ II (γ) ∧ E(γ)
) and it provides better state space approximations for timed systems with conflicting interactions.

Corollary 3.15. Φ = ∃H A ∃H γ .( i CI (B h i ) ∧ II (γ) ∧ E * (γ) ∧ S(γ)) is an invariant of γ B i . Example 3.16.
To get some intuition about the invariant generated using separation constraints, let us reconsider the running example with two workers. The subformula which we emphasise here is the conjunction of E * and S. The interaction invariant is:

II (γ) =(l 11 ∨ lc 1 ∨ lc 2 ) ∧ (l 12 ∨ lc 1 ∨ lc 2 ) ∧ (lc 2 ∨ l 11 ∨ l 12 ) ∧ (lc 0 ∨ lc 1 ∨ l 21 ∨ l 22 )
The components invariants are:

CI (Controller h ) =(lc 0 ∧ x = h 0 ∧ h 0 < h a ∧ h 0 < h c ) ∨ (lc 1 ∧ x ≤ h 0 -8 ∧ x ≤ 4 ∧ h 0 < h a ∧ h 0 < h c ) ∨ (lc 1 ∧ x ≤ 4 ∧ x = h c ≤ h a ≤ h 0 -12) ∨ (lc 2 ∧ x ≤ h 0 -12 ∧ h a = x ∧ h 0 < h c )) ∨ (lc 2 ∧ x = h a ∧ h c = h a + 4 ≤ h 0 -12) CI (Worker h i ) =(l 1i ∧ y i = h 0 ∧ h 0 < h d i ∧ h 0 < h b i ) ∨ (l 1i ∧ y i = h d i ≤ h b i ≤ h 0 -8) ∨ (l 2i ∧ y i ≥ h b i + 8 ≤ h 0 < h d i )) ∨ (l 2i ∧ y i = h d i ≤ h 0 -8 ∧ h b i ≤ h d i -8)
The inequalities for action and interaction history clocks are:

E * (γ) =(h b 1 = h a|b 1 ) ∧ (h b 2 = h a|b 2 ) ∧ (h a = min i=1,2 (h a|b i ))∧ (h d 1 = h c|d 1 ) ∧ (h d 2 = h c|d 2 ) ∧ (h c = min i=1,2 (h c|d i ))
By recalling the expression of S(γ) we obtain that:

∃H γ .E * (γ) ∧ S(γ) = (|h b 2 -h b 1 | ≥ 4 ∧ |h d 2 -h d 1 | ≥ 4)
and thus, after quantifier elimination in

∃H A ∃H γ .(CI (Controller h ) ∧ i CI (Worker h i ) ∧ II (γ) ∧ E * (γ) ∧ S(γ))
after simplification, we obtain the following invariant Φ:

Φ = l 11 ∧ l 12 ∧ lc 0 ∧ x = y 1 = y 2 ∨ l 11 ∧ l 12 ∧ lc 1 ∧ x ≤ 4 ∧ (y 1 = y 2 ≥ x + 8∨ (y 1 = x ∧ y 2 -y 1 ≥ 4)∨ (y 1 ≥ x + 8 ∧ y 1 -y 2 ≥ 8)∨ (y 2 = x ∧ y 1 -y 2 ≥ 4)∨ (y 2 ≥ x + 8 ∧ y 2 -y 1 ≥ 8)) ∨ l 21 ∧ l 12 ∧ lc 2 ∧ y 1 ≥ x + 8 ∧ ((y 2 ≥ x + 4 ∧ |y 1 -y 2 | ≥ 4)∨ y 2 ≥ x + 12 ) ∨ l 11 ∧ l 22 ∧ lc 2 ∧ y 2 ≥ x + 8 ∧ ((y 1 ≥ x + 4 ∧ |y 1 -y 2 | ≥ 4)∨ y 1 ≥ x + 12 )
We emphasised in the expression of Φ the newly discovered constraints. All in all, Φ is strong enough to prove that the system is deadlock free.

We conclude the section with a discussion about the computation of the separation constants k a . A simple but incomplete heuristics to test that a given value k a is a correct separation constraint for an action a is as follows. Consider all paths connecting two transitions (not necessarily distinct) labelled by a. If on every such path, there exists a clock x which is reset and then tested in a guard x ≥ ct, with ct ≥ k a then, it is safe to conclude that actually k a is a correct separation value. Nonetheless, alternative methods to exactly compute k a have been already proposed in the literature. For details, the interested reader can refer, for instance, to [START_REF] Courcoubetis | Minimum and maximum delay problems in real-time systems[END_REF] which reduces this computation to finding a shortest path in a weighted graph built from the zone graph associated to the component.

Improving (VR) -Three Heuristics

We describe and elaborate on heuristics allowing to strengthen the generated invariants and to reduce the generation time. These heuristics have been successfully applied on our case studies considered later in Section 5.

4.1.

Refining conflicting interactions. The initialisation of the history clock h 0 provides a convenient way to express and reason about invariants relating occurences of various actions and interactions at execution. The assertion h α ≤ h 0 has the intuitive meaning that "α has been executed". We describe below a new family of invariants providing a finer characherisation for the execution of conflicting interactions and related actions.

We fix a as a potential conflicting action within some component B = (L, A, T, X , tpc). We define the set of preceding actions P rec(a) as all actions of B that can immediately precede a in an execution, formally P rec(a) = {a ∈ A | ∃l, l , l ∈ L. l a → l , l a → l }. For any two conflicting interactions α 1 , α 2 involving a, the following assertion:

h α 1 ≤ h 0 ∧ h α 2 ≤ h 0 ⇒ a ∈P rec(a)
h a ≤ h 0 is an invariant. Intuitively, the assertion states that whenever α 1 and α 2 have both been executed (implying that a has also been executed two or more times), at least one of the preceding actions of a must also has been executed. We remark that the invariant above is rather weak and can be implied by the component invariant CI(B) and the glue invariant E * in many situations. In fact, whenever a is an action which is not enabled at the initial location of B, the component invariant CI(B) implies that

h a ≤ h 0 ⇒ a ∈P rec(a) h a ≤ h 0 .
This states that whenever a has been executed, at least one of its preceding actions has been executed as well. Knowing moreover that h a = min a∈α h α , we can then infer the invariant above.

Nonetheless, if a is an action that is enabled at the initial location, the newly proposed invariant is stronger and cannot be derived as shown before. In this case, a can be actually executed once while none of its predecessors has been executed yet. The component invariant alone does not relate anymore the execution of a to the execution of its preceding actions. Moreover, the component invariant considers always the last occurence of a and has no means of distinguishing cases where a has been executed only once or more often. This information can sometimes be re-discovered when interaction history clocks h α 1 , h α 2 are taken into account, henceforth, leading to the proposed invariant. A concrete illustration is provided later in Section 5.

Invariant computation using regular expressions.

There exist situations where the computation of component invariants can be extremely costly. In particular, for untimed components extended with history clocks, their zone graphs will most likely have an exponential size. In fact, due to history clocks, the zones will record the order of (the last) occurences of actions, and there could be exponentially many of them, reachable at different locations. We note that, in timed components, clocks restrict the dynamics of the components, consequently, it cannot be the case that all the orders are possible.

The above observation suggests (and was confirmed by our experiments) that applying the same methodology for computing component invariants (based on the reachability graph of the corresponding components with history clocks) regardless of the components being timed or not leads to large formulae when possibly shorter ones exist.

Example 4.1. Consider the untimed component presented in Figure 3 (left) and its extension with history clocks (right). The entire zone graph reachable from l 0 , ζ 0 , with ζ 0 = (h 0 = 0, h a,b,c > 0) has 6 symbolic states. Therefore, the component invariant is expressed as a disjunction of 16 terms, 9 of them are related to location l 0 and 7 are related to location l 1 .

We recall that untimed automata have elegant and compact encodings as regular expressions. This basic fact can be exploited in order to provide an alternative computation method for component invariants. More concretely, given an untimed component B = (L, A, T ) we show how to automatically compute the invariant describing the relations between the history clocks of B h at some location , from the language accepted by B at some designated location . The first key observation is that only the last occurrence of each action should be retained. This implies that it is safe to abstract, with respect to last occurrences, the regular expression characterising the language accepted at the chosen control location. The second key observation is that, regular expressions in some restricted form, can be used to directly generate less constraints on the history clocks. Our regular expression based method can be therefore summarised as follows:

(1) construct the regular expression E representing the language accepted by B at location , ( 2) abstract E with respect to the last occurence retention towards some restricted form E = i e i where, every e i contains each action at most once, and does not contain nested *-operators, (3) generate from every e i a characteristic formula on history clocks φ(e i ) and obtain as invariant for B the assertion ⇒ ∨ i φ(e i ). The first step is well known for finite automata and will not be detailed here. For the second abstraction step, the key ingredients are the simplification rules in Figure 4. Rule 1 eliminates all but the last occurrence of the trailing a symbol from a regular expression of the form E • a. The " " denotes a syntactic elimination operator defined structurally on expressions as follows. Let a and x be two symbols and E, E 1 and E 2 be arbitrary regular expressions.

Rule 1 [Last Occurrence Retention]:

E • a -→ (E a) • a Rule 2 [Back-unfolding]: E * -→ (E * • E) + ε
a = x a = if x = a x if x = a (E 1 + E 2 ) a = (E 1 a) + (E 2 a) (E 1 .E 2 ) a = (E 1 a).(E 2 a) E * a = (E a) *
Rule 2 simply unfolds *-expressions once. By using this rule and other basic manipulation of regular expressions, further simplification opportunities for Rule 1 are enabled. In the example above, we have applied the iterative strategy consisting of (1) choosing symbols from right to left and applying Rule 1 until no longer possible and then (2) applying Rule 2 to unfold the rightmost *-expression and split the incoming +. It can be shown that such a strategy always terminates with expressions in the restricted form. Intuitively, what happens is that Rule 2 splits larger expressions into smaller ones and, further, for each of these Rule 1 eliminates repetitions of symbols.

For the third step, we construct from a regular expression e in restricted form an equivalent formula φ(e ) on history clocks. This formula represents exactly the set of orders on actions (the strings) encoded by the regular expression:

φ(e ) ≡ a 1 ...an∈L(e ) distinct a 1 ,...,an h 0 ≥ h a 1 ≥ ... ≥ h an ∧ c =a 1 ,...,an h c > h 0
where L(e ) is the language of e . We note that since we only consider words with distinct symbols, they are finitely many and the disjunction is finite as well.

As an illustration, let e be the regular expression in the restricted form a * bc + (a + c) * b obtained in Example 4.2. The finite words on which φ(e ) builds upon are abc and bc (from a * bc) and acb, cab, cb, ab, b from (a + c) * b. By applying the above encoding, we obtain:

(h 0 ≥ h a ≥ h b ≥ h c ) ∨ (h a > h 0 ≥ h b ≥ h c ) ∨
(corr. to abc, resp. bc)

(h 0 ≥ h a ≥ h c ≥ h b ) ∨ (h 0 ≥ h c ≥ h a ≥ h b ) ∨ (corr. to acb, resp. cab) (h a > h 0 ≥ h c ≥ h b ) ∨ (h c > h 0 ≥ h a ≥ h b ) ∨ (corr. to cb, resp. ab) (h 0 ≥ h b ∧ h c , h a > h 0 ) (corr. to b)
Such encodings are, in fact, invariants. Intuitively, the inequalities in φ(e ) reflect precisely the order in which the last action occurences have taken place. Proposition 4.3. Let B be an untimed component, E l the regular expression characterising the language accepted by B at location l, and E l be the result of applying the simplification rules. We have that l (l ∧ φ(E l )) is an invariant of B h .

Proof. (sketch) The local component invariant at some location l is precisely characterised by the orders of the last occurrences of actions on traces reaching l. To show that these orders are captured by φ(E l ), it suffices to note that, on the one hand, E l and E l preserve the language of the last occurrences of actions. This follows from the simplification rules. As for regular expressions e in restricted form we can prove the following property. For every word w in L(e ), the restricted sub-word w loc obtained from w by removing all but last occurrences of every symbol belongs to L(e ) as well. Henceforth, one can enumerate over all last occurrence words w loc by simply considering all accepted words of L(e ) having distinct symbols. To conclude the proof we only need to note that the inequalities in φ(E l ) encode the enumeration of all possible words corresponding to traces of B h ending at l.

We can exploit the structure of regular expressions in restricted form to optimise the technique described above even further. To illustrate this, we consider the regular expression (b 1 + ... + b m ) * a 1 ...a n in restricted form (whenever a 1 , ..., a n , b 1 , ..., b m are distinct). The corresponding formula on history clocks is

h 0 ≥ h a 1 ≥ ... ≥ h an ∧ h b 1 ≥ h a 1 ∧ ... ∧ h bm ≥ h a 1 ∧ c =a i ,b j h c > h 0 .
The first part encodes the ordering constraints on the mandatory string a 1 ...a n . All these actions occur (consequently, their history clocks are smaller than h 0 ) in this precise order. The second part considers constraints on occurences of b j actions, which are optional: if some occur, their executions are unconstrained by each other, however, they take place before a 1 . Finally, the last part deals with actions c which do not appear in the regular expression. For all of them, their history clocks should be strictly greater than h 0 . We remark that, for this particular example, the obtained formula has linear size with respect to the size of the regular expression. In contrast, the number of strings encoded (i.e., whenever restricted to last occurrences of symbols) is exponential, with respect to the number of b actions. The construction above can be generalised for arbitrary restricted regular expressions without much difficulty. The resulting formula remains of polynomial size (at worse quadratic) with respect to the size of the restricted regular expression provided as input.

Example 4.4. Following the approach described above, the regular expression in the restricted form a * bc + (a + c) * b translates into:

(h 0 ≥ h b ≥ h c ∧ h a ≥ h b ) ∨ (h 0 ≥ h b ∧ h a ≥ h b ∧ h c ≥ h b )
We note this expression is significantly smaller, yet logically equivalent to the disjunction of 7 distinct terms corresponding to symbolic zones reached at l 1 as initially presented in Example 4.1.

To sum up, we described a heuristic which can be applied to untimed components to automatically compute an invariant with a reasonable enough size to be handled by existing SMT solvers. Given an untimed component B, our heuristic makes use of the regular expressions characterizing the language accepted by B to avoid a direct construction of the zone graph of B h which would result in considerably large invariants. 4.3. Exploiting Symmetry. At a closer examination of the definition of separation constraints in Section 3.2, it can be noticed that it characterises all possible orderings of conflicting interactions with respect to permutations. The size of the corresponding search space is exponential in the number of conflicting interactions and this, in turn, may be a bottleneck for the solver. Such situations can and must be avoided especially in the case of symmetric systems. What we show next is how the inherent symmetry in the formula can be eliminated such that the search space becomes considerably smaller.

The use of symmetry has long been addressed, mostly with the intention of making model-checking more feasible and especially in the context of parameterised systems [START_REF] Emerson | Reasoning about rings[END_REF][START_REF] Emerson | Symmetry and model checking[END_REF][START_REF] Emerson | Reducing model checking of the many to the few[END_REF][START_REF] Namjoshi | Symmetry and completeness in the analysis of parameterized systems[END_REF]. There the goal is to show the existence of a small cutoff bound which allows the reduction of the verification problem from an arbitrary number of instances to a small, fixed one. Our context is different, that is, breaking the symmetry in some of the generated invariants, for an a priori known number of components.

The types of systems we consider next are formed of a fixed number, be it n, of isomorphic components interacting with a controller, thus the interactions are binary. Isomorphic components are obtained from a generic component B by attaching an index i (from 1 to n) to all symbols in B . The resulting component is denoted by B i . For any i, j, B i and B j are isomorphic 6 . For the ease of reference, we denote systems like C n γ B i by the letter M and we use Exec to denote the set of their global executions.

In this framework, the notion of symmetry is intrinsically related to permutations. Let Π n denote the group of permutations of n. The application of permutations is defined on the structure of systems and properties. For a system M as C n γ B i , and a permutation π, π(M ) is defined as

C n π(γ) π(B i ) where π(B i ) is defined as B π(i) and π(γ) as {π(α) | α ∈ γ} with π(a c | a i ) = a c | a π(i)
for α an arbitrary binary interaction between an action a c of C and an action a i of a B i . For an execution σ = α 1 , . . . α i , . . . α k , π(σ) is defined as π(α 1 ), π(α 2 ) . . . π(α i ), . . . , π(α k ). For a global state s = (s c , s 1 , . . . , s n ), π(s) is defined as (s c , s π(1) , . . . , s π(n) ). As for system properties ϕ, we restrict to those built (with the usual logical connectors) from clock constraints and locations, and define:

π(ϕ) =          x π(i) rop x π(j) if ϕ = x i rop x j and rop ∈ {<, ≤, =, >, ≥} l π(i) if ϕ = l i ¬π(ϕ 1 ) if ϕ = ¬ϕ 1 π(ϕ 1 ) op π(ϕ 2 ) if ϕ = ϕ 1 op ϕ 2 and op ∈ {∧, ∨}
where l i , x i denote a location, respectively, a clock in B i .

The symmetric systems we consider are symmetric in a "strong" sense, i.e., they are fully symmetric. A system M is fully symmetric if for any π ∈ Π n , π(M ) is syntactically identical to M . Similarly, a property ϕ is fully symmetric if for any permutation π, π(ϕ) is equivalent to ϕ. A property like l 1 ∧ l 2 ∧ ... ∧ l n is symmetric. On the contrary, G = x 1 ≤ x 2 is not as for the permutation π

(1) = 2, π(2) = 1, π(G) = x π(1) ≤ x π(2) = x 2 ≤ x 1 which is not equivalent to G.
Symmetric systems have the convenient property that, whenever started in a symmetric state, for any of its executions σ ∈ Exec, π(σ) is itself an execution, that is, π(σ) ∈ Exec. To see why this is indeed the case, let γ be the interaction set and α = (a c | a i ) an interaction in γ. It suffices to note that if α is possible after σ, then it is also the case for π(α) after π(σ). Note also that, thanks to symmetry, π(α) is in γ.

The idea behind simplifying the separation constraints S is to break the symmetry by replacing the constraints on absolute values | h α i -h α j |. More precisely, given a conflicting (controller) action a c , in an execution where interaction α i = a c | a i executes before α j = a c | a j for j > i, we can naturally replace | h α i -h α j | by h α i -h α j . As for an execution which violates this natural ordering (or "canonicity"), we show that we can make use of symmetry to rearrange it. First, we formalise what we mean more precisely by canonicity. Given an execution σ and an interaction α i = a c | a i we denote by lpos(σ, α i ) the last position of α i in σ. An execution σ is canonical with respect to a c if lpos(σ, α i ) < lpos(σ, α j ) for any i < j. Let Exec c be the set of canonical executions. Thanks to symmetry, any execution has a corresponding canonical execution. Assume σ is such that there is a conflicting a c 6 We note that, by construction, isomorphic components cannot have clock constraints involving indices: any constraint in a worker Bi is obtained from those in B which are oblivious to indices i. and for i > j the last occurrence of α i = a c | a i appears latter than that of α j = a c | a j . Let π be such that π(i) = j and π(j) = i. Then π(σ) is itself an execution and is canonical.

For a canonical execution with a c being the action of interest S simplifies to:

S c (γ) = i<j ac∈α i ∩α j h α i -h α j ≥ k ac ∧ b =ac b∈β i ∩β j | h β i -h β j |≥ k b
We note that S c reduces S by n!. This is the best we can get in general. However, under particular conditions, S can be further reduced. For instance, if the controller is such that it considers components one by one and moreover, requires the use of some designated action a c , then S further reduces to:

a∈Act(C) i<j a∈α i ∩α j h α i -h α j ≥ k ac
This is because by considering components one by one, all conflicting interactions involving the controller follow the same order as defined for the designated action a c . We anticipate and note that such a scenario is the "temperature controller" case study from Section 5. Finally, we show that for symmetric systems and properties it is correct to consider S c instead of S. Proposition 4.5. Let M be a symmetric system, ϕ be a symmetric property and Φ the global invariant as defined in Section 3.2. We have that if Φ[S ← S c ] → ϕ then M |= ϕ.

Proof. (sketch) It suffices to show that Φ[S ← S c ] → ϕ iff Φ → ϕ. "⇐": trivial. "⇒": It boils down to show that if ϕ is an invariant of Exec c then it is also an invariant of the remaining executions σ in Exec \ Exec c . If σ does not have a conflicting action, we are done, as S c is an invariant by default. Else, we make use of the fact that σ has a canonical representation and that ϕ is symmetric.

An immediate application of the above reduction results in the simplification we make use of in the temperature controller example from Section 5. Naturally, the results can be extended also to systems with less symmetry by adapting the standard constructions of automorphisms from, for example, [START_REF] Emerson | Symmetry and model checking[END_REF]. More precisely, for a system M for which Aut(M ) = {π | π(M ) = M } is a proper subgroup of Π n , we need to restrict to canonical executions which are consistent with the permutations in Aut(M ). However, though such a generalisation is possible, it is not clear if it is also useful: as it is well pointed out in the literature about symmetries, determining Aut(M ) is, in itself, a hard problem. This, together with the goal of keeping the presentation as clear as possible, were the reasons why we strictly considered only fully symmetric systems.

Implementation and Experiments

The method has been implemented in the RTD-Finder tool designed to check safety properties for real-time component-based systems modelled in the RT-BIP language [START_REF] Abdellatif | Model-based implementation of real-time applications[END_REF]. The tool and the examples are available at http://www-verimag.imag.fr/RTD-Finder.

In RT-BIP, components are modelled as timed automata and synchronise by means of n-ary multi-party interactions. The tool takes as input a real-time BIP model and a file containing the safety property. It subsequently generates a Yices [START_REF] Dutertre | The Yices SMT solver[END_REF] output file where the invariants are expressed together with the property. RTD-Finder proceeds by the following steps. It extends the components with history clocks and computes their local invariants. The computation of those invariants requires the implementation of several operations on zones. For this purpose, we developed a DBM (Difference Bound Matrices) library. RTD-Finder subsequently computes the history clocks constraints and the interaction invariant. It writes all these invariants to a file and calls Yices to check the satisfiabilty of GI∧¬Ψ. If GI∧ ¬Ψ is unsatisfiable, the property is valid. Otherwise, Yices generates a counter-example. We note that, at present, the tool cannot conclude if it is a valid counter-example, however, a guided backward analysis module is currently under development. The benchmarks we used in our experiments with RTD-Finder are described in what follows.

5.1. Train gate controller (TGC). This is a classical example from [START_REF] Alur | A theory of timed automata[END_REF]. The system is composed of a controller, a gate and a number of trains. For simplicity, Figure 5 depicts only one train interacting with the controller and the gate. The controller lowers and raises the gate when a train enters, respectively exits. We propose to check that when all the trains are at far location, the gate cannot be going down (g 2 location). The results are presented in Table . 1. When there are more than one train, be it n, the interactions approach i | approach (respectively exit i | exit), for 1 ≥ i ≥ n are in conflict on approach (respectively exit) of the controller. In this case, in addition to the separation constraints, we made use of the first heuristic presented in Section 4.1. More precisely, the invariant generated by the heuristic is as follows:

i =j (h approach i ≤ h 0 ∧ h approach j ≤ h 0 ) → h raise ≤ h 0 f ar 1 near 1 x 1 ≤ 5 in 1 x 1 ≤ 5
Train approach x := 0 Fischer protocol. This is a well-studied protocol for mutual exclusion [START_REF] Lamport | A fast mutual exclusion algorithm[END_REF]. The protocol specifies how processes can share a resource one at a time by means of a shared variable to which each process assigns its own identifier number. After θ time units, the process with the id stored in the variable enters the critical state and uses the resource.

x 1 ≥ 3 exit 1 approach 1 exit 1 c 0 c 1 z ≤ 1
We use an auxiliary component Id Variable to mimic the role of the shared variable. The system with two concurrent processes is represented in Figure 6. The property of interest is mutual exclusion: (cs i ∧ cs j ) → i = j.

The component Id Variable has combinatorial behavior and a large number of actions (2n + 1), thus the generated invariant is huge except for very small values of n. To overcome this issue, we made use of the second heuristic presented in Section 4.2. To simplify, we write s i instead of set i and e i instead of eq i . We construct the regular expression corresponding to location l i and project it for actions e i , e j , s i , s j , respectively e i , e 0 , s i , s 0 . The latter projection leads to the following regular expression in restricted form: R i = (e 0 + s 0 ) * e i .s i + (e 0 + s 0 ) * s i .e i + (e 0 + e i ) * s 0 s i + (e i + s 0 ) * e 0 s i + s i This regular expression translates into the following constraint on history clocks:

φ(R i ) =(h e 0 ≥ h e i ∧ h s 0 ≥ h e i ∧ h e i ≥ h s i ∧ h e i ≤ h 0 ) ∨ (h e 0 ≥ h s i ∧ h s 0 ≥ h s i ∧ h e i ≤ h s i ∧ h s i ≤ h 0 ) ∨ (h e 0 ≥ h s 0 ∧ h e i ≥ h s 0 ∧ h s 0 ≥ h s i ∧ h s 0 ≤ h 0 ) ∨ (h s 0 ≥ h e 0 ∧ h e i ≥ h e 0 ∧ h e 0 ≥ h s i ∧ h e 0 ≤ h 0 ) ∨ (h s i ≤ h 0 ∧ h s 0 , h e 0 , h e i > h 0 )
We deduce that at(l i ) → φ(R i ) is an invariant of the Id Variable, for any i. These invariants in addition to component invariants of processes and inequality constraints E(γ) are sufficient to show that mutual exclusion holds. 3. Gear controller system. Our third example is taken from [START_REF] Lindahl | Formal design and analysis of a gear controller[END_REF]. There it is described a model of gear controller components in embedded systems operating inside vehicles. A gear controller system is composed of five components: an interface, a controller, a clutch, an engine and a gear-box. The interface sends signals to the controller to change the gear. In turn, the controller interacts with the engine, the clutch and the gear-box. The engine is either regulating the torque or synchronising the speed. The gear-box sets the gear between some fixed bounds. The clutch works as the gear-box and it is used whenever the engine is not able to function correctly (under difficult driving conditions, for instance).

S 1 S 2 S 0 Id Variable eq 1 , set 1 eq 2 , set 2 eq 0 set 1 set 2 set 2 set 1 eq 0 eq 2 set 2 eq 1 set 1 i 1 r 1 x 1 ≤ θ w 1 cs 1 Process 1 try 1 , x 1 := 0 set 1 x 1 := 0 enter 1 , x 1 > θ enter 1 try 1 set 1 i 2 r 2 x 2 ≤ θ w 2 cs 2 Process 2 try 2 , x 2 := 0 set 2 x 2 := 0 enter 2 , x 2 > θ
One requirement that such a system should satisfy in order to be correct is predictability. This requirement ensures a strict order between components. For instance, it ensures that when the engine is regulating the torque, the clutch is closed and the gear-box sets the gear. Another property of interest that we checked is that the controller is in an error location only when one of the other four components is in an error location also.

5.4.

Temperature controller (TC). This example is an adaptation from [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]. It represents a simplified model of a nuclear plant. The system consists of a controller interacting with an arbitrary number n of rods (two, in Figure 7) in order to maintain the temperature between the bounds 450 and 900: when the temperature in the reactor reaches 900 (resp. 450), a rod must be used to cool (resp. heat) the reactor. The rods are enabled to cool only after 900n units of time. The global property of interest is the absence of deadlock, that is, the system can run continuously and keep the temperature between the bounds. When the controller should take the cool action, at least one of the rods is ready to synchronise with it. For one rod, E(γ) is enough to show the property. For more rods, because interactions are conflicting, we need the separation constraints which basically bring as new information conjunctions as ∧ i (h rest π(i) -h rest π(i-1) ≥ 1350) for π an ordering on rods. Recalling the discussion from Section 4.3, such a reduction is correct because the system enjoys the particularly helpful property of being symmetric. As a last benchmark, we consider the verification of a dual chamber implantable pacemaker presented in [START_REF] Jiang | Modeling and verification of a dual chamber implantable pacemaker[END_REF]. A pacemaker is a device for the management of the cardiac rhythm. It paces both the atrium and the ventricle of the heart, and based on sensing both chambers it can activate or inhibit further pacing. The model of pacemakers we experimented with has five components, for (1) keeping the heart rate above a minimum value, (2) maintaining delays between atrial and ventricular activation, (3) preventing pacing the ventricle too fast, filtering noise after (4) ventricular and (5) atrial events. In our experiments, we considered the upper rate limit (URI ) property stating that the ventricles of the heart should not be paced beyond a maximum rate, equal to a constant called TURI. The property states the existence of a minimum time elapse between a ventricular sense (VS ) event and the following ventricular pace (VP ) event. As in [START_REF] Jiang | Modeling and verification of a dual chamber implantable pacemaker[END_REF], we verified the property by translating it into a monitor component which is shown in Figure 8. The actions VS and VP of the monitor are synchronised with those of the other components. We verified that when the monitor reaches the location interval, its clock t is greater than TURI. The corresponding property is interval → t ≥ TURI. Figure 8: Monitor for the upper rate limit property: the interval between a VS venticular event and a VP venticular event should be longer than TURI Our method offers an additional way to check this property without resorting to the monitor. We expressed it by means of the introduced history clocks. The difference between the history clocks relative to those two events is longer than the required time elapse:

(h V P ≤ h V S ∧ h V S ≤ h 0 ) → h V S -h V P ≥ TURI 5.6.
Results. We ran our experiments on a Linux machine with Intel Core 3.20 GHz ×4 and 15.6 GiB memory. The results, synthesised in Table 1, show the potential of our method in terms of accuracy and scalability. In Table 1, n is the number of components, q is the total number of control locations, c (resp. h) is the number of system clocks (resp. history clocks), i is the number of interactions, while t shows the total verification time and t yices is the timed taken by Yices for satisfiability checking of GI ∧ ¬Ψ. To the best of our knowledge, there are no tools to compositionally verify safety properties of timed systems. Consequently, there are no relevant tools to compare RTD-Finder with. Netherveless, we did a small comparison with Uppaal. Uppaal is a well-known modelchecking tool which is highly optimised. For instance, thanks to some reduction techniques, it has better scores on the first example (the TGC system) in particular and on smaller systems in general. Nonetheless, generally, the state space exploration is costly. This can be illustrated by means of the temperature controller example: for 10 rods, Uppaal generated no results after five hours and 436519 explored states. Nevertheless, RTD-Finder checked the property for 300 rods in few minutes, as shown in Table 1. The timings for the RTD-Finder tool are obtained by the java command getCpuTime called to compute the total verification time, while the results for Uppaal come from the command verifyta which comes with the Uppaal 4.1.14 distribution.

Model

Related Work

Automatic generation of invariants for concurrent systems is a long-time studied topic. Yet, to our knowledge, specific extensions or applications for timed systems are rather limited. As an exception, the papers [START_REF] Badban | Automated invariant generation for the verification of real-time systems[END_REF][START_REF] Fietzke | Superposition as a decision procedure for timed automata[END_REF] propose a monolithic, non-compositional method for finding invariants in the case of systems represented as a single timed automaton.

Compositional verification for timed systems has been mainly considered in the context of timed interface theories [START_REF] Alfaro | Timed interfaces[END_REF] and contract-based assume guarantee reasoning [START_REF] David | Compositional verification of real-time systems using Ecdar[END_REF][START_REF] Lin | Automatic generation of provably correct embedded systems[END_REF][START_REF] Alur | MOCHA: modularity in model checking[END_REF]. These methods usually rely upon choosing a "good" decomposition structure and require individual abstractions for components to be deterministic timed I/O automata. Finding the abstractions is in general difficult, however, their construction can be automated by using learning techniques [START_REF] Lin | Automatic generation of provably correct embedded systems[END_REF] in some cases. In contrast to the above, we are proposing a fully automated method generating, in a compositional manner, an invariant approximating the reachable states of a timed system.

Abstractions serve also for compositional minimisation, for instance [START_REF] Berendsen | Compositional abstraction in real-time model checking[END_REF] minimises by constructing timed automata quotients with respect to simulation; these quotients are in turn composed for model-checking. Our approach is orthogonal in that we do not compose at all. Compositional deductive verification as in [START_REF] De Boer | Hoare-style compositional proof systems for reactive shared variable concurency[END_REF] is also orthogonal on our work in that, by choosing a particular class of local invariants to work with, we need not focus on elaborate proof systems but reason at a level closer to intuition.

The use of additional clocks has been considered, for instance, in [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Håkansson | Partial order reduction for verification of real-time components[END_REF]. There, extra reference clocks are added to components to faithfully implement a partial order reduction strategy for symbolic state space exploration. Time is allowed to progress desynchronised for individual components and re-synchronised only when needed, i.e., for direct interaction within components. Clearly, the history clocks in our work behave in a similar way, however, our use of clocks is as a helper construction in the generation of invariants and we totally avoid global state space exploration. Finally, another successful application of extra clocks has been provided in [START_REF] Salah | Compositional timing analysis[END_REF] for timing analysis of asynchronous circuits. There, specific history clocks are reset on input signals and used to provide a new time basis for the construction of an abstract model of output signals of the circuit.

Conclusions

We presented a fully automated compositional method to generate global invariants for timed systems described as parallel compositions of timed automata components using multi-party interactions. The soundness of the method proposed has been proven. In addition, it has been successfully tested on several benchmarks. This method has been implemented in the RTD-Finder tool. The results show that it may outperform the existing exhaustive exploration-based techniques for large systems, thanks to the use of compositionality and over-approximations. Nonetheless, the generated invariant is an over-approximation of the reachable states set and false-positives may raise. To remedy this, we are working on a guided backward analysis module to decide upon their validity. In order to achieve a better integration, we are working on handling richer classes of systems, including systems with data variables and urgencies [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF] on transitions. Actually, urgencies provide an alternative way to constrain time progress, which is more intuitive to use by programmers but very difficult to handle in a compositional way. A second direction of research which is potentially interesting for systems containing identical, replicated components and closely related to the symmetry-based reduction is the application of our method to the verification of parameterised timed systems. Finally, we are considering specific extensions to particular classes of timed systems and properties, in particular, for schedulability analysis of systems with mixed-critical tasks.

Figure 1 :

 1 Figure 1: Compositional verification

3 Figure 2 :

 32 Figure 2: A timed system

Figure 3 :

 3 Figure 3: An untimed component (left) and its extension with history clocks (right).

Figure 4 :

 4 Figure 4: Simplification Rules

Example 4 . 2 .

 42 Let us consider again the example presented in Figure3. The language accepted at l 1 is defined as (a + bc * b) * bc * . This expression is progressively abstracted into the restricted form as follows: (a + bc * b) * bc * (a + c * ) * bc * (by Rule 1) ≡ (a + c * ) * b(c * c + ) (by Rule 2) ≡ (a + c * ) * bc * c + (a + c * ) * b (by splitting the last +) (a + ) * bc + (a + c * ) * b (by Rule 1) ≡ a * bc + (a + c) * b (by standard transformation)

1 Figure 5 :

 15 Figure 5: A controller interacting with a train and a gate

enter 2 try 2 set 2 Figure 6 :

 26 Figure 6: The Fischer protocol

Figure 7 : 5 .

 75 Figure 7: A Controller interacting with two rods

Table 1 :

 1 Results from experiments

	n	q	c	i	h	t	t yices

Acknowledgement. We are grateful to the anonymous referees for their constructive input and for their thorough feedback. We would also like to thank our colleague Mahieddine Dellabani for his help with two benchmarks.

Project 288175 CERTAINTY.