J Julliand
email: jacques.julliand@lifc.univ-fcomte.fr

H Mountassir
email: hassan.mountassir@lifc.univ-fcomte.fr

E Oudot

Incremental Verification of Component-Based Timed Systems

Keywords: Timed τ -simulation, component-based timed systems, incremental development, preservation of properties, Mitl

We are interested in the incremental development, by integration of components, of component-based timed systems, and in particular, in the preservation of their properties during such a development process. We model timed components with timed automata. Their composition is achieved with the classic parallel composition operator for timed automata. The specifications of these timed systems are expressed with the timed linear logic Mitl (Metric Interval Temporal Logic). To guarantee the preservation of properties during an incremental development process, we propose to use τ -simulation relations, adapted for timed systems. First, we extend the classic notion of τ -simulation with timed aspects. As in the untimed case, this relation, called timed τ -simulation, preserves safety properties. To preserve more properties, in particular liveness ones, we present another relation, called divergencesensitive and stability-respecting (DS) timed τ -simulation. This last relation preserves all Mitl properties (and thus liveness ones), but also strong non-zenoness and deadlockfreedom. Moreover, as we put ourselves in a component-based framework, we study if the relations are appropriate to the use of the composition operator that we consider. For this purpose, we study if the relations are compatible with this operator, and if composability and compositionality hold. These three properties are a way to reduce the cost of the verification of the preservation, or even to get it for free. It results that the timed τ -simulation is appropriate with the classic operator since the properties hold without any assumption. However, this is not the case for the DS timed τ -simulation. We implemented the algorithmic verification of the simulations in a tool called Vesta (Verification of Simulation for Timed Automata). The structure of the tool was inspired from the one of the Open-Kronos tool. This allows, as additionnal feature, to connect the models considered in Vesta to the modules of the verification platform Open-Caesar. We show the interest of our method by applying it on a case study, concerning a production cell example.

Motivations

Component-based modeling is a method which receives more and more attention. In particular, timed systems are often modeled this way. Instead of modeling an entire system in one go, it consists in decomposing the system into a set of sub-systems, called components, and to model each component independently. The complete model of the system is obtained by putting together all the components thanks to some parallel composition operator. We distinguish two main classes of properties which can be expressed to guarantee the correctness of such models: local properties and global properties. Local properties express requirements about the behaviour of a component (or subgroup of components) while global properties concern the behaviour of the whole system. Model-checking is a verification method which can be used to ensure that properties hold on the model of the system. For both kind of properties, the procedure consists in general in performing the verification on the complete model. However, model-checking is known to be difficult to apply on large-sized systems. Indeed, it suffers of the so-called state space explosion problem, which is accentuated in the case of timed systems, due to the presence of timing constraints.

Incremental development processes represent an alternative to circumvent this problem. The idea is to obtain the complete model of a system gradually, and, from a verification point of view, to check properties at each step of the development, where the model is small enough for the verification to be run to completion. The goal of this paper is to show how these incremental development processes can be exploited for componentbased timed systems, and to study the impact in practice of the use of such methods, compared to classic verification. We distinguish two kinds of incremental development methods: integration of components and refinement. Given a set of components C 1 , • • • , C n , integration of components consists in considering one component (or group of components), for instance C 1 , and to check its properties in isolation before integrating it with other components. An essential property in this kind of development is composability, i.e., already established properties of C 1 must be preserved by the integration. Refinement is another kind of incremental development. The principle is first to establish an abstract model of the system and to progressively add details to it until getting to a model representing the complete system. Of course, this refinement process must not bring incoherences w.r.t. the abstract model. In particular, properties which hold on the abstract model must be preserved on the detailed version. For component-based systems, refinement consists in giving an abstract model for each component, and then adding details to each one. From a verification point of view, the goal is double: checking local properties of the components on their abstract model, and verifying global properties on the entire abstract model, obtained by the assembling of all abstract components. An important property is compositionality, meaning that if each detailed version of the components refines the abstract one, then the complete detailed model is a refinement of the complete abstract model. When using such incremental methods, a major issue concerns the preservation of already checked properties. A way to ensure preservation is to compare the behaviour of the models, i.e., the model on which verification is performed and the model on which preservation must be ensured. This comparison must be done on some criteria, depending on the properties which must be preserved. Several equivalence relations or preorders have been defined to compare two systems: equivalence relations are generally used to test the "equality" between two systems modulo the relation, while preorders rather represent an implementation relation. In [START_REF] Glabbeck | The Linear Time -Branching Time Spectrum[END_REF], twelve equivalence relations such as bisimulation, simulation or trace equivalences, and their associated preorder, are defined for (untimed) transition systems and are ordered according to a linear-branching time hierarchy. These relations are reconsidered in [START_REF] Glabbeck | The Linear Time -Branching Time Spectrum II ; The semantics of sequential systems with silent moves[END_REF]) by taking into account internal activity of the systems.

We are interested in the simulation preorder. Indeed, this kind of relation has already been used in the untimed case as a formalization of the refinement process to guarantee preservation of properties. For instance, [START_REF] Bellegarde | Ready-simulation is not Ready to Express a Modular Refinement Relation[END_REF] formalizes the refinement of (untimed) transition systems as a kind of τ -simulation which preserves Ltl properties. We present here two τ -simulation relations taking into account the timing constraints of the systems: a timed τ -simulation which preserves all safety properties, and a so-called divergence-sensitive and stability-respecting (DS) timed τ -simulation with the ability of preserving all properties which can be expressed with the linear timed logic Mitl (Metric Interval Temporal Logic), strong non-zenoness and deadlock-freedom. A way to show the usefulness of these relations for incremental development and their impact in practice is to examine if they preserve composability and compositionality. Given components A and B, and some composition operator , composability is ensured if A simulates A B. The direct consequence is that local properties of A are automatically preserved during its integration (the kind of properties preserved depends on the notion of simulation considered). Given components A, B, C and D, compositionality means that if A simulates B and C simulates D then A C simulates B D. We study these properties of the simulations w.r.t. the classic composition operator for timed systems, which uses a composition paradigm a la CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF]. We show that the timed τsimulation is well-adapted to incremental development achieved with this operator, since composability and compositionality are guaranteed for free. However, this is not the case for the DS timed τ -simulation. Thus, to guarantee the preservation when using this operator, the DS timed τ -simulation has to be checked algorithmically. We implemented this verification in a tool named Vesta (Verification of Simulation for Timed Automata). With this tool, we performed experiments to ensure that an algorithmic verification of the simulation (and thus of the preservation) does not advances to incremental development comparing to a direct verification of the properties. The results obtained are encouraging since they show that, even when the DS timed τ -simulation is checked to ensure preservation, incremental development can speed up verification and that models that are too large to be verified in a whole can be checked this way.

The structure of the paper is the following. First, in section 2, we recall some background on timed systems. Section 3 presents the τ -simulations we define for timed systems, and their preservation abilities. In section 4, we show the usefulness of the simulations for incremental development by studying composability and compositionality w.r.t. the classic parallel composition operator that we consider. Section 5 is dedicated to the verification in practice of the simulations, and to experiments. We present some related works in section 6. Finally, section 7 contains the conclusion and plans the future works.

Modeling timed systems and their properties

In this section, we review some basics concerning timed systems. First, we present the model we consider for timed systems, i.e., timed automata, and timed composition operators. We also present the logic Mitl that we use to express properties of timed systems.

Timed Automata

Timed automata (TA) [START_REF] Alur | A theory of timed automata[END_REF] are amongst the most studied models for continuous-time systems. They are finite automata extended with real-valued variables called clocks, modeling the time elapsing. We consider as time domain the set of non-negative reals R + . Before considering TA, we recall some usual definitions about clocks. Then, we present the syntax and semantics of TA, and the symbolic representation of the state-space of a TA. Clock constraints and polyhedra. The set C df (X) of diagonal-free clock constraints over X is defined by the following grammar:

Clock valuations

g ::= x ∼ c | g ∧ g | true where x ∈ X, c ∈ N, and ∼ ∈ {<, ≤, =, ≥, >}.
Diagonal-free constraints do not allow comparisons between clocks, of the form

x -y ∼ c. A valuation v over X satisfies a constraint x ∼ c, written v ∈ x ∼ c, if v(x) ∼ c.
The satisfaction of other constraints is defined as usual. Note that a clock constraint over X defines a convex X-polyhedron. Let zero denote the Xpolyhedron defined by x∈X x = 0. Operations on polyhedra. The dimension-restricting projection and reset operations defined on valuations can be directly extended to polyhedra. The backward diagonal projection of the X-polyhedron ζ defines an 3) on a finite set of polyhedra and the infinite semantic graph (see Def. 2) of a timed automaton to be bisimilar.

X-polyhedron ζ such that v ∈ ζ if ∃δ ∈ R + • v + δ ∈ ζ. Similarly, the forward diagonal projection of ζ defines an X-polyhedron ζ such that v ∈ ζ if ∃δ ∈ R + • v -δ ∈ ζ. Given c ∈ N,

Definition 1 (Timed Automaton) Let Props be a set of atomic propositions. A timed automaton is a tuple

A = Q, q 0 , Σ, X, T, Invar, L where: • Q is a finite set of locations. • q 0 ∈ Q is the initial location of the automaton. • Σ is a finite alphabet.
• X is a finite set of clocks.

• T ⊆ Q × C df (X) × Σ × 2 X × Q is a finite set of edges.
• Invar : Q → C df (X) is a function associating a time-progress condition (called invariant) to each location.

• L : Q → 2 Props is the labelling function mapping a set of atomic propositions to each location.

approach, {x}

x > 2,

x ≤ 5 An edge is written as a tuple e = (q, g, a, r, q ) where q and q are the source and target locations, g is a clock constraint defining the guard of the edge, a is the label of the edge and r is the set of clocks to be reset by the edge. In the sequel, we use the notations label(e) and reset(e) to denote respectively a and r.

x ≤ 5 exit enter f ar near in exit, {z} z ≤ 1 approach, {z} z ≤ 1 c0 c1 c2 c3 raise z = 1, lower

T rain Controller

Example 1 As a running example, we use the wellknown railroad crossing taken from [START_REF] Alur | Techniques for Automatic Verification of Real-Time Systems[END_REF]. It is made up of at least three elements: one or several trains, a gate and the controller of the gate. Each element is subject to strong timing constraints. The expected global behaviour of this system is the following. When a train arrives near the crossing, it sends a signal to the controller to inform of its approach. One time unit (t.u.) later, the controller commands the closing of the gate which must be down within the following t.u. The train enters the crossing, and its passage lasts at most three t.u. When it exits the crossing, it sends a signal to the controller which commands the opening of the gate during the following t.u. The gate must respond and be up within the next t.u. Fig. 1 shows the timed automata modeling each component of this system. Each location is designated by a name (the label associated by the function L) and a clock constraint representing its invariant. For more readability, guards and invariants equal to true are omitted, as well as empty resets on edges.

Definition 2 (Semantic Graph)

The semantics of a TA A = Q, q 0 , Σ, X, T, Invar, L is an infinite graph where states are pairs (q, v), q ∈ Q and v is a clock valuation over X such that v ∈ Invar(q). Its initial state is the pair (q 0 , 0). For a state s = (q, v), we call disc(s) the discrete part q of s. The transitions of this graph can be either discrete transitions or time transitions:

• Discrete transitions: given an edge e = (q, g, a, r, q ) of A, (q, v)

g,a,r → (q , v ) is a discrete transition in the semantics of A if v ∈ g. The valuation v ∈ Invar(q ) is obtained by resetting in v all clocks in r. We call (q , v ) a discrete successor of (q, v). We also directly write (q, v) e → (q , v ) such a transition, or simply (q, v) a → (q , v ) when the other elements are irrelevant.

• Time transitions have the form (q, v) t → (q, v + t) where t ∈ R + and v + t ∈ Invar(q). We say that (q, v + t) is a time successor of (q, v). Given a state s = (q, v), we also use the notation s + t for the pair (q, v + t).

In the sequel, we directly say states and transitions of the TA A, instead of states and transitions of the semantic graph of A.

Runs.

A run of a TA A is a path of its semantic graph. Thus, a run is a finite or infinite sequence ρ = (q 0 , v 0

) t0 → (q 0 , v 1 ) e0 → (q 1 , v 2 ) t1 → (q 1 , v 3 ) t2 → (q 1 , v 4 ) e1 → (q 2 , v 5 ) • • • .
Note that we do not concatenate successive time transitions in a run. In the rest of the paper, we note (ρ, k) the k th state of ρ and Γ(A) represents the set of runs of A. With the definition of runs, we can now define what a reachable state is. A state (q i , v i ) of A is said reachable if there exists some run of A visiting it, i.e. ∃ρ • (ρ ∈ Γ(A)

∧ ρ = (q 0 , v 0 ) t0 → (q 0 , v 1 ) e0 → (q 1 , v 2 ) t1 → • • • (q i , v i ) • • • ).

Non-zenoness.

A run is called non-zeno if time can diverge along the run. We write time(ρ, k) to denote the time elapsed from the initial state of the run ρ until its k th state, time(ρ, s) for the time elapsed from the initial state of ρ until the state s and time(ρ) for the total time elapsed in the run. Given a run ρ, if time(ρ) = ∞, then ρ is non-zeno [START_REF] Tripakis | The analysis of timed systems in practice[END_REF]. A TA is said strongly non-zeno if all its runs are non-zeno. A weakest notion of non-zenoness can also be considered, expressing that there exists no reachable state which is zeno, i.e., such that all runs leaving from it are zeno.

Remark 1 (Timed state sequences) The executions of a TA can also be expressed in terms of timed state sequences (TSS) instead of runs. A TSS is a sequence σ = (q 0 , I 0 ) e0 → (q 1 , I 1 ) e1 → • • • alternating pairs and discrete transitions. The q i and e i are respectively locations and edges of the TA, while the I i are closed intervals representing the time elapsing before some discrete transition is taken. We say that a run ρ = (q 1 , v 1 )

t1 → (q 1 , v 1 ) e1 → (q 2 , v 2 ) t2 → (q 2 , v 2 ) t 2 → (q 2 , v 2 ) e2 → • • • is inscribed in a TSS σ = (q 1 , I 1 ) e1 → (q 2 , I 2 ) e2 → • • • if ∀i = 1, 2, ..., time(ρ, (q i , )) ∈ I i .
Note that a run is inscribed in a unique TSS, and that there exists an infinite number of runs inscribed in a single TSS, since successive time transitions are not concatenated. We use the notation σ(ρ) for the TSS in which is inscribed the run ρ and (σ, i) the i th pair of the TSS σ. Given t ∈ I i , we write σ t the suffix of a TSS σ at time t, where σ t = (q i , I

i -t) ei → (q i+1 , I i+1 -t) ei+1 → (q i+2 , I i+2 -t) • • • .
Symbolic representation. The semantic graph of a TA has an infinite number of states. To get a finite representation of this graph, the symbolic representation currently used is based upon the notion of zones, and leads to a symbolic graph called simulation graph.

Zones. A zone is a symbolic state which groups together states of a TA A such that they have the same discrete part, and the set of their valuations forms a convex polyhedron. Thus, a zone z is a pair (q, ζ) where q is a location of A and ζ is a convex polyhedron. We note disc(z) the discrete part q of the zone z, and poly(z) its polyhedron. Operations on zones. The operations time-succ(z) and time-pred(z) define respectively the set of time successors and predecessors of some state in z. The operations disc-succ(e, z) and disc-pred(e, z) represent respectively the set of discrete sucessors and predecessors of some state in z by taking a discrete transition stemming from an edge e.

time-succ(z)

def = {s | ∃s ∈ z, t ∈ R + s t → s } time-pred(z) def = {s | ∃s ∈ z, t ∈ R + • s t → s } disc-succ(e, z) def = {s | ∃s ∈ z • s e → s } disc-pred(e, z) def = {s | ∃s ∈ z • s e → s }
Let us now define the successor and predecessor operations for zones. The operation post(e, z, c) defines the successor zone of z by the transition e (w.r.t. a constant c), i.e., the set of states which can be reached from some states in z by taking transition e and letting time elapse. Note that the operator Approx c is also used in the definition of post, to ensure the termination of the construction of the simulation graph described below and which is based on this notion of zone. For more readability, in the definition of post, Approx c is applied on a zone instead of the polyhedron of the zone. The operation pre(e, z) defines the predecessor zone of z by the discrete transition e, i.e., the set of states from which a state in z can be reached, by taking e and letting some time pass. Formally:

post(e, z, c)

def = Approx c (time-succ( disc-succ(e, z)))
pre(e, z) def = disc-pred(e,time-pred(z))

Definition 3 (Simulation graph) Let A = Q, q 0 , Σ, X, T, Invar, L be a timed automaton and c ∈ N a constant greater or equal to the greatest constant appearing in a constraint of A. The simulation graph of A w.r.t. c, written SG(A, c), is a tuple Z, z 0 , Σ, T where:

(far) 2 < x x ≤ 5 (near) (far) (in) 2 < x ≤ 5 approach, enter x > 2, {x} {x} exit approach, z ≤ 1 z ≤ 1 1 ≤ z (c2) (c0) ( c1) exit, approach, raise lower z = 1, {z} {z} (c3)
T rain Controller • Z is the finite set of states of the graph, which is a set of zones,

1 ≤ y y < 1 (is up) down y ≤ 2 (is down) (is up) ( coming
• z 0 = (q 0 , zero ∩ Invar(q 0 )) is the initial zone,

• T ⊆ Z × T × Z is
π = z 0 e0 → z 1 e1 → z 2 • • • .
The set of paths of a simulation graph SG is written Π(SG). A path is nonzeno if, for each clock x ∈ X, either x is reset infinitely often in the path, or x remains unbounded from one zone in the path. A formal definition can be found in [START_REF] Tripakis | The analysis of timed systems in practice[END_REF].

Relation between runs and paths. Each run (respectively non-zeno run) of A is inscribed in a unique path (resp. non-zeno path) of SG(A, c), and for each path π of SG(A, c) (resp. non-zeno path), there exists a run (resp. non-zeno run) inscribed in π [START_REF] Tripakis | The analysis of timed systems in practice[END_REF]).

The classic composition operator for timed automata

We consider timed systems modeled in a compositional way. Each component is modeled as a TA. To put timed components together, parallel composition operators which can handle timing informations have been defined. We focus on a particular kind of timed composition. We call it classic parallel composition since it is the classic composition used in the timed case.

This composition, written , operates between TA with disjoint sets of clocks. Intuitively, it is defined as a synchronized product where synchronizations are done on actions with identical label, while other actions interleave and time elapses synchronously between all the components.

Formally, let us consider two TA

A i = Q i , q 0i , Σ i , X i , T i , Invar i , L i for i = 1, 2, such that X 1 ∩ X 2 = ∅. The parallel composition of A 1 and A 2 , written A 1 A 2 , creates a new TA whose set of clocks is X 1 ∪ X 2 and whose labels are in Σ 1 ∪ Σ 2 .
The set Q of locations consists of pairs (q 1 , q 2 ) where q 1 ∈ Q 1 and q 2 ∈ Q 2 . The initial location is the pair (q 01 , q 02 ). The invariant of a location (q 1 , q 2 ) is Invar(q 1 ) ∧ Invar(q 2 ), and its label is L(q 1 ) ∪ L(q 2 ). The set T of edges is defined by the following rules:

• Interleaving:

(q1,q2)∈Q , (q1,g1,a,r1,q 1 ) ∈ T1 , a ∈Σ2 ((q1,q2),g1,a,r1,(q 1 ,q2)) ∈ T (q1,q2)∈Q , (q2,g2,a,r2,q 2 ) ∈ T2 , a ∈Σ1
((q1,q2),g2,a,r2,(q1,q 2 )) ∈ T

• Synchronization:

(q1,q2)∈Q, (q1,g1,a,r1,q 1 ) ∈ T1 , (q2,g2,a,r2,q 2 ) ∈ T2 ((q1,q2),g1∧g2,a,r1∪r2,(q 1 ,q 2 )) ∈ T

.

Example 3 Let us go back to the railroad crossing example. This system is modeled by at least three components : one or several train, a gate and its controller. The parallel composition of the three timed automata representing respectively the train, the gate and the controller (as they are presented in Fig. 1) leads to the timed automaton given in Fig. 3.

Metric Interval Temporal Logic

Mitl (Metric Interval Temporal Logic) [START_REF] Alur | The benefits of relaxing punctuality[END_REF]) is a logical formalism allowing to express linear timed properties. It can be viewed as an extension of the linear (untimed) logic Ltl (Linear Temporal Logic) [START_REF] Pnueli | The temporal semantics of concurrent programs[END_REF], where each temporal operator is constrained by a time interval. Mitl formulas are defined inductively by the following grammar:

ϕ ::= ap | ¬ϕ | φ ∨ ψ | φ U I ψ
where ap is an atomic proposition and I is a nonsingular interval with integer bounds (a singular interval is of the form [a, a], i.e., it is closed and its left and right bounds are equal). Other classic temporal operators can also be defined: 3 I ϕ = true U I ϕ (eventually ϕ within the interval I) and I ϕ = ¬3 I ¬ϕ (always ϕ within the interval I).

Mitl formulas are interpreted over timed state sequences. The satisfaction of a Mitl formula ϕ over a timed state sequence σ, written σ |= ϕ, is defined as follows:

• σ |= true is true,

• σ |= ap iff ap ∈ L(disc((σ, 0))), • σ |= ¬ϕ iff it is not true that σ |= ϕ, • σ |= φ ∨ ψ iff σ |= φ or σ |= ψ, • σ |= φ U I ψ iff there exists t ∈ I such that σ t |= ψ, and ∀t ∈ (0, t), σ t |= φ.
We say that a Mitl formula ϕ is valid on a TA A, written A |= ϕ, iff ϕ is true over all the runs of A, i.e.:

A |= ϕ iff ∀ρ • (ρ ∈ Γ(A) ⇒ σ(ρ) |= ϕ).

Example 4

The following safety 1 property must hold on the railroad crossing example: the gate is never open when the train is on the railroad crossing, or equivalently the gate is never open between the moment when the controller commands its lowering and the moment when it receives a signal exit from the train (P 1 ). In M itl syntax, P 1 is written (c 2 ⇒ ¬is up). The liveness 2 property: the gate is closed within the two t.u. after the controller received an approach signal from the train (P 2 ) is expressed by (is up ∧ c 1 ⇒ 3 <2 is down).

Properties preservation using timed τsimulations

Consider the railroad crossing example. Both properties P 1 and P 2 concern the behaviour of two components of the system, namely the gate and the controller. Therefore, it seems interesting to verify them only on these two components, instead of performing the verification on the complete model, obtained by the integration of one or several components train to these two components. Indeed, the assembling of the gate and the controller leads to a smaller-sized system than the whole one, and thus model-checking is more applicable.

However, by performing such a verification, it must be ensured that properties established on the composition gate/controller are preserved when integrating the component(s) train. A way to ensure such a preservation is to compare the behaviour of both models, i.e., the one on which verification is run, and the one on which properties must be preserved. A way to make such a comparison is to use equivalence or preorder relations. Equivalence relations are generally not adapted to incremental development, contrary to preorders. A preorder already used in the untimed case to guarantee preservation of properties during lower, raise, {y}

z = 1, {y} x ≤ 5 ∧ x ≤ 5 ∧ y < 1 z ≤ 1 approach, {x, z} z ≤ 1 x ≤ 5 x ≤ 5 y ≤ 2 x ≤ 5 ∧ z ≤ 1 ∧ y ≤ 2 approach, {x, z} down 1 ≤ y, up 1 ≤ y, up {near, c 1 , is up} {in, c 2 , is down} { far, c 3 , is down} {far, c 0 , going up} {near, c 1 , going up} {near, c 2 , is down} {near, c 2 , coming down} {far, c 0 , is up} x > 2, enter exit, {z}
Figure 3 Parallel composition of the train, the gate and the controller a refinement process for transitions systems is τsimulation [START_REF] Bellegarde | Ready-simulation is not Ready to Express a Modular Refinement Relation[END_REF]. We extend this relation to take into account timing informations. By doing so, we obtain two τ -simulation relations: a timed τ -simulation dealing with the preservation of safety properties, and a stability-respecting and divergencesensitive timed τ -simulation to handle the preservation of all Mitl properties, in particular liveness ones 3 . (i) If A 2 can make an observable action after some amount of time, then A 1 could do the same observable action after the same amount of time.

Timed τ -simulation / safety properties

Consider two TA A 1 = Q 1 , q 01 , Σ 1 , X 1 , T 1 , Invar 1 , L 1 and A 2 = Q 2 , q 02 , Σ 1 ∪ {τ }, X 2 , T 2 , Invar 2 , L 2 such that A 2 is obtained from A 1 either
In particular, this implies that observable actions can not be taken later in A 2 than they could be in A 1 (items 1, 2 and 5 of Definition 4).

(ii) Non-observable actions stutter (item 3 of Definition 4).

These points are illustrated in Fig. 4, where s 1 and s 1 are states of the semantic graph A 1 , s 2 and s 2 are states of the semantic graph A 2 , a is a label of A 1 and t is a time delay.

We also use a so-called gluing predicate, defined at a syntactic level on the atomic propositions of A 2 and A 1 . This predicate is defined by the following grammar, where ap 1 and ap 2 are respectively atomic propositions of A 1 and A 2 :

P g ::= ap 1 | ap 2 | ¬p | p ∨ p.
This gluing predicate induces a relation between locations of A 2 and A 1 . That is, two locations q 2 ∈ Q 2 and q 1 ∈ Q 1 are in relation w.r.t. the gluing predicate P g if they respect P g , written (q 1 , q 2 ) |= g P g , where:

(q 2 , q 1 ) |= g P g iff ap2∈L2(q2) ap 2 ∧ P g ⇒ ap1∈L1(q1) ap 1 . Definition 4 (Timed τ -simulation) Let A 1 = Q 1 , q 01 , Σ 1 , X 1 , T 1 , Invar 1 , L 1 and A 2 = Q 2 , q 02 , Σ 1 ∪ {τ }, X 2 , T 2 , Invar 2 , L 2 be two timed automata s.t. X 1 ⊆ X 2 .
We call S 1 and S 2 the respective set of states of the semantic graphs A 1 and A 2 , and P g the gluing predicate provided between A 2 and A 1 . The timed τ -simulation S is the greatest binary relation included in S 2 × S 1 . We say that (q 2 , v 2 )S(q 1 , v 1 ) if the following conditions hold:

1. Strict simulation: (q 2 , v 2 ) e2 → (q 2 , v 2 ) ∧ label(e 2 ) ∈ Σ 1 ⇒ ∃(q 1 , v 1 ) • ((q 1 , v 1 ) e1 → (q 1 , v 1 ) ∧ label(e 1 ) = label(e 2 ) ∧ (q 2 , v 2 ) S (q 1 , v 1 )). a a τ s 2 s 2 s 2 s 2 s 2 s 2 s 1 s 1 s 1 s 1 s 1 S S S S S S (a ∈ Σ 1 ) t t Figure 4 Illustration of timed τ -simulation 2. Delay equality 4 : (q 2 , v 2 ) t → (q 2 , v 2 + t) ⇒ ∃(q 1 , v 1 + t) • ((q 1 , v 1 ) t → (q 1 , v 1 + t) ∧ (q 2 , v 2 + t) S (q 1 , v 1 + t)).

τ -transitions stuttering:

(

q 2 , v 2 ) e2 → (q 2 , v 2 ) ∧ label(e 2 ) = τ ⇒ (q 2 , v 2 ) S (q 1 , v 1 ).

Location labelling respect:

(q 2 , q 1 ) |= g P g .

Common clock valuation equality:

v 2 X1 = v 1 .
We extend this notion of simulation to timed automata. Given two TA A 1 and A 2 , and their respective initial state s 01 and s 02 , we say that A 1 simulates A 2 w.r.t. S, written A 2 S A 1 if s 02 Ss 01 .

Remark 2 In Definition 4, we consider the greatest relation included in S 2 × S 1 and satisfying the clauses 1 to 5. Note that such a relation exists. Indeed, let us consider two relations R 1 and R 2 , both included in S 2 × S 1 , satisfying the previous conditions. Trivially, the union of these two relations satisfy these conditions as well. Consider S as the union of all such relations included in S 2 × S 1 and satisfying the conditions. Thus, S contains them all. Therefore, it is the greatest relation included in S 2 × S 1 satisfying the conditions.

Remark 3

The following conditions are necessary syntactic conditions on A 2 and A 1 for the verification of the timed τ -simulation to succeed. First, consider an observable action a modeled by an edge e 2 = (q 2 , g 2 , a, r 2 , q 2 ) in A 2 , and by the edge e 1 = (q 1 , g 1 , a, r 1 , q 1 ) in A 1 . The edge e 2 must reset the same clocks in X 1 than e 1 , i.e., r 2 ∩ X 1 = r 1 . Secondly, non observable actions in A 2 must only reset clocks which do not exist in A 1 . Moreover, their guard must only involve such clocks. Formally, given a non-observable action in A 2 modeled by an edge e = (q, g, τ, r, q ), we impose that r ∩ X 1 = ∅ and that g ∈ C df (X 2 ).

It is well-known that such a simulation relation only preserves safety properties. To deal with the preservation of all Mitl, in particular liveness, we restrict the relation with two additional clauses, called divergence-sensitivity and stability-respect.

Divergence-sensitive and stability-respecting timed τ -simulation / MITL properties

The relation S between two TA A 2 and A 1 guarantees that the sequences of observable actions of A 2 , with possibly τ -actions inserted, are sequences of actions which also exist in A 1 , and that each observable action in A 2 occurs at most after the same time delay than in A 1 .

Consider the liveness property P 2 , expressed by (is up ∧ c 1 ⇒ 3 <2 is down), and recall that it concerns the composition of the components gate and controller. Intuitively, for this property to be preserved when adding the component train, runs of the obtained model must not be cut between the moment when is up ∧ c 1 holds and the moment when is down is reached. However, during composition, sequences of observable actions (i.e., actions of the gate and the controller) can be cut, either by introducing a deadlock when adding the component train or by the introduction of an infinite sequence of nonobservable actions. Thus, to preserve such a property, the integration of the component train must not introduce deadlocks neither infinite sequences of nonobservable actions. These two criteria are respectively called stability-respect and divergence-sensitivity [START_REF] Glabbeck | The Linear Time -Branching Time Spectrum II ; The semantics of sequential systems with silent moves[END_REF].

Stability-respect.

To express this criterion, we use the predicate free defined in [START_REF] Tripakis | The analysis of timed systems in practice[END_REF]) (free stands for deadlock-free). Informally, given a location q, free(q) is the set of all valuations (of states with q as discrete part) from which a discrete transition can be taken after some time elapsed. In other words, it is the set of all valuations for which the location is not a deadlock. The formal definition is: free(q) = e=(q,g,a,r,q )∈T (g ∩ ([r := 0]Invar(q ))).

Divergence-sensitivity. The detection of infinite sequences of non-observable actions in a timed automaton A consists in detecting non-zeno τ -cycles in A (a cycle which only contains timed transitions and discrete transitions labelled by τ is called a τ -cycle). Formally, we say that A does not contain any non-zeno τ -cycles if:

∀ρ, k • (ρ ∈ Γ(A) ∧ time(ρ) = ∞ ∧ k ≥ 0 ⇒ ∃k , e • (k ≥ k ∧ (ρ, k ) e → (ρ, k + 1) ∧ label(e) = τ )).
These two notions are illustrated in Fig. 5, where s 1 is a state of the semantic graph A 1 , s 2 and s 2 are states of the semantic graph A 2 and a and b are common labels between A 1 and A 2 .

Definition 5 (Divergence-sensitive (DS) timed τsimulation) Consider two TA

A 1 = Q 1 , q 01 , Σ 1 , X 1 , T 1 , Invar 1 , L 1 and A 2 = Q 2 , q 02 , Σ 1 ∪ {τ }, X 2 , T 2 , Invar 2 , L 2 , such that X 1 ⊆ X 2
. S 1 and S 2 are the respective set of states of A 1 and A 2 . The relation S ds is included in S 2 × S 1 . We say that (q 2 , v 2 )S ds (q 1 , v 1 ) if (q 2 , v 2 )S(q 1 , v 1 ) and

• Stability-respect: v 2 ∈ free(q 2 ) ⇒ v 1 ∈ free(q 1 ),

• Divergence-sensitivity: A 2 does not contain any non-zeno τ -cycles.

Let A 1 and A 2 be two TA, with respective initial state s 01 and s 02 . We say that A 2 simulates A 1 w.r.t. S ds , written A 2 S ds A 1 , if s 02 S ds s 01 .

Preservation of properties

We defined the relation S ds to preserve a larger spectrum of properties. We prove in this section that the relation preserves all Mitl properties, as well as strong non-zenoness and deadlock-freedom.

MITL.

Consider two TA A 1 and A 2 such that A 2 S ds A 1 . We prove that, for each run in A 2 , if the run of A 1 which simulates it satisfies a Mitl property ϕ, then this run of A 2 also satisfies ϕ. Before proving this, recall that the satisfaction of a Mitl formula is not defined on runs, but on timed state sequences. Thus, the following result is necessary to prove the preservation.

Lemma 1 Consider two runs ρ 1 and ρ 2 , such that ρ 2 S ds ρ 1 . Let σ 1 and σ 2 be the timed state sequences in which are respectively inscribed ρ 1 and ρ 2 . Consider t ∈ R + , and the suffixes σ t 1 and σ t 2 of σ 1 and σ 2 at time t. We have:

∀ρ 2 inscribed in σ t 2 , ∃ρ 1 inscribed in σ t 1 such that ρ 2 S ds ρ 1 .
Proof. Let us consider ρ 2 as the suffix of ρ 2 at time t. We distinguish two cases:

1. There exists a state (q 2 , v 2 ) in ρ 2 s.t.

time(ρ 2 , (q 2 , v 2 )) = t. As ρ 2 S ds ρ 1 , there exists (q 1 , v 1 ) in ρ 1 s.t. (q 2 , v 2 )S ds (q 1 , v 1 ). By clause 2 of Def. 4, we can deduce that time(ρ 1 , (q 1 , v 1 )) = t.

Let ρ 1 be the suffix of ρ 1 from the state (q 1 , v 1 ).

We have ρ 2 S ds ρ 1 .

2. If such a state (q 2 , v 2 ) does not exist in ρ 2 , it means that this time value occurs during a time transition. Then, it is enough to split the time transition and create an intermediary state (q 2 , v 2 ) s.t. time(ρ 2 , (q 2 , v 2 )) = t. Then, if we also split the corresponding time transition in ρ 1 (this transition exists since ρ 2 S ds ρ 1 ), the previous case applies.

The lemma is true for the particular case of the suffix ρ t 2 of run ρ 2 at time t built from σ t 2 . Without loss of generality, we can affirm that the lemma is also true for each run inscribed in σ t 2 (as each run can be written as ρ t 2 by splitting or concatenating time transitions). 2

Recall that the locations of A 2 are not labelled over the same set of propositions (called P rops 2 ) than the locations of A 1 (called P rops 1 ). A gluing predicate is defined between A 2 and A 1 to establish a correspondence between propositions of A 2 and propositions of A 1 . As Mitl properties of A 1 are expressed over P rops 1 , they will be satisfied (by preservation) on A 2 modulo the gluing predicate P g . The satisfaction by preservation of a Mitl formula ϕ over P rops 1 , written σ |= p ϕ, is defined as follows (where σ is a TSS of A 2 , and ap, ϕ, ψ and φ are Mitl formulas over P rops 1 ):

• σ |= p true is true, • σ |= p ap iff ap2∈L2(disc((σ,0))) ap 2 ∧ P g ⇒ ap, • σ |= p ¬ϕ iff it is not true that σ |= p ϕ, • σ |= p φ ∨ ψ iff σ |= p φ or σ |= p ψ, • σ |= p φ U I ψ iff there exists t ∈ I such that σ t |= p ψ, and ∀t ∈]0, t[, σ t |= p φ.
By extension, a TA A satisfies a Mitl property ϕ by preservation if all its runs satisfies ϕ by preservation:

∀ρ • (ρ ∈ Γ(A) ⇒ σ(ρ) |= p ϕ).

Lemma 2 (Preservation of MITL properties on a run)

Let A 1 and A 2 be two TA such that A 2 S ds A 1 , ρ 1 a run of A 1 and ρ 2 a run of A 2 . Consider a Mitl property ϕ. We have:

ρ 2 S ds ρ 1 ∧ σ(ρ 1 ) |= ϕ ⇒ σ(ρ 2 ) |= p ϕ.
Proof. We prove, by induction on the structure of the formula, that S ds preserves Mitl properties. In the following, for more readability, we write σ 1 for σ(ρ 1 ) and σ 2 for σ(ρ 2 ). The basis, i.e., when the formula is an atomic proposition, comes directly from the fact that the relation respects the gluing predicate.

2 S ds A 1 then A 2 |= p ϕ. Proof. The proof is immediate. Since A 2 S ds A 1 , then ∀ρ 2 • (ρ 2 ∈ Γ(A 2 ) ⇒ ∃ρ 1 • (ρ 1 ∈ Γ(A 1 ) ∧ ρ 2 S ds ρ 1 )).
Since A 1 |= ϕ, then all its runs also satisfy this property, i.e., ∀ρ 1 • (ρ 1 ∈ Γ(A 1 ) ⇒ σ(ρ 1 ) |= ϕ). By lemma 2, ϕ also holds by preservation, for all runs of A 2 , and thus A 2 |= p ϕ. 2

Strong non-zenoness.

We prove that S ds preserves strong non-zenoness.

Proposition 1 Consider two TA A 1 and A 2 . If A 1 is strongly non-zeno and A 2 S ds A 1 , then A 2 is strongly non-zeno.

Proof. (sketch, by contradiction).

We prove intuitively this proposition. Consider that A 1 is strongly nonzeno, and that A 2 is not. Thus, A 2 contains a run ρ 2 which is zeno. As A 2 S ds A 1 , then each infinite run of A 2 is simulated by an infinite run of A 1 . Let ρ 1 be the run which simulates ρ 2 . The clause delays equality ensures that if the total time elapsed in ρ 2 converges, then the total time elapsed in ρ 1 also converges. This is contradictory with the assumption that A 1 is strongly non-zeno, and thus that it does not contain any executions in which the total time elapsed converges. Recall that the run ρ 2 contains the same sequence of observable actions than ρ 1 , with also non-observable actions which can be inserted between observable actions. As the time delay between two observable actions must remain the same than in A 1 , if an infinite number of non-observable actions is inserted in this finite delay, then the run becomes zeno. But, this case is excluded by the clause divergence-sensitivity, which forbids such infinite sequences of non-observable actions. 2Remark 4 (Non-zenoness preservation) The weaker notion of non-zenoness is not preserved by the DS timed τ -simulation. Recall that non-zenoness is the fact that there is not reachable state which is zeno. In other words, non-zenoness expresses that there is no reachable state such that all runs leaving from it are zeno. Therefore, contrary to strong non-zenoness which imposes that all runs are non-zeno, non-zenoness only requires that there exists at least one run from each reachable state. In terms of runs, the simulations we defined express that each run in A 2 is simulated by a run in A 1 . It is thus possible that some runs in A 1 do not simulate any runs in A 2 . These runs somehow do not exist in A 2 . Consider now a state s 1 in A 1 from which only one run is non-zeno, and a state s 2 in relation with s 1 . It can be the case that the non-zeno run from s 1 does not exist any more from s 2 , and thus that only zeno runs leave from s 2 . Non-zenoness is thus immediatly not preserved.

Deadlock-freedom.

Deadlock-freedom is preserved by the DS timed τsimulation, as a direct consequence of the definition of the relation (with the clause stability-respect ).

Proposition 2 Let A 1 and A 2 be TA. If A 1 is deadlockfree and A 2 S ds A 1 , then A 2 is deadlock-free.

Exploiting simulations for incremental development

In the previous section, we defined two relations: a timed τ -simulation which preserves safety properties, and a divergence-sensitive and stability-respecting timed τsimulation, which preserves all Mitl properties, strong non-zenoness and deadlock-freedom. To exploit these relations, and thus their preservation abilities, during an incremental development of a component-based timed system, it is necessary to study the three following properties:

• compatibility of the relations w.r.t. composition operators,

• composability, which means that a component simulates its integration with other components,

• and compositionality. This last property expresses that, given components A, B, C and D, if B simulates A and D simulates C, then the composition of B and D simulates the composition of A and C.

Composability is essential for integration of components since it guarantees automatically the preservation of properties during the integration (the kind of properties preserved depends on the notion of simulation considered). Compositionality is essential for refinement in order to verify it in a compositional way.

We study these properties in the case of the classic parallel composition. In the sequel, we use the following notations. Given a timed automaton A, we note S A its set of states and Σ A its alphabet. A state of A is simply written s A or s A , which respectively represents the pairs (q A , v A ) or (q A , v A ). The initial state of A is written s 0A .

Proposition 3 (Composability)

Let A and B be TA. We have: A B S A.

Proof. By construction of A B, its initial state is the pair (s 0A , s 0B ). To prove that A B S A, it is enough to prove that (s 0A , s 0B )Ss 0A . By definition, S is the greatest relation included in S A B × S A which satisfies clauses 1 to 3 of Definition 4. Thus, each relation The timed τ -simulation is well-adapted to incremental development with the classic parallel composition operator, since composability, compatibility and compositionality hold for free. This is not the case for the DS timed τ -simulation when using such a composition paradigm. Indeed, the fact that this kind of composition generally introduces deadlocks does not allow to benefit of the three properties. For composability for instance, this introduction of deadlocks is incompatible with the stability-respect clause of the DS timed τ -simulation. However, it remains possible to benefit of its assets in terms of preservation, but at the cost of an algorithmic verification of the relation.

R ⊆ S A B × S A which satisfies these clauses is included in S . Consider a relation R ⊆ S A B × S A such that ∀(s A , s B ) ∈ S A B , (s A , s B )R s A if s A = s A . Consider ((s A , s B ), s A ) ∈ R. 1. Strict simulation: let (s A , s B ) a → (s A , s B ) in A B such that a ∈ Σ A . By construction of A B, a transition s A a → s A exists in A. By definition of R, (s A , s B )R s A and

Simulations in practice

In the previous sections, we defined the simulations at a semantic level, on the states of TA. To check algorithmically the DS timed τ -simulation, we extend it on the symbolic representation of TA, i.e., on zones.

Symbolic timed τ -simulations

We focus directly on the symbolic version of the DS timed τ -simulation. The definition for the timed τ -simulation can be obtained by not considering divergence-sensitivity and stability-respect. Most of the clauses of this symbolic definition can be obtained straightforward from the semantic definition. The main changes concern the clauses delays equality, common clocks valuations equality and strict simulation. Consider two simulation graphs SG 1 and SG 2 , z 1 a zone of SG 1 and z 2 a zone of SG 2 . In simulation graphs, time elapsing does not appear explicitly as transitions. Intuitively, time elapses inside zones. Thus, delays equality and common clocks valuations equality are checked by verifying that the polyhedron of the zone z 2 (projected on the set of clocks of SG 1 ) is included in the polyhedron of z 1 . Let us now study strict simulation. The definition we give at the symbolic level is based on the post-stability property of the simulation graph. This property ensures that, given a transition z e → z , all the successors of (semantic) states in z and taking e are in z . A part of this clause is directly extended from the semantic one, by imposing that if the transition z 2 e2 → z 2 exists, then a transition z 1 e1 → z 1 exists with the same label. But, as the simulation graph does not have the prestability property (i.e., a symbolic transition z e → z does not imply that all the (semantic) states in z can take the transition e), another condition is needed. Each (semantic) state in z 2 taking this transition e 2 must correspond to a state in z 1 taking transition e 1 . This clause is illustrated by Fig. 6. To express this condition, we define a predicate named src val, defined as follows: src val(z, e, z ) = poly(pre(e, z ) ∩ z).

Definition 6 (Symbolic DS timed τ -simulation)

Let SG 1 = Z 1 , z 01 , Σ 1 , T 1 and SG 2 = Z 2 , z 02 , Σ 2 ,
T 2 be two simulation graphs, obtained respectively from two TA A 1 and A 2 . Let X 1 be the set of clocks of A 1 . The symbolic DS timed τ -simulation Z ds is the greatest binary relation included in Z 2 × Z 1 , such that z 2 Z ds z 1 if the following conditions hold:

1. Strict simulation: z 2 e2 → z 2 ∧ label(e 2 ) ∈ Σ 1 ⇒ ∃z 1 • (z 1 e1 → z 1 ∧ label(e 1 ) = label(e 2 ) ∧ src val(z 2 , e 2 , z 2 ) X1 ⊆ src val(z 1 , e 1 , z 1 ) ∧ z 2 Z ds z 1 ).

Delay equality and common clock valuation equality:

poly(z 2 ) X1 ⊆ poly(z 1 ).

τ -transition stuttering:

z 2 e2 → z 2 ∧ label(e 2 ) = τ ⇒ z 2 Z ds z 1 .

Location labelling respect:

(disc(z 2 ), disc(z 1 )) |= g P g .

Stability-respect:

(poly(z 2 )\free(disc(z 2 )) X1 ⊆ poly(z 1 )\free(disc(z 1 )).

Divergence-sensitivity:

SG 2 does not contain any non-zeno τ -cycles 5 .

We extend this relation to simulation graphs. Consider two simulation graphs SG 1 and SG 2 . Their initial zones are respectively z 01 and z 02 . We say that

SG 1 simulates SG 2 w.r.t. Z ds , written SG 2 Z ds SG 1 , if z 02 Z ds z 01 .
We now prove that this symbolic relation Z ds implies the semantic relation S ds . This implication allows to benefit of the preservation abilities of S ds at the symbolic level. The proof is decomposed into two parts. First, we express Lemma 3, which is necessary for the divergence-sensitivity clause, then we prove the implication of the relations in Lemma 4.

Lemma 3 Let A be a TA and c be the greatest constant appearing in a constraint of A. Let SG(A, c) be the simulation graph associated to A. If A does not contain any non-zeno τ -cycles, then SG(A, c) does not contain any non-zeno τ -cycles, and conversely.

Proof. Immediate by the fact that each non-zeno run of A is inscribed in a unique non-zeno path of SG(A, c), and that for each non-zeno path of SG(A, c), there exists a non-zeno run inscribed in this path. 2 Lemma 4 Let SG 1 and SG 2 be two simulation graphs. Let (q 1 , ζ 1 ) and (q 2 , ζ 2 ) be two respective zones of SG 1 and SG 2 , such that (q 2 , ζ 2 )Z ds (q 1 , ζ 1 ). We have the following. For each state (q 2 , v 2 ) ∈ (q 2 , ζ 2 ), there exists only one state (q 1 , v 1 ) ∈ (q 1 , ζ 1 ) such that (q 2 , v 2 )S ds (q 1 , v 1 ). Formally:

(q 2 , ζ 2 ) Z ds (q 1 , ζ 1 ) ⇒ ∀v 2 • (v 2 ∈ ζ 2 ⇒ ∃v 1 • (v 1 ∈ ζ 1 ∧ (q 2 , v 2 ) S ds (q 1 , v 1 ))). ( )
Proof. The proof is done by fixed-point induction.

Consider the function F : Z 2 × Z 1 → Z 2 × Z 1 defined in the following way. If Z ds ⊆ Z 2 × Z 1 , then ((q 2 , ζ 2 ), (q 1 , ζ 1 )) ∈ F(Z ds ) iff the clauses 1 to 6 of Definition 6 hold.

In the definition of Z ds , we consider the greatest fixed-point of the function F . This function is trivially monotonic (and the sets Z 2 and Z 1 are finite), thus we can reason inductively about the pre-fixed-points of this function. The principle of this induction is the following: given a predicate P , this induction allows to prove P (Z ds ), by proving P (F (Z ds )), with the induction assumption that P (Z ds ) holds. We proceed clause by clause. Details are given in Appendix B. 2 Theorem 2 Let A 1 and A 2 be two TA, and SG 1 and SG 2 the simulation graphs respectively obtained from A 1 and A Figure 6 Clause strict simulation at the symbolic level

2 . If SG 2 Z ds SG 1 then A 2 S ds A 1 . Proof. Since SG 2 Z ds SG 1 ,

The tool VeSTA

We implemented the verification of the DS timed τsimulation Z ds in a tool named Vesta 6 (Verification of Simulations for Timed Automata) [START_REF] Bellegarde | The Tool VeSTA: Verification of Simulations for Timed Automata[END_REF]. Vesta considers component-based timed systems developed incrementally using timed automata and the classic parallel composition operator. The tool focuses on the verification of the simulation during incremental development achieved by integration of components using the classic composition . Thus, it allows to ensure that local properties of a component (or a group of components) are preserved when it is merged with other components. Consider two TA A 1 and A 2 . To check if A 1 A 2 Z ds A 1 , two main algorithms are implemented in the tool. The first algorithm performs a joint on-the-fly depthfirst search of the simulation graphs of A 1 and A 2 and checks the stability-respecting timed τ -simulation (i.e., clauses 1 to 5 of Z ds ). If the verification of this part of the simulation does not succeed, the tool reports a diagnostic. This diagnostic consists in a symbolic trace in A 2 with a zone which does not satisfy the relation, and the corresponding symbolic trace in A 1 . The divergence-sensitivity part consists in the detection of non-zeno τ -cycles in A 2 . Thus, we reuse the module Profounder [START_REF] Tripakis | Checking Timed Büchi Automata Emptiness Efficiently[END_REF], which is part of the Open-Kronostool [START_REF] Tripakis | The analysis of timed systems in practice[END_REF] to achieve this search. Profounder was initially designed to check if a state is reachable in a TA, or to check timed Büchi automata emptiness. This second possibility consists in detecting non-zeno cycles in a TA. We adapted it to search only non-zeno τ -cycles.

A case study: the production cell

We present in this section 7 a case study on which we performed experiments to show the suitability of timed τ -simulations for incremental development, even when an algorithmic verification of the simulation is needed. The verification of the properties was achieved with the tool Kronos [START_REF] Yovine | Kronos: A verification tool for real-time systems[END_REF]. Kronos is a verification tool for timed systems which performs Tctl model-checking [START_REF] Alur | Model-Checking in Dense Real-time[END_REF], in particular for component-based timed models (indeed, Kronos can compute the parallel composition of TA). Tctl is a logical formalism that allows to express branching-time properties. It can be seen as the timed extension of the untimed logic Ctl [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF][START_REF] Emerson | Decision procedures and expressiveness in the temporal logic of branching time[END_REF]. To our knowledge, there is no tool performing Mitl modelchecking. Thus, we focused on linear-time properties that can also be expressed in Tctl to perform the verification with Kronos. The verification of the simulations was achieved with Vesta.

The production cell case study was developed by FZI (the Research Center for Information Technologies, in Karlsruhe) as part of the Korso project. The goal was to study the impact of the use of formal methods when treating industrial applications. Thus, this case study was treated in about thirty different formalisms. We treat it with timed automata, as it was in [START_REF] Burns | How to verify a safe real-time system: The application of model-checking and timed automata to the production cell case study[END_REF].

Modeling.

The cell is made up of six devices, where pieces are treated: a feed-belt, equipped with a sensor, where pieces arrive, a deposit-belt from which pieces are evacuated, an elevating-rotary table, a two-arms robot and a press. The sensor detects when a piece is introduced in the system, and sends a signal to the robot to inform it of this arrival. When the piece is at the end of the feed-belt, it is transferred to the table which goes up and turns until being in a position from which the arm A of the robot can take the piece. The robot turns 90 • so that the arm A can put down the piece on the press, where it is processed and then transported by the arm B to the deposit belt. The cell is presented in Fig. 7. It is modeled by at least seven components: one for each device, and one or several pieces. The cell is subject to timing constraints, which are shown in Fig. 8. Each component is modeled as a TA. These TA can be found in [START_REF] Burns | How to verify a safe real-time system: The application of model-checking and timed automata to the production cell case study[END_REF]). The complete model is obtained by making the classic parallel composition of all these components. Fig. 9 shows the size of the simulation graphs for each component.

Verification.

To ensure that the modeling is correct, there are several properties to check. Recall that we focus on the local properties of the components (or group of components).

We propose to perform the verification locally, and then to ensure that the properties hold on the global model by preservation, by checking algorithmically the DS timed τ -simulation. In particular, we consider local properties concerning the robot. Here is a nonexhaustive list of dynamic properties to check on this component. Properties 1 and 2 are safety requirements, properties 3 and 4 are liveness ones and properties 5 to 7 are bounded-response ones:

(1) When the robot is in wait position, its two arms are empty,

(2) The robot is not waiting in front of the table if the arm A is full,

(3) If there is a piece on arm B, the robot will eventually go to the deposit belt, (4) If there is a piece on arm A, the robot will eventually go to the press,

(5) When the robot is in front of the deposit belt, then it goes back to the The following liveness property concerns the correct interaction between the robot and the press :

(8) If arm A is full then the press will eventually be free.

We use two approaches to verify these properties on the plant. As a first approach, we verify the properties in a classic way, directly on the global model, with one piece. As a result, we obtain that all the properties hold on this model of the plant. The second approach consists in verifying the properties locally, i.e., on the robot component for properties 1 to 7, and on the composition robot press for property 8. Here again, the verification succeeds. Next, to guarantee the preservation of these properties, first when integrating the robot with the press, then when integrating the composition robot press with the rest of the components, we use the DS timed τ -simulation. More precisely, we check that robot press Z ds robot to ensure that properties 1 to 7 are preserved on the composition robot press, and complete model Z ds robot press to check the preservation of property 8 on the complete model (as well as the preservation of properties 1 to 7 if their preservation on robot press is established). We use our tool Vesta to check it for both cases, and obtain as a result that the verification of the simulation was successful. Thus, properties are preserved. Fig. 10 gives the detailed results of the comparison of the two approaches in terms of verification times (in seconds). We can see that, even on this small example, the second approach only needs 0.57 sec. of computation time to ensure that the properties hold on the cell (0.06 sec. for local verification and 0.51 sec. for preservation), whereas the classic approach consumes 19.58 sec. Note that, in both approaches, we focused on a global system which contains only one piece. The reason is the following. First, in the case of the second approach, adding other pieces to the global system does not affect the results of the preservation. As the component piece already exists in the global system and that there are no synchronizations between the pieces, no new deadlocks can appear while adding a new piece. Indeed, the system can behave like it did with only one piece, or synchronize with the new piece. In this last case, as the environment of the pieces could synchronize with one piece without introducing deadlocks, then it will synchronize with the new pieces in the same way, thus without introducing deadlocks. On the other hand, in the first approach, adding pieces considerably increase the computation time for the verification of liveness or bounded-response properties. Indeed, even with few pieces, the memory needed to perform classic verification of such properties is too large for the verification to be run to completion.

Related works

Several works have been devoted to study behavioral equivalences, as well as their associated preorder, in the timed case. Concerning equivalences, timed bisimulation was studied in [START_REF] Cerans | Decidability of bisimulation equivalence for parallel timer processes[END_REF]. Three time-abstracting bisimulations were introduced in [START_REF] Tripakis | Analysis of Timed Systems using Time-abstracting Bisimulations[END_REF]): strong time-abstracting bisimulation, observational time-abstracting bisimulation and delay time-abstracting bisimulation. Contrary to the timed bisimulation, time-abstracting bisimulations abstract away from quantitative aspects of time elapsing. Strong time-abstracting bisimulation preserves reachability, timed Büchi automata and Ctl (Tctl is also preserved modulo a transformation of the TA and of the formula as presented in [START_REF] Tripakis | The analysis of timed systems in practice[END_REF]. Observational and delay time-abstracting bisimulations preserve reachability and timed Büchi automata. Therefore, bisimulations preserve a wide range of properties. However, they are not really adapted to incremental modeling. Preorders, to which we are interested in this paper, are more adapted and have also been widely studied. Timeabstracting simulation equivalence and preorder have been studied in [START_REF] Henzinger | Computing simulations on finite and infinite graphs[END_REF], but timed properties are not preserved by these relations. Timed simulation was defined in [START_REF] Tasiran | Verifying Abstractions of Timed Systems[END_REF]. The authors showed that the problem of checking if a TA simulates another one w.r.t. the relation they defined is solvable in Exptime. The relation has the properties of composability, compatibility and compositionality w.r.t. a totally synchronous composition operator. However, non-observable actions are not considered in the definition of this simulation. The notion of simulation which seems the closest to the one we defined in this paper is the timed ready simulation of [START_REF] Jensen | Scaling up Uppaal : Automatic verification of real-time systems using compositionnality and abstraction[END_REF]. It is defined on extended timed automata, i.e., timed automata which can contain urgent actions and shared variables. Non-observable actions are also considered. The definition of this relation is almost equivalent to the definition of our timed τ -simulation, and thus preserves safety properties. But, it has not been extended to handle the preservation of liveness properties. It has the properties of composability, compatibility and compositionality w.r.t. a composition operator which paradigm is close to the one of the classic parallel composition we considered. However, an assumption concerning the absence of internal activity (i.e., the absence of τ -transitions) in the automata is done to benefit of these properties, in particular, for the compositionality property. To our knowledge, there is no simulation preorder which has been defined in the timed case, taking into account non-observable actions, and preserving in particular liveness properties.

Conclusion and future works

The context of this paper is the verification by modelchecking of component-based timed systems, modeled by timed automata. To cope with the state-space explosion problem of model-checking, we propose to develop such systems incrementally, either by refinement or by integration of components. These methods allow to check properties on smaller-sized models, where modelchecking is still applicable. The main issue for these methods to be applicable concerns the preservation of properties, established on these smaller-sized models, on the complete model.

To guarantee the preservation, we defined τsimulation relations for timed systems, with preservation abilities: a timed τ -simulation which ensures the preservation of safety properties, and a divergencesensitive and stability-respecting one which handles the preservation of all Mitl properties, as well as strong non-zenoness and deadlock-freedom. We have shown that the timed τ -simulation is well-adapted to incremental development with the classic parallel composition operator for timed automata. Indeed, it is compatible with the operator, and composability and compositionality hold. This is not the case for the DS timed τ -simulation, due to the fact that deadlocks often appear when composition is achieved with this operator. Composability is the fact that a component simulates its integration with other ones. Its direct consequence is thus that properties are automatically preserved during integration of components. As this property does not hold in the case of the classic operator for the DS timed τ -simulation, it is essential to check that the algorithmic verification of the preservation, by means of the simulation, does not remove interest to incremental development. We implemented the verification of the DS timed τ -simulation in a tool named Vesta, in the particular case of integration of components. We made experiments to check if, even if the simulation is checked algorithmically, the cost in practice of an incremental verification by integrating components is still lower than the cost of a direct verification on the complete model. It turns out that, on a production cell example and in terms of computation times, the methodology we propose appears to be more efficient. This case study (as well as the study of the CSMA/CD protocol that we presented in (Bellegarde, Julliand, Mountassir & Oudot 2006a)) shows the interest of the method for some kind of parameterized systems, when a system S is likely to contain an undetermined number of identical components C i , i = 1..n, modulo some renaming. The number n of these components can be viewed as a parameter of the system. For instance, in the production cell example, the number of pieces which are admitted in the cell is this parameter. In the case of integration of components with the classic operator, it would be interesting to be able to check properties with a small fixed number m of components, such that preservation is ensured whatever the number n of components, with n ≥ m. For this purpose, it seems sufficient to get conditions on the C i s and/or on their synchronizations to guarantee that adding more of these components in the system does not introduce deadlocks (in addition to the condition on the absence of non-zeno cycles of internal activity in the components). Thus, an interesting work is to study such conditions. Another work direction concerns the problem of implementability of timed automata. It consists in studying if the properties which are established on a timed automaton are preserved on the implementation corresponding to it, on a given platform. The main issue comes from the fact that the semantics of timed automata is often considered as being ideal: execution times of actions are ignored, clocks are infinitely precise, etc... In practice, these perfect concepts are not true.

To check properties on the implementation, [START_REF] Altisen | Implementation of Timed Automata : an Issue of Semantics or Modeling ?[END_REF] proposes an approach based on modeling, to benefit of the existing verification tools for timed automata. They propose to model the execution platform P as timed automata, and to transform the timed automaton A modeling the system into an untimed finite automaton. The composition of all these automata, called the execution model M , represents the execution of A on the platform P . An interesting perspective would be to study the compatibility of the simulations we defined in the specific framework of the timed automaton A and its execution model M , while taking into account the way the platform is specified. This could also allow to exhibit conditions on the modeling of the platform (and thus on the real platform) which guarantee the preservation of the properties of A on its implementation on the platform.

(ii) Transitions in Σ B 8 which do not synchronize with an action of C (the part of Σ B in dark grey in Fig. 11), (iii) Transitions in C which synchronize with a transition in A. They appear in B C either as interleaving actions of C if the synchronization is done with an action of A which does not appear in B, or as an action of B synchronized with an action of C otherwise (the part in the center inside the bold line in Fig. 11).

Let us detail these three cases: Consider a transition (q 2 , v 2 ) e2 → (q 2 , v 2 ) such that label(e 2 ) ∈ Σ 1 . By construction of the simulation graph, if such a transition exists, then a transition (q 2 , ζ 2 ) e2 → (q 2 , ζ 2 ) exists in SG(A, c), such that v 2 ∈ ζ 2 and v 2 ∈ ζ 2 . Since ((q 2 , ζ 2 ), (q 1 , ζ 1 )) ∈ F (Z ds ), there exists a transition (q 1 , ζ 1 ) e1 → (q 1 , ζ 1 ) such that label(e 1 ) = label(e 2 ) which satisfies the clause strict simulation of the definition of F . In particular, we have (q 2 , ζ 2 )Z ds (q 1 , ζ 1 ). Since this transition exists, and by construction of the simulation graph, there exists at least one discrete (semantic) transition inscribed in this transition. Moreover, we prove that there exists v 1 ∈ ζ 1 such that v 2 X1 = v 1 . Since src val((q 2 , ζ 2 ), e 2 , (q 2 , ζ 2 )) X1 ⊆ src val((q 1 , ζ 1 ), e 1 , (q 1 , ζ 1 )), there exists a discrete transition (q 1 , v 1 ) e1 → (q 1 , v 1 ) such that v 1 ∈ ζ 1 . It remains to prove that (q 2 , v 2 )S ds (q 1 , v 1 ). The action which labels e 2 is an observable action of A 2 . Thus, we know that the transition resets exactly the same clocks in X 1 than e 1 , i.e., reset(e 2 ) ∩ X 1 = reset(e 1 ). Moreover, since v 2 X1 = v 1 , and that, by definition we have v 2 X1 = v 1 . Since (q 2 , ζ 2 )Z ds (q 1 , ζ 1 ), and ( ) holds for Z ds , we have (q 2 , v 2 )S ds (q 1 , v 1 ).

(i) Consider a transition (s A , s C ) g,c,r → (s A , s C ) such that c ∈ Σ C \Σ A . By construction of A C, a transition s C g,c,r → s C exists in C.
3. Delay equality: we prove that ((q 2 , ζ 2 ), (q 1 , ζ 1 )) ∈ F(Z ds ) ⇒ ∀v 2 • (v 2 ∈ ζ 2 ∧ (q 2 , v 2 ) t → (q 2 , v 2 ) ⇒ ∃v 1 , v 1 • (v 1 ∈ ζ 1 ∧ (q 1 , v 1 ) t → (q 1 , v 1 ) ∧ (q 2 , v 2 )S ds (q 1 , v 1 ))). Time transitions which appear in a semantic transition system do not appear explicitly as transitions in the associated simulation graph. Time elapses intuitively inside zones. Consider a transition (q 2 , v 2 ) t → (q 2 , v 2 ) inside the zone (q 2 , ζ 2 ) (i.e., v 2 ∈ ζ 2 and v 2 ∈ ζ 2 ). Consider also the valuation v 1 ∈ ζ 1 such that v 2 X1 = v 1 (this valuation exists by the clause Common clocks valuations equality). Since ζ 2 X1 ⊆ ζ 1 , there exists a transition (q 1 , v 1 ) t → (q 1 , v 1 ) such that v 1 ∈ ζ 1 and v 1 = v 2 X1 . With the induction assumption, we know that there exists a valuation v 1 such that (q 2 , v 2 )S ds (q 1 , v 1 ) and v 1 = v 2 X1 . Thus, v 1 = v 1 . It follows that (q 2 , v 2 )S ds (q 1 , v 1 ). 4. τ -transitions stuttering: we prove that ((q 2 , ζ 2 ), (q

1 , ζ 1 )) ∈ F(Z ds ) ⇒ ∀v 2 • (v 2 ∈ ζ 2 ∧ (q 2 , v 2 ) e2 → (q 2 , v 2 ) ∧ label(e 2 ) = τ ⇒ ∃v 1 • (v 1 ∈ ζ 1 ∧ (q 2 , v 2 )S ds (q 1 , v 1 ))).
Consider a transition (q 2 , v 2 ) e2 → (q 2 , v 2 ) such that label(e 2 ) = τ . By construction of the simulation graph, a transition (q 2 , ζ 2 ) e2 → (q 2 , ζ 2 ) exists in SG(A, c), such that v 2 ∈ ζ 2 and v 2 ∈ ζ 2 . Since ((q 2 , ζ 2 ), (q 1 , ζ 1 )) ∈ F(Z ds ), and by definition of F , we have (q 2 , ζ 2 )Z ds (q 1 , ζ 1 ). We proved previously that there exists a valuation v 1 ∈ ζ 1 such that v 1 = v 2 X1 . It remains to prove that v 2 X1 = v 1 . Since τ -transitions only reset clocks in X 2 \X 1 , only the valuations of the clocks in X 2 are changed in v 2 in comparison to v 2 . Thus, v 2 X1 = v 1 . Since (q 2 , ζ 2 )Z ds (q 1 , ζ 1 ), and ( ) holds for Z ds , we have (q 2 , v 2 )S ds (q 1 , v 1 ).

5.

Location labelling respect : immediate by the definition of F .

6. Divergence-sensitivity: immediate by lemma 3.

7. Stability-respect : we prove that if (ζ 2 \free(q 2 )) X1 ⊆ ζ 1 \free(q 1 ) then

∀v 2 • (v 2 ∈ ζ 2 ∧ v 2 ∈ free(q 2 ) ⇒ ∃v 1 • (v 1 ∈ ζ 1 ∧ v 1 ∈ free(q 1 ))).
This is equivalent to:

if ∀v • (v ∈ (ζ 2 \free(q 2 )) X1 ⇒ ∃v • (v ∈ ζ 1 \free(q 1 ) ∧ v = v))
then ∀v 2 • (v 2 ∈ free(q 2 ) ⇒ ∃v 1 • (v 1 ∈ free(q 1 ) ∧ v 2 X1 = v 1 )).

Therefore, we have immediately that ( ) holds F (Z ds ).

Notes

  the extrapolation of ζ w.r.t c, written Approx c (ζ), is the smallest polyhedron ζ ⊇ ζ defined intuitively as follows: lower bounds of ζ greater than c are replaced by c, and upper bounds greater than c are ignored. All these operations preserve the convexity of polyhedra. This property allows the simulation graph (see Def.

Figure 1

 1 Figure 1 Timed automata of the train, the controller and the gate

Example 2

 2 the finite set of transitions. Given a zone z and an edge e ∈ T , if z = post(e, z, c) = ∅, then z is a zone of the graph and z e → z is a transition of the graph. Let us go back to the railroad crossing example as presented in Fig. 1. The simulation graphs built from each timed automaton are presented in Fig. 2. The polyhedron of each zone is represented (graphically) by a constraint given inside the zone. Paths and non-zeno paths in a simulation graph. A path in the simulation graph is a finite or infinite sequence

Figure 5

 5 Figure 5 Stability-respect and divergence-sensitivity

Figure 9

 9 Figure 9 Size of the simulation graphs of each component of the production cell

  Therefore, g only involves clocks of C and v C ∈ g. Thus, by construction of B C, a transition (s B , s C ) g,c,r → (s B , s C ) exists in B C. Since s A Ss B , and by definition of R, we have (s A , s C)R(s B , s C ). (ii) Consider a transition (s A , s C ) g,a,r → (s A , s C ) such that a ∈ (Σ A ∩ Σ B )\Σ C (the state s C is not modified). By definition of , the transition s A g,a,r → s A exists in A. Since s A Ss B , there is a transition s B g ,a,r → s B in B, such that s A Ss B . Thus, v B ∈ g . Sinceg only involves clocks of B and that the set of clocks of B and C are disjoint (by hypothesis in the construction of B C), then (v B , v C ) ∈ g and the transition (s B , s C ) g ,a,r→ (s B , s C ) exists in B C and (s A , s C )R(s B , s C ) by definition of R. (iii) Consider a transition (s A , s C ) g,a,r → (s A , s C ) such that a ∈ Σ A ∩ Σ C . Bydefinition of , there is a transition s A g1,a,r1 → s A in A and a transition s C g2,a,r2 → s C in C. There are two cases: either a ∈ Σ A ∩ Σ B (a is an observable action of A comparing to B and thus exists in B), or a ∈ Σ A \Σ B (a is a non-observable action of A which do not exists in B). In the first case, since s A Ss B , there is a transition s B g3,a,r3 → s B in B such that s A Ss B . Thus, there is a transition (s B , s C ) g ,a,r → (s B , s C ) in B C, such that (s A , s C )R(s B , s C ) by definition of R. In the second case, since s A Ss B , we have s A Ss B . The transition (s B , s C ) g2,a,r2 → (s B , s C ) exists in B C since v B do not involve clocks of C and v C ∈ g 2 . By definition of R, we have (s A , s C )R(s B , s C ).

  v 2 = [reset(e 2 ) := 0]v 2 and v 1 = [reset(e 1 ) := 0]v 1

  Y is a new valuation over Y containing only the values in v of clocks in Y . The reset in v of the clocks in Y , written [Y := 0]v is the valuation obtained from v by setting to zero all clocks in Y , and leaving the values of other clocks (∈ X\Y ) unchanged.

. Let X be a set of clocks. A clock valuation over X is a function v : X → R + mapping to each clock in X a value in R + . Let 0 denote the valuation assigning 0 to each clock in X. Operations on valuations. Let v be a valuation over X and t ∈ R + , the valuation v + t (respectively vt) is obtained by adding (resp. substracting) t to the value of each clock. Given Y ⊆ X, the dimension-restricting projection of v over Y , written v

  by refinement or by integration of components. Labels in Σ 2 \Σ 1 concern actions introduced by the development process and are considered as being non-observable and renamed by τ . Thus, Σ 2 = Σ 1 ∪ {τ }. Other actions are called observable. The timed τ -simulation, called S, is defined informally by the following points:

  The cases ∨ and ¬ are trivial. The interesting case is when the type of formula is ϕU I ψ. Let us prove that this kind of formula is preserved. Since σ 1 |= φ U I ψ, there exists a suffix σ t 1 at time t ∈ I such that σ t 1 |= ψ. Consider now the suffix σ t 2 of σ 2 at time t. The relation S ds forbids infinite sequences only composed of non-observable actions in ρ 2 (and thus, in σ 2 ). Thus, each discrete action which occurs in ρ 1 (and in σ 1 ) also occurs in ρ 2 (and thus in σ 2 ). Moreover, since S ds does not allow introduction of deadlocks in ρ 2 , if time t can be reached in ρ 1 (and in σ 1 ), then this time value t can also be reached in ρ 2 (and in σ 2 ). Mitl formula, A 1 and A 2 be two TA. If A 1 |= ϕ and A

	Consequently, if the suffix σ t 1 exists, the suffix σ t 2 also
	exists.
	We now prove that σ t 2 satisfies ψ. We know that σ t 1 satisfies ψ and that (induction hypothesis) ψ is
	preserved. It remains to prove that each run inscribed in
	σ t 2 is in relation w.r.t. S ds with a run inscribed in σ t 1 . By lemma 1, each run ρ 2 inscribed in σ t 2 is in relation (w.r.t S ds ) with a run ρ 1 inscribed in σ t 1 . Thus we have that σ t 2 |= p ψ.
	Since σ 1 |= φ U I ψ, then ∀t ∈]0, t[, σ t 1 |= φ. And thus, as
	previously, with lemma 1 and the induction hypothesis
	that φ is preserved, ∀t ∈]0, t[, σ t 2 |= p φ.
	Thus, σ 2 |= p φ U I ψ.
	2
	Theorem 1 (Preservation of MITL properties)
	Let ϕ be a

  R satisfies the strict simulation. Common clocks valuation equality: immediate by definition of R and since X A and X B are disjoint.

	4. Location labelling respect : immediate by definition
	of R.
	5. 2
	Proposition 4 (Compatibility) Let A, B and C be
	TA. If A S B then A C S B C.
	Proof. The structure of the proof is similar to the
	previous one. Details can be found in Appendix A.
	2
	Proposition 5 (Compositionality) Let A, B, C, D
	be TA. If A
	2. Delay equality: same arguments than those for
	strict simulation can be used to prove that this
	clause holds for R.

3. τ -transitions stuttering: consider a transition (s A , s B ) τ → (s A , s B ) in A B. Recall that τtransitions represent non-observable actions initially labelled by an action in Σ B \Σ A . By construction of A B, s A = s A . Thus, (s A , s B )R s A and R satisfies τ -transitions stuttering. S B and C S D then A C S B D. Proof. Immediate with Proposition 4. Since A S B, then A C S B C. Since C S D, then B C S B D. By transitivity of the relation S , we have A C S B D. 2

  we have z 02 Z ds z 01 . Let s 02 and s 01 be the respective initial states of A 2 and A 1 . By definition, s 02 ∈ z 02 and s 01 ∈ z 01 . By lemma 4, s 02 is in relation (w.r.t. S ds ) with a unique state s in z 01 . By definition of S ds , the valuations of s and s 02 over X 1 are equal. It follows that s = s 01 and s 02 S ds s 01 .

			⊇
	z 1		(modulo projection		z 2
		000 000 000 000 111 111 111 111	Z ds over X 1 )	000 000 000 111 111 111
	e 1	e 1	e 2	e 2	(label(e 2 ) = label(e 1 ))
			Z ds
	z 1				z 2

  Thus, the relation R satisfies the strict simulation. C exist respectively in A and C. Since s A Ss B , then the transition s B t → s B exists in B and s A Ss B . The transition (s B , s C ) B , s C ) exists also in A C and, by definition of R, (s A , s C )R(s B , s C ). 3. τ -transitions stuttering: in A C, comparing to B C, τ -transitions are labelled in Σ A \(Σ B ∪ Σ C ) (the hatched part in Fig. 11). Consider a transition (s A , s C ) A , s C ) (the state s C is not modified since τ represents an action of Σ A \(Σ B ∪ Σ C )). Since s A Ss B , we have s A Ss B . It follows that (s A , s C )R(s B , s C ). 4. Location labelling respect : immediate since s A Ss B . 5. Common clocks valuation equality: immediate since s A Ss B .

	transitions s A	t → s A	and	s C	t → s

2. Delay equality: consider a time transition (s A , s C ) t → (s A , s C ). By definition of , the t → (s τ → (s

Safety properties express that on some conditions, something never happens.

Liveness properties express that on some conditions, something will eventually happen.

The work presented in this section (except sections 3.3.2 and 3.3.3) was first presented in[START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF].

Note that we do not intend to directly check algorithmically this semantic definition. It will be extended into a symbolic relation (see section

5) where this clause delay equality consists in polyhedra inclusion and thus, is decidable.5 In the simulation graph, only discrete transitions appear. Thus, a τ -cycle is a cycle which only contains transitions labelled by τ . 6 Vesta at: http://lifc.univ-fcomte.fr/~oudot/VeSTA 7 This case study, as well as other experimentations, was first presented in(Bellegarde et al. 2006a). 8 These transitions are also in ΣA, since A S B and therefore ΣB ⊆ ΣA.

Appendix B. Proof of Lemma 4

The proof is done by fixed-point induction. Consider the function F :

iff the clauses 1 to 6 of Definition 6 hold.

In the definition of Z ds , we consider the greatest fixed-point of the function F . This function is trivially monotonic (and the sets Z 2 and Z 1 are finite), thus we can reason inductively about the pre-fixed-points of this function. The principle of this induction is the following: given a predicate P , this induction allows to prove P (Z ds ), by proving P (F (Z ds )), with the induction assumption that P (Z ds ) holds. Therefore, we suppose that ( ) is true for Z ds , and prove that ( ) holds for F (Z ds ). In other words, we prove that

We proceed clause by clause. For clarity's sake, we specify exactly the formula we intend to prove for each clause. We begin with the clause common clocks valuation equality since we use it in the rest of the proof.

1. Common clocks valuations equality: we prove that

The proof is immediate by definition of the operator .

Strict simulation

e1 → (q 1 , v 1 ) ∧ label(e 1 ) = label(e 2 ) ∧ (q 2 , v 2 )S ds (q 1 , v 1 ))).