Kim Guldstrand Larsen

Axel Legay
email: axel.legay@inria.fr

Louis-Marie Traonouez
email: louis-marie.traonouez@inria.fr

Andrzej Wąsowski
email: wasowski@itu.dk

Robust Synthesis for Real Time Systems

Keywords: Stepwise refinement, Timed I/O automata, Timed games, Specification theory, Robustness

published or not. The documents may come

L'archive ouverte

Introduction

Component-based design is a software development paradigm well established in the software engineering industry. In component-based design, larger systems are built from smaller modules that depend on each other in well delimited ways described by interfaces. The use of explicit interfaces encourages creation of robust and reusable components.

Practice of component-based design is supported by a range of standardized middleware platforms such as CORBA [START_REF] Group | Corba 3.2[END_REF], OSGi [START_REF] Mcaffer | OSGi and Equinox: Creating Highly Modular Java Systems[END_REF] or WSDL [START_REF]W3C, Web services description language (wsdl) version 2.0 part 1: Core language[END_REF]. These technologies are usually not expressive enough to handle intricate correctness properties of safety-critical concurrent real-time software-a domain where component-based design would be particularly instrumental to address the strict legal requirements for certification [START_REF] Standard | Functional safety of electrical/electronic/programmable electronic safety-related systems[END_REF]. To aid these needs, researchers work on developing trustworthy rigorous methods for component-oriented design. In the field of concurrency verification this includes compositional design (specification theories, stepwise-refinement) and compositional model checking. Akin to algebraic specifications, specification theories provide a language for specifying component interfaces together with operators for combining them, such as parallel (structural) composition or conjunction (logical composition), along with algorithms for verification based on refinement checking.

For real-time systems, timed automata [START_REF] Alur | A theory of timed automata[END_REF] are the classical specification language. Designs specified as timed automata are traditionally validated using model checking against correctness properties expressed in a suitable timed temporal logic [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF]. Mature modeling and model-checking tools exist, such as Uppaal [START_REF] Behrmann | Developing uppaal over 15 years[END_REF], that implement this technique and have been applied to numerous industrial applications [START_REF] Cimatti | Industrial applications of model checking[END_REF][START_REF] Long | Experience applying the spin model checker to an industrial telecommunications system[END_REF][START_REF] Keating | An industrial application of model checking to a vessel control system[END_REF][START_REF] Kammüller | An industrial application of symbolic model checking[END_REF][START_REF] Chandra | Software model checking in practice: an industrial case study[END_REF].

In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], we have proposed a specification theory for real time systems based on timed automata. A specification theory uses refinement checking instead of model-checking to support compositionality of designs and proofs from ground up. We build on an input/output extension of timed automata model to specify both models and properties. The set of state transitions of the timed systems is partitioned between inputs, representing actions of the environment, and outputs that represent the behavior of the component. The theory is equipped with a game-based semantic. The two players, Input and Output, compete in order to achieve a winning objective-for instance safety or reachability. These semantics are used to define the operations of the theory, including satisfaction (can a specification be implemented), refinement (how two specifications compare), logical composition (superposition of two specifications), structural composition (combining smaller components into larger ones), and quotient (synthesizing a component in a large design).

Let us illustrate the main concepts with an example. Figure 1a displays a specification of a coffee machine that receives an input coin? and outputs either coffee (cof!) or tea (tea!). It can be composed with the specification of a researcher in Fig. 1b by synchronizing input with output labeled with the same channel name (cof and tea). In Fig. 1b the researcher specifies that if tea arrives after 15 time units, she enters into an error state lu. We can say that if there exists an environment for these two specifications that avoids reaching this error state then the two specifications are compatible [START_REF] De Alfaro | Interface automata[END_REF]. In this particular example, such an environment simply needs to provide coin? sufficiently often. In general deciding existence of safe environments is reduced to establishing whether there exists a winning strategy in the underlying timed safety game.

Besides compatibility checking, the theory of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] is equipped with a consistency check to decide whether a specification can indeed be implemented. fee machine in Fig. 2. This machine first proposes to make a choice of a drink, then awaits a coin, and, after receiving the payment, delivers the coffee. If the payment does not arrive within six time units, the machine aborts the drink selection and returns to the initial state, awaiting a new choice of a beverage. Already in this simple example it is quite hard to see that implementing a component satisfying this specification is not possible due to a subtle mistake. Suppose that the environment makes the choice? action in the Idle location, waits six time units, and then provides the coin? action. In such execution the system reaches the location Serving with clock y at value 6. The invariant y ≤ 6 in the Serving location requires now that any valid implementation must deliver the coffee (cof!) immediately, in zero time units. No physical system would permit this, so we say that this state is not robustly consistent.

The above example can be fixed easily by adding another reset to clock y, when the coin? message is received. It is probably the intended behaviour of the specification that the serving should take six time units from the insertion of the coin, and not from the choice of the drink. After all the machine does not control how much time passes between the choice of the drink and the payment. An alternative simple fix is to allow the timeout abort transition to be taken earlier -for example after four time units. This would guarantee at least two time units for brewing the coffee. Despite both corrections being quite simple, it is clear that subtle timing mistakes like this one are very difficult to spot. Finding such errors in specifications is even harder in larger designs as non-robust timing can emerge in the compositions of multiple specifications, as a result of combing behaviours that themselves are robust. Examples exist where independent components appear compatible, but their compatibility requires infinitely precise execution platform or an infinitely fast environment.

The timing precision errors in specifications are not handled in any way in idealized interface theories such as [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF][START_REF] De Alfaro | Timed interfaces[END_REF]. These and similar issues have led to a definition of the timing robustness problem that checks if a model can admit some timing perturbations while preserving a desired property. The robustness problem has been studied in various works for timed automata. Providing a solution to this problem in the setting of timed I/O specifications is the objective of this paper:

• We propose a notion of implementation of a specification that is robust with respect to a given perturbation in the delay before an action. The concept of robust implementation is lifted to a robust satisfaction relation that takes variations of timed behaviors into account when checking whether the implementation matches the requirement of the specification.

• Classical compositional design operators are lifted to the robust setting. One of the remarkable features of this new theory is that this does not require modifications to the definitions of the operators themselves and that all the good properties of a specification theory (including independent implementability) are maintained-the only effort requires is reproving the properties of the operators in a non-idealized setting.

• We propose a consistency check for robust satisfaction. This new check relies on an extension of the classical timed I/O game to the robust setting.

In [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF], Chatterjee et al. show that problems on robust timed games can be reduced to classical problems on an extended timed game. We modify the original construction of [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] to take the duality of inputs and outputs into account. Then, we show how our new game can be used to decide consistency in a robust setting as well as to synthesize a robust implementation from a given specification.

• Finally, we present a technique that computes the greatest admissible perturbations for the robustness problems. We apply a counterexample abstraction refinement-like technique that analyzes parametrically the results of loosing timed games in order to refine the value of the perturbation. This technique and the different constructions presented in the paper are implemented in a prototype tool. We demonstrate the performance of the refinement heuristic against the baseline of a simple binary search technique for finding an optimal precision value.

To the best of our knowledge, this paper presents the first theory for stepwise refinement and specification of timed systems in a robust manner. While the presentation is restricted to the theory of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], we believe that our methods work for any timed specifications. Our experience with industrial projects shows that such realistic design theories are of clear interest [START_REF]Combest[END_REF][START_REF]Speeds[END_REF][START_REF] Badouel | Contract Theories for Embedded Systems : A white paper[END_REF].

Organization of the paper. We proceed by summarizing the state of the art in Section 2 and introducing the background on Timed Specifications (Section 3). In Section 4 we introduce methods for solving robust time games that arise in our specification theory. These methods are used in Sections 5 to reason about consistency, conjunction, parallel composition, in order to synthesize robust implementations of real time components. In Section 6 we develop a counterexample refinement technique to measure the maximum imprecision allowed by the specifications. Finally in Section 7 we present a prototype that implements some of the functionalities of the tool ECDAR, extended with the robustness concepts presented in this paper. We demonstrate this tool on three experiments.

State of The Art

In the literature the robustness problem has been considered for timed automata using logical formulas as specifications (and neglecting compositional design operators). The robust semantics for timed automata with clock drifts has been introduced by Puri [START_REF] Puri | Dynamical properties of timed automata[END_REF]. The problem has been linked to the implementation problem in [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF], which introduced the first semantics that modeled the hardware on which the automaton is executed. In this work, the authors proposed a robust semantics of Timed Automata called AASAP semantics (for "Almost As Soon As Possible"), that enlarges the guards of an automaton by a delay ∆. This work has been extended in [START_REF] Wulf | Robust safety of timed automata[END_REF] to propose another robust semantics with both clock drifts and guard enlargement. Extending [START_REF] Puri | Dynamical properties of timed automata[END_REF] they solve the robust safety problem, defined as the existence of a non-null value for the imprecision. They show that in terms of robust safety the semantics with clock drifts is just as expressive as the semantics with delay perturbation. We extend the work of [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF][START_REF] Wulf | Robust safety of timed automata[END_REF] by considering compositional design operators, stepwise-refinement, and reasoning about open systems (only closed system composition were considered so far).

We solve games for consistency and compatibility using a robust controller synthesis technique inspired by Chatterjee et al. [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF], who provide synthesis techniques for robust strategies in games with parity objectives. Driven by the fact that consistency and compatibility are safety games, we restrict ourselves to safety objectives, but we extend [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] by allowing negative perturbation of delays.

Our paper is also similar to the works in [START_REF] Bouyer | Timed automata can always be made implementable[END_REF][START_REF] Sankur | Shrinking timed automata[END_REF] that show how one can synthesize from any timed automaton an equivalent robust automaton. We also synthesize robust components, but we start from the specification and we apply a controller synthesis methods to the specification, rather than modifying an existing implementation.

Robustness is defined in [START_REF] Wulf | Robust safety of timed automata[END_REF] as the existence of a positive value for the imprecision of a timed automaton. The papers shows that this problem is decidable, but it does not show how to synthesize the value. A bound on the value is computed in [START_REF] Bouyer | Robust model-checking of timed automata via pumping in channel machines[END_REF]. Finally a quantitative analysis is performed in [START_REF] Jaubert | Quantitative robustness analysis of flat timed automata[END_REF] that computes the greatest admissible value for the perturbation, but the method is restricted to timed automata without nested loops. We propose an approximation technique that computes this value in our timed specifications context, with no major restrictions on syntax of the specifications.

There is presently no alternative specification theory for timed systems with support for robustness. A preliminary version of this paper has appeared in [START_REF] Larsen | Robust specification of real time components[END_REF]. This version differs from the short version by including proofs of theorems, by adding two entirely new sections presenting parametric methods for robustness (Sections 6-7). The algorithms of [START_REF] Larsen | Robust specification of real time components[END_REF] merely check whether a given specification is robust with respect to a given timing precision parameter. The new methods compute the maximum value of the precision for which the specification is robustly consistent (or two specifications are robustly compatible). We also add an experimental evaluation of the performance of the proposed methods.

Background on Timed I/O Specifications

We now recall the definition of Timed I/O specifications [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]. We use N for the set of all natural numbers, R for the set of all real numbers, and R ≥0 (resp. R >0 ) for the non-negative (resp. strictly positive) subset of R. Rational numbers are denoted by Q, and their subsets are denoted analogously. For x ∈ R ≥0 , let x denote the integer part of x and x denote its fractional part. Given a function f on a domain D and a subset C of D, we denote by f |C the restriction of f to C.

Timed I/O Transitions Systems and Timed I/O Automata

In the framework of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], specifications and their implementations are semantically represented by Timed I/O Transition Systems (TIOTS) that are nothing more than timed transition systems with input and output modalities on transitions. Later we shall see that input represents the behaviors of the environment in which a specification is used, while output represents behaviours of the component itself.

Timed I/O Transitions Systems

Definition 1 A Timed I/O Transition System is a tuple S = (St S , s 0 , Σ S , → S ), where • St S is an infinite set of states, • s 0 ∈ St S is the initial state, • Σ S = Σ S i Σ S
o is a finite set of actions partitioned into inputs Σ S i and outputs Σ S o ,

• and → S :

St S ×(Σ S ∪ R ≥0 )×St S is a transition relation.
We write s a -→ S s when (s, a, s ) ∈→ S , and use i?, o! and d to range over inputs, outputs and R ≥0 , respectively.

In what follows, we assume that any TIOTS satisfies the following conditions: A run ρ of a TIOTS S from its state s 1 is a sequence

s 1 a1 -→ S s 2 a2 -→ S . . . s n-1 an-1 ---→ S s n an --→ . . . such that for all 1 ≤ i ≤ n, s i ai -→ S s i+1 with a i ∈ Σ S ∪ R ≥0 .
We write Runs(s 1 , S) for the set of runs of S starting in s 1 and Runs(S) for Runs(s 0 , S). We write States(ρ) for the set of states reached in ρ, and if ρ is finite then we denote the last state occurring in ρ by last(ρ).

A TIOTS S is deterministic iff the action or delay fully determines the next state: ∀a ∈ Σ S ∪ R ≥0 , whenever s a -→ S s and s a -→ S s , then s = s . It is input-enabled iff there is an input transition for every input action in each of its states s ∈ St S : ∀i? ∈ Σ S i . ∃s ∈ St S . s i?

-→ S s . A TIOTS is output urgent iff whenever an output transition is possible, no further delaying is allowed:

∀s, s , s ∈ St S if ∃o! ∈ Σ S o .∃d ≥ 0.s o! -→ S s and s d -→ S s then d = 0
Output urgency captures predictability of timing of system's reactions. Finally, we say that a TIOTS S satisfies the independent progress condition iff it can always evolve using delays and outputs, regardless whether the environment collaborates providing inputs or not. This is not a limiting assumption-in real systems, when the environment does not interact, the time is simply passing, and so it should be possible in the models of systems. ). Given a valuation u and d ∈ R ≥0 , we write u+d for the valuation in which for each clock x ∈ Clk we have (u+d)(x) = u(x)+d. For λ ⊆ Clk, we write u[λ] for a valuation agreeing with u on clocks in Clk \ λ, and giving 0 for clocks in λ.

Let B(Clk) denote all clock constraints ϕ generated by the grammar ϕ ::

= x ≺ k | x -y ≺ k | ϕ ∧ ϕ,
where k ∈ Q, x, y ∈ Clk and ≺ ∈ {<, ≤, >, ≥}. By U(Clk) ⊂ B(Clk), we denote the set of constraints restricted to upper bounds and without clock differences. For constraint ϕ ∈ B(Clk) and u ∈ R Clk ≥0 , we write

u |= ϕ if u satisfies ϕ. If Z ⊆ R Clk ≥0 , we write Z |= ϕ if u |= ϕ for all u ∈ Z. We write ϕ to denote the set of valuations {u ∈ R Clk ≥0 | u |= ϕ}. A subset Z ⊆ R Clk ≥0 is a zone if Z = ϕ for some ϕ ∈ B(Clk). Let Clk ⊂ Clk and Z ⊆ R Clk
≥0 be a zone. We define the projection of Z on the subset of clocks Clk as

Z |Clk = {u ∈ R Clk ≥0 | ∃u ∈ Z.u = u |Clk }.
Definition 2 A Timed I/O Automaton is a tuple A = (Loc, q 0 , Clk, E, Act, Inv), where

• Loc is a finite set of locations,

• q 0 ∈ Loc is the initial location,

• Clk is a finite set of clocks,

• E ⊆ Loc × Act × B(Clk) × 2 Clk × Loc is a set of edges,
• Act = Act i Act o is a finite set of actions, partitioned into inputs (Act i ) and outputs (Act o ),

• Inv : Loc → U(Clk) is a set of location invariants.

Without loss of generality we assume that the guards are satisfiable and that the invariants are always satisfied by the incoming edges. Formally, let e = (q, a, ϕ, λ, q ) ∈ E, we assume that ϕ = ∅ and that ∀u ∈ ϕ .u[λ] |= Inv(q ).

A universal location, denoted l u , in a TIOA accepts every input and can produce every output at any time. Formally l u is such that, ∀a ∈ Act.∃(l u , a, , ∅, l u ) ∈ E, where is the clock constraints such that = R Clk ≥0 . We assume that every TIOA contains a universal location, even if it is not drawn on the graph. The universal location will be used to model an unpredictable behavior of a component. 1b on page 3 depicts an example of a TIOA that admits two input actions cof? and tea?, and one output action pub!. Edges are labeled with an action, a guard and a set of reset clocks. Edges with input action are drawn with plain arrows, while Edges with output action are drawn with dashed arrows. Location are labeled with a name and an invariant constraint. lu is the universal location.

Example 1 Figure

The semantics of a TIOA A = (Loc, q 0 , Clk, E, Act, Inv) is a TIOTS A sem = (Loc × R Clk ≥0 , (q 0 , 0), Act, →), where 0 is a constant function mapping all clocks to zero, and → is the largest transition relation generated by the following rules:

• Each edge (q, a, ϕ, λ, q ) ∈ E gives rise to (q, u)

a -→(q , u ) for each clock valuation u ∈ R Clk ≥0 such that u |= ϕ and u = u[λ].
• Each location q ∈ Loc with a valuation u ∈ R Clk ≥0 gives rise to a transition (q, u) --→(C, (0))

d -→(q, u + d) for each delay d ∈ R ≥0 such that u + d |= Inv(q).
2.6 --→(C, (2.6)) pub! --→(Idle, (0))
Let X be a set of states in A sem . For a ∈ Act the a-successors and a-predecessors of X are defined respectively by:

Post a (X) = {(q , u ) | ∃(q, u) ∈ X. (q, u) a -→(q , u )} Pred a (X) = {(q, u) | ∃(q , u ) ∈ X. (q, u) a -→(q , u )}
The timed successors and predecessors of X are respectively defined by:

X = {(q, u + d) | (q, u) ∈ X, d ∈ R ≥0 } X = {(q, u -d) | (q, u) ∈ X, d ∈ R ≥0 }
The safe timed predecessors of X with respect to a set of unsafe states Y are the set of timed predecessors of X such that the states of Y are avoided along the path:

Pred t (X, Y ) = {(q, u) | ∃d ∈ R ≥0 . (q, u) d -→(q, u + d) and (q, u + d) ∈ X and ∀d ∈ [0, d]. (q, u + d ) ∈ Y }
These operations can be implemented symbolically on zones using Difference Bound Matrices (DBMs) [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF].

Symbolic abstractions

Since TIOTSs are infinite size they cannot be directly manipulated by computations. Usually symbolic representations, such as region graphs [START_REF] Alur | A theory of timed automata[END_REF] or zone graphs, are used as data structures that finitely represent semantics of TIOAs. A symbolic state is a pair (q, Z) that combines all concrete states (q, u) such that u ∈ Z, where q ∈ Loc and Z ⊆ R Clk ≥0 . Usually symbolic states are formed combining locations with special kinds of sets of valuations: regions and zones. Recall that zones are sets expressed by clock constraints in TIOAs. We now define regions.

Let M be the integer constant with the greatest absolute value among constants appearing in the guards and invariants of a TIOA1 . A clock region is an equivalence class of the relation ∼ on clock valuations such that u ∼ v iff the following conditions hold:

• ∀x ∈ Clk, either u(x) = v(x) , or u(x) > M and v(x) > M , • ∀x, y ∈ Clk, ∀k ∈ [-M, M ], u(x) -u(y) ≤ k iff v(x) -v(y) ≤ k, • ∀x ∈ Clk if u(x) ≤ M then u(x) = 0 iff v(x) = 0,
We write r for the region that is the unique direct time successor of region r, if such exists. Formally, r is the regions such that ∀u ∈ r.∃d > 0.(u + d ∈ r ∧ ∀d < d.u + d ∈ r ∪ r ). For a clock valuation u, we write [u] to denote the unique region containing u.

The region graph of a TIOA A is a triple

G A = (R A , r 0 , - →), where R A = {(q, [u]) | (q, u) ∈ St A sem }
is the set of symbolic states, r 0 = (q 0 , [0]) is the initial symbolic state, and -→ ⊆ R A × (Act ∪ {τ }) × R A , such that (q, r) τ -→(q, r ) iff r |= Inv(q), and (q, r) a -→(q , r ) iff (q, u) a -→(q , u ) for some u ∈ r and u ∈ r . The zone graph G A = (Z A , X 0 , -→) is defined analogously, but using zones instead of regions. It provides a coarser abstraction, in which only discrete transitions are observed. There, Z A is the set of reachable symbolic states:

(q, Z) ∈ Z A if Z is a zone of R Clk ≥0 .
The initial symbolic state is defined by X 0 = {(q 0 , 0 ∩ Inv(q 0 ) )}. For action a ∈ Act there is an edge (q, Z)

a -→(q , Z ) iff (q, a, ϕ, λ, q ) ∈ E with Z = ((Z ∩ ϕ )[λ]) ∩ Inv(q ) .

Basics of the Timed Specification Theory

In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], timed specifications and implementations are both represented by TIOAs satisfying additional conditions: Definition 3 A specification S is a TIOA whose semantics S sem is deterministic and input-enabled. An implementation I is a specification whose semantics I sem additionally satisfies the output urgency and the independent progress conditions.

Example 3

The TIOA in Figure 1b is a specification of a researcher. It accepts either coffee (cof) or tea in order to produce publications (pub). If tea is served after a too long period the researcher falls into an error state, represented by the universal state lu. An implementation of this specification is presented in Figure 3. It is output urgent since it produces pub exactly 3 time units after receiving cof and 6 time units after receiving tea. The location Blocked is an implementation of the universal location that never produces pub. In specification theories, a refinement relation plays a central role. It allows to compare specifications, and to relate implementations to specifications. In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], as well as in [START_REF] De Alfaro | Interface automata[END_REF][START_REF] De Alfaro | Interface-based design[END_REF][START_REF] Bulychev | Efficient on-the-fly algorithm for checking alternating timed simulation[END_REF], refinement is defined in the style of alternating (timed) simulation:

q x ≤ 10 q 1 q 2 q 3 a! x ≥ 4 c? x < 8 c? x ≥ 8 b! x ≤ 9 (a) Specification S q x ≤ 6 q 1 a! x ≥ 5 c? (b) Specification T q x ≤ 6 q 1 q 2 q 3 a! x ≥ 5 c? b! x ≤ 9 (c) Specification U
= (St T , t 0 , Σ , → T ) and S = (St S , s 0 , Σ , → S ) is a relation R ⊆ St T × St S such that (t 0 , s 0 ) ∈ R and for every (t, s) ∈ R • If ∃i? ∈ Σ i .∃s ∈ St S .s i? -→ S s , then ∃t ∈ St T .t i? -→ T t and (t , s ) ∈ R. • If ∃o! ∈ Σ o .∃t ∈ St T .t o! -→ T t , then ∃s ∈ St S .s o! -→ S s and (t , s ) ∈ R. • If ∃d ≥ 0.∃t ∈ St T .t d -→ T t , then ∃s ∈ St S .s d -→ S s and (t , s ) ∈ R.
We write T ≤ S if there exists an alternating simulation between T and S. For two TIOAs T and S, we say that T refines S, written T ≤ S, iff T sem ≤ S sem .

Example 4

We illustrate the concept of refinement between three simple specifications presented in Figure 4. T refines S, because it can only delay up to x = 6 and performs a! between [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF]. However, U does not refine S (and S does not refine U), because when c? is received at x = 0, the states (q, 0) from S and (q 2 , 0) from U must be in relation, which is not possible because (q 2 , 0) b! -→ U (q 3 , 0) is not allowed at (q, 0) by S. The reader might find it surprising that in a robust specification theory we refrain from adjusting the refinement to account for imprecision of implementations when comparing specifications. Our basic assumption is that specifications are precise mathematical objects that are not susceptible to imprecision of execution. In contrary, implementations can behave imprecisely when executed, so in Section 4 we will introduce an extension of Def. 5 that takes this into account. It is a fortunate property of Def. 4 that we do not need to modify it in order to reason about robust implementations (Property 3 in Sect. 4).

In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], we have reduced refinement checking to finding winning strategies in timed games. In the reminder of this section, we recall the definition of such games and show how they can be used to check consistency. Timed games also underly other operations such as conjunction, composition, and quotient [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], which will be illustrated in Sect. 5.

Timed Games for Timed I/O Specifications

TIOAs are interpreted as two-player real-time games between the output player (the component) and the input player (the environment). The input player plays with actions in Act i and the output player plays with actions in Act o . A strategy for a player is a function that defines her move at any given time (either delaying or playing a controllable action). The delay chosen by one player is implicitely defined by the time until a controllable action is chosen. A strategy is called memoryless if the next move depends solely on the current state. We only consider memoryless strategies, as these suffice for safety games [START_REF] De Alfaro | The element of surprise in timed games[END_REF]. For simplicity, we only define strategies for the output player (i.e. output is the verifier). Definitions for the input player are obtained symmetrically.

Definition 7 A memoryless strategy f o for the output player on the TIOA A is a partial function St

A sem → Act o ∪ {delay}, such that • Whenever f o (s) ∈ Act o then s fo(s)
---→s for some s . The game proceeds as a concurrent game between the two players, each proposing its own strategy. The restricted behavior of the game defines the outcome of the strategies.

Definition 8

Let A be a TIOA, f o and f i be two strategies over A for the output and input player, respectively, and s be a state of A sem . Outcome(s, f o , f i ) is the subset of Runs(s, A sem ) defined inductively by:

• s ∈ Outcome(s, f o , f i ), • if ρ ∈ Outcome(s, f o , f i ), then ρ = ρ a -→s ∈ Outcome(s, f o , f i ) if ρ ∈ Runs(s, A sem )
and one the following conditions hold: A winning condition for a player in the TIOA A is a subset of Runs( A sem ). This player is then called the verifier, whereas the other player tries to prevent her from winning, and therefore is called the spoiler. In safety games the winning condition is to avoid a set Bad ⊆ St A sem of "bad" states. Formally, the winning condition for output is

1. a ∈ Act o and f o (last(ρ)) = a, 2. a ∈ Act i and f i (last(ρ)) = a, 3. a ∈ R ≥0 and ∀d ∈ [0, a[. ∃s . last(ρ) d -→s and ∀k ∈ {o, i} f k (s ) = delay. • ρ ∈ Outcome(s, f o , f i ) if ρ is infinite and all its finite prefixes are in Outcome(s, f o , f i ).
W o (Bad) = {ρ ∈ Runs( A sem ) | States(ρ) ∩ Bad = ∅}.
A strategy f o is a winning strategy from state s if and only if, for all strategies

f i of input, Outcome o (s, f o , f i ) ⊆ W o (Bad). On the contrary, a strategy f i for input is a spoiling strategy of f o if and only if Outcome(s, f o , f i ) ⊆ W o (Bad).
A state s is winning for output if there exists a winning strategy from s. The game (A, W o (Bad)) is winning if and only if the initial state is winning. Solving this game is decidable [START_REF] Maler | On the synthesis of discrete controllers for timed systems (an extended abstract)[END_REF][START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF][START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]. We only consider safety games in this paper, and without lost of generality we assume these "bad" states are specified by a set of entirely "bad" locations (in the sense that all states in which such a location participates are bad).

Strategies in Timed Games as Operators on Timed Specifications. We sketch how timed games can be used to establish consistency of a timed specification.

An immediate error occurs if the specification disallows progress of time and output transitions in a given state-such a specification will break if the environment does not send an input. For a specification S we define the set of immediate error states err S ⊆ St S sem as:

err S = s (∃d. s d -→) and ∀d ∀o! ∀s . s d -→s implies s o! --→
It follows that no immediate error states can occur in implementations, since they verify independent progress. In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] we show that S is consistent (see Def. 6) iff there exists a winning strategy for output in the safety game (S, W o (err S )).

Consider the example specification of another coffee machine on Figure 5. There is a unique reachable error state err S = {(Blocked, 0)}. Now let us take a strategy for the output player, f o , such that f o ((Serving, 4)) = coff!, and ∀y = 4.f o (Serving, y)) = delay. It can be translated into an implementation of the coffee machine, in which tea is never served. Thus this specification is consistent.

Robust Timed I/O Specifications

We now define a robust extension of our specification theory. An essential requirement for an implementation is to be realizable on a physical hardware, but this requires admitting small imprecisions characteristic for physical components (computer hardware, sensors and actuators). The requirement of realizability has already been linked to the robustness problem in [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF] in the context of model checking. In specification theories the small deficiencies of hardware can be reflected in a strengthened satisfaction relation, which introduces small perturbations to the timing of implementation actions, before they are checked against the requirements of a specification. This ensures that the implementation satisfies the specification even if its behavior is perturbed.

We first formalize the concept of perturbation. Let the constraint ϕ ∈ B(X) be a guard over the set of clocks X. For all ∆ ∈ Q ≥0 , the enlarged guard ϕ ∆ is constructed according to the following rules:

• Any term x ≺ k of ϕ with ≺ ∈ {<, ≤} is replaced by x ≺ k+∆ • Any term x k of ϕ with ∈ {>, ≥} is replaced by x k-∆
Similarly, the restricted guard ϕ ∆ is using the two following rules:

• Any term x ≺ k of ϕ with ≺ ∈ {<, ≤} is replaced by x ≺ k-∆ • Any term x k of ϕ with ∈ {>, ≥} is replaced by x k+∆.
Notice that for a for a clock valuation u and a guard ϕ, we have that u |= ϕ implies u |= ϕ ∆ , and u |= ϕ ∆ implies u |= ϕ, and ϕ ∆ ∆ = ϕ ∆ ∆ = ϕ.

Perturbed Implementation and Robust Timed I/O Specifications.

We lift the perturbation to implementation TIOAs. Given a jitter ∆, the perturbation means a ∆-enlargement of invariants and of output edge guards. Guards on the input edges are restricted by ∆: Definition 9 For an implementation I = (Loc, q 0 , Clk, E, Act, Inv) and ∆ ∈ Q ≥0 , the ∆-perturbation of I is the TIOA I ∆ = (Loc, q 0 , Clk, E , Act, Inv ), such that:

• Every edge (q, o!, ϕ, λ, q ) ∈ E is replaced by (q, o!, ϕ ∆ , λ, q ) ∈ E , • Every edge (q, i?, ϕ, λ, q ) ∈ E is replaced by (q, i?, ϕ ∆ , λ, q ) ∈ E , • ∀q ∈ Loc. Inv (q) = Inv(q) ∆ ,
• ∀q ∈ Loc. ∀i? ∈ Act i there exists and edge (q, i?, ϕ u , ∅, l u ) ∈ E with I ∆ is not necessarily action deterministic, as output guards are enlarged. However it is input-enabled, since by construction (last case in the previous definition), any input not accepted after restricting input guards is redirected to the universal location l u . Also I 0 equals I. An illustration of this transformation is presented in Figure 6.

ϕ u = ¬   (q,i?,ϕ,λ,q )∈E ϕ ∆   q x ≤ 10 q 1 q 2 q 3 l u o! x ≥ 10 i? x ≥ 8 i? x < 8 (a) Implementation I q x ≤ 11 q 1 q 2 q 3 l u o! x ≥ 9 i? x ≥ 9 i? x < 7 i? 7 ≤ x < 9 (b) I 1 , the ∆-perturbation of I
In essence, we weaken the constraints on output edges, and strengthen the constraints on input edges. This is consistent with the game semantics of specifications: perturbation makes the game harder to win for the verifier. Since the gaps created by strengthening input guards are closed by edges to the universal location, the implementation becomes less predictable. If an input arrives close to the deadline, the environment cannot be certain it will be handled precisely as specified. Enlargement of output guards has a similar effect. The environment of the specification has to be ready that outputs will arrive slightly after the deadlines.

Such considerations are out of place in classical robustness theories for model checking, but are crucial when moving to models, where input and output transitions are distinguished. For example, in [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF] the authors propose a robust semantics for timed automata. Their maximal progress assumption is equivalent to the output urgency condition of our implementations. However, in [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF] both input and output guards are increased, which is suitable for the one-player setting, but incompatible with the contravariant nature of two-player games. Such enlargement would not be monotonic with respect to the alternating refinement (Def. 4), while the perturbation of Def. 9 is monotonic.

We are now ready to define our notion of robust satisfaction:

Definition 10 An implementation I robustly satisfies a specification S for a given delay ∆ ∈ Q ≥0 , denoted I sat ∆ S, iff I ∆ ≤ S. We write S ∆ mod for the set of all ∆-robust implementations of S, such that

S ∆ mod = {I | I sat ∆ S ∧ I is an implementation}
Property 1 (Monotonicity) Let I be an implementation and 0 ≤ ∆ 1 ≤ ∆ 2 . Then:

I ≤ I ∆1 ≤ I ∆2
I ∆2 sem . Let R = {(s 1 , s 2 ) ∈ St I ∆ 1 sem × St I ∆ 2 sem | s 1 = (q, u) = s 2 }
be a candidate alternating simulation relation. We prove by co-induction that R satisfies Def. 4. Consider any state (q, u) such that (q, u)R(q, u).

1. If (q, u) d -→ I1 (q, u + d) for some d ∈ R ≥0 , then (q, u) d -→ I2 (q, u + d), since u + d |= Inv(q) ∆1 ⇒ u + d |= Inv(q) ∆2 . 2. If (q, u) o! -→ I1 (q , u ), then (q, u) o! -→ I2 (q , u ), since u |= ϕ ∆1 ⇒ u |= ϕ ∆2
(where ϕ is the guard of the edge that fires o!), and, similarly, u |= Inv(q

) ∆1 ⇒ u |= Inv(q ) ∆2 . 3. If (q, u) i? -→ I2 (q , u ) then (q, u) i? -→ I1 (q , u ), since u |= ϕ ∆2 ⇒ u |= ϕ ∆1
(where ϕ is the guard of the edge that fires i?). Besides u |= ϕ and therefore we assume that u |= Inv(q ), which implies that u |= Inv(q ) ∆1 .

Clearly, both transition systems I ∆1 sem and I ∆2 sem share the same initial state s 0 and s 0 Rs 0 , which concludes the proof. The argument that I ≤ I ∆1 proceeds similarly with the same witness relation R.

In addition, we obtain these properties by transitivity of alternating simulation:

Property 2 Let S be a specification and ∆ 1 ≤ ∆ 2 . Then:

S ∆2 mod ⊆ S ∆1 mod ⊆ S mod
Property 3 Let S and T be specifications and 0 ≤ ∆. Then:

S ≤ T =⇒ S ∆ mod ⊆ T ∆ mod
The definition of robust satisfaction naturally induces a notion of robust consistency (implementability): Definition 11 Let S be a specification and ∆ ∈ Q >0 , then S is ∆-robust consistent iff there exists an implementation I such that I sat ∆ S.

Like in the non-robust case, deciding consistency is reducible to solving games. But now, we will need to make the games aware of the robustness conditions. In the rest of this section, we propose a definition for such games. Then, in Section 5 we show how they can be used to perform classical operations on specifications.

Example 5 Figure 7 presents a ∆-perturbation of the researcher implementation presented in Fig. 3. This implementation robustly satisfies the specification of Fig. 1b for any ∆ ∈ ]0, 1]. However, for ∆ = 2 the following run is possible in the perturbed implementation:

(Idle, (0)) cof? --→ (C, (0)) 5 -→ (C, (5))
but it cannot be matched by the specification because it exceeds the invariant of the location corresponding to C in Fig. 1b.

Robust Timed Games for Timed I/O Specifications.

As we have seen timed specifications are interpreted as timed games. Solving games is used to analyze and synthesize real-time components. Now that we add imprecision to models, we need a notion of suitable games that can be used to synthesize robust components. Therefore we extend timed games with ∆perturbations, and study the synthesis of robust timed strategies. Note that it is not enough to restrict the specifications in order to synthesize robust components, since the behaviors removed might still happen after the ∆-perturbation and could lead to error states. However we propose a construction that encodes a robust game into a classical timed game.

De Alfaro et al. show [START_REF] De Alfaro | The element of surprise in timed games[END_REF] that timed games can be solved using region strategies, where the players only need to remember the sequence of locations and clock regions, instead of the sequence of states used in Definition 7. Consequently timed games can be solved through symbolic computations performed on symbolic graphs (either the region graph or the zone graph) using for instance the algorithm presented in [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF]. The following definition formalizes the notion of a symbolic strategies, which can be represented using symbolic states only: Definition 12 A symbolic strategy F for the output player is a function Z → Act o ∪{delay}, where Z is a set of symbolic states, such that whenever F ((q, Z)) ∈ Act o then for each u ∈ Z we have (q, u) -----→(q , u ) for some (q , u ). A symbolic strategy for the input player is defined analogously.

F ((q,Z))
A symbolic strategy F corresponds to the set of (non-symbolic explicit) strategies f such that whenever F ((q, Z)) = a then f ((q, u)) = a for some u ∈ Z. Syntactic outcomes. The following construction represents the outcome of applying a symbolic strategy to a TIOA as another timed automaton. It decorates a region graph with clocks, guards and invariants. We exploit the region graph construction in the definition, but any stable partitioning of the state-space could serve this purpose, and would be more efficient in practice.

Definition 13

Let A = (Loc, q 0 , Clk, E, Act, Inv) be a TIOA and F a symbolic strategy over A for output. The TIOA A F = (R A , (q 0 , r 0 ), Clk, E, Act ∪ {τ }, Inv) representing the outcome of applying F to A is built by decorating the region graph

G A = (R A , - → G ) of A.
For each region r in location q, the incident edges and the invariant are defined as follows:

• ((q, r), τ, r , ∅, (q, r )) ∈ E iff (q, r) τ -→ G (q, r ).

• For each edge (q, i?, ϕ, λ, q ) ∈ E, ((q, r), i?, ϕ, λ, (q , r )) ∈ E, iff (q, r)

i?

-→ G (q , r ).

• If F ((q, r)) = delay then Inv(q, r) = Inv(q) ∧ (r ∨ r ),

• If F ((q, r)) = o!, then Inv(q, r) = r, and for each edge (q, o!, ϕ, λ, q ) ∈ E,

((q, r), o!, ϕ, λ, (q , r )) ∈ E, iff (q, r) o! -→ G (q , r ).
In a robust timed game we seek strategies that remain winning after perturbation by a delay ∆. The perturbation is defined on the syntactic outcome of the strategy, by enlarging the guards for the actions of the verifier, so that each action can happen within ∆ time of what the strategy originally prescribes. We write A o ∆ (respectively A i ∆ ) for the TIOA where the guards of the output (resp. input) player and the invariants have been enlarged by ∆-so every guard ϕ has been replaced by ϕ ∆ and every invariant γ by γ ∆ . Definition 14 For a timed game (A, W o (Bad)), a symbolic strategy F for output is ∆-robust winning if it is winning when the moves of output are perturbed, i.e.

Runs( A

F o ∆ sem ) ⊆ W o (Bad)
In the rest of this section we describe a technique to find these robust strategies by modifying the original game automaton.

Robust game automaton

Robust timed games for a bounded delay can be reduced to classical timed games by a syntactic transformation of the game automaton [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF]. Below in Def. 15, we propose an extended version of the construction presented in [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF]. We admit both positive and negative perturbations of the player moves. In the original construction of [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] only delayed executions of actions were treated, but premature execution of communication may also lead to a safety violation in a specification theory, so we have to account for them. Then we show, in Theorem 1, how this construction can be used to find robust strategies as defined in Def. 14.

Let (A, W o (Bad)) be a timed game, where A = (Loc, q 0 , Clk, E, Act, Inv) and Bad ∈ Loc. We assume that all the constants in A are integers and we consider a perturbation ∆ ∈ N.

q rob , from an automaton A, with one location q and incident edges e = (q, o!, ϕ o , λ o , q 1 ) and (q, i?, ϕ i , λ i , q 2 ).

Inv(q) q 1 q 2 o! ϕ o , λ o i? ϕ i , λ i (a) TIOA A q Inv(q) q α e y ≤ ∆ q β e y ≤ ∆ q 1 q 2 Bad τ o! ϕ o , y := 0 i? ϕ i , λ i τ o! y = ∆, y := 0 o!, ϕ o ∧ Inv(q), λ o o! ¬(ϕ o ∧ Inv(q)) i? ϕ i , λ i o! ϕ o ∧ Inv(q), λ o o! ¬(ϕ o ∧ Inv(q)) i? ϕ i , λ i (b) Robust game automaton A ∆ rob

Definition 15 The robust game automaton

A ∆ rob = ( Loc, q 0 , Clk ∪ {y}, E, Act, Inv) is constructed from A, with an additional clock y, input actions Act i = Act i ∪Act o ,

and output actions Act

o = {τ o! | o! ∈ Act o },
according to the following rules. For each location q ∈ Loc, and for each edge e = (q, o!, ϕ, λ, q ) ∈ E:

• q ∈ Loc, and two locations q α e and q β e are added in Loc. The invariant of q is unchanged; the invariants of q α e and q β e are both y ≤ ∆.

• Each edge e = (q, i?, ϕ, λ, q ) ∈ E gives rise to the following edges in E: (q, i?, ϕ, λ, q ), (q α e , i?, ϕ, λ, q ) and (q β e , i?, ϕ, λ, q ).

• e gives rise to the following edges in E: (q, τ o! , ϕ, {y}, q α e ), (q α e , τ o! , {y = ∆}, {y}, q β e ), (q α e , o!, ϕ∧Inv(q), λ, q ), (q β e , o!, ϕ∧Inv(q), λ, q ), (q α e , o!, ¬(ϕ ∧ Inv(q)), ∅, Bad) and (q β e , o!, ¬(ϕ ∧ Inv(q)), ∅, Bad)

Actions τ o! are considered as silent actions, and consequently they will be concealed from the runs of the automaton.

Technically speaking, since in a TIOA guards must be convex, the two transitions to the Bad location (drawn in red on Fig. 8) may be split into several copies, one for each convex guard in ¬ϕ.

The construction is illustrated in Fig. 8. Intuitively, whenever the output player wants to fire a transition induced by an edge (q, o!, ϕ o , λ o , q 1 ) in the original automaton, from a state (q, u), after elapsing d time units, in the robust automaton the input player is allowed to perturb the timing of this action. Consider the following traces on the robust game automaton that explain the construction.

1. Output proposes to play action o! after a delay d with the following sequence of transitions:

(q, u)

d-∆ ---→(q, u + d -∆) τ o! --→(q α e , u + d -∆) ∆ -→(q α e , u + d) τ o! --→(q β e , u + d)
Note that this forbid output to play any action with a reaction time smaller than ∆. More precisely, any strategy for output found in the robust game automaton A ∆ rob will effectively correspond to a non-zeno strategy in A. 2. Input can perturb this move with d ≤ ∆, such that action o! is performed with either a smaller delay:

(q α e , u + d -∆) d -→(q α e , u + d -∆ + d ) o! -→(q 1 , u + d -∆ + d )
or a greater delay:

(q β e , u + d) d -→(q β e , u + d + d ) o! -→(q 1 , u + d + d )
3. In locations q,q α e and q β e , the original input edge (q, i?, ϕ i , λ i , q 1 ) may still be fired. So while the execution of the output o! is delayed control can be intercepted by an arriving input. 4. If output reaches a state (q α e , u) or (q β e , u), with u |= ϕ o , then input has a winning strategy with one of the following moves: (q α e , u)

o! -→(Bad, u) or (q β e , u) o!
-→(Bad, u), that denote the late firing of action o!.

Let F : R A ∆ rob → Act o ∪ {delay} be a winning symbolic strategy for output in the robust game (A ∆ rob , W o (Bad)). We construct a strategy F rob : R A → Act o ∪ {delay} for the game (A, W o (Bad)) in the following manner. For each (q, r) ∈ R A ,

• F rob ((q, r)) = o! if there exists an edge e ∈ E and a region (q α e , r) ∈ R A ∆ rob , such that r = r |Clk and F ((q α e , r)) = τ o! .

• Otherwise F rob ((q, r)) = delay.

Theorem 1

The robust game automaton is a sound construction to solve robust timed games in the following sense: if F is a winning strategy for output in the game (A ∆ rob , W o (Bad)), then F rob (constructed above) is a ∆-robust winning strategy for output in the game (A, W o (Bad)).

Proof 2 (Theorem 1) We consider the automaton A F rob representing the outcome of applying

F rob to A. We must prove that Runs( A F rob o ∆ sem ) ⊆ W o (Bad), where W o (Bad) = {ρ ∈ Runs( A sem ) | States(ρ) ∩ Bad = ∅}.
First, we map each run ρ of A F rob o ∆ to a run ρ of A. We use an induction on the length of the runs. We assume that the property holds for runs of length i:

if ρ i is a run of Runs( A F rob o ∆ sem ) such that last( ρ i ) = ((q i , r i ), u i ), then there exists a run ρ i in Runs( A sem ), such that last(ρ i ) = (q i , u i ). Let ρ i+1 = ρ i a -→((q i+1 , r i+1 ), u i+1 ).
We prove the inductive step, splitting into cases:

1. If a ∈ Act i , then there exists an edge e = ((q i , r i ), a, ϕ, λ, (q i+1 , r i+1 )) in A F rob . By construction, there also exists an edge e = (q i , a, ϕ, λ, q i+1 ) in A. Since e is firable, u i |= ϕ, and therefore e and e are also firable. So

ρ i+1 = ρ i a -→(q i+1 , u i+1 ) is a run of A. 2. If a ∈ Act o ,
then there exists e = ((q i , r i ), a, ϕ, λ, (q i+1 , r i+1 )) in A F rob and by construction, e = (q i , a, ϕ, λ, q i+1 ) in A. Since e is firable, u i |= ϕ ∆ and u i |= r i ∆ that is the enlarged invariant of (q i , r i ). By construction also F rob ((q i , r i )) = a, which implies that there exists r i such that r i = r i|Clk and F ((

q α i , r i )) = a. Since u i |= r i ∆ , ∃δ ∈ [-∆, ∆]. u i + δ |= r i . Let u i = (u i1 , u i2 , . . . , u in ), then u i + δ = (u i1 + δ, u i2 + δ, .

. . , u in + δ). By definition of the projection this implies that

u iδ = (u i1 + δ, u i2 + δ, . . . , u in + δ, ∆) ∈ r i . Now in the automaton A ∆ rob , F is a winning strategy, which implies that ∀δ ∈ [-∆, ∆]. u iδ + δ |= ϕ ∧ Inv(q i ) (

otherwise input as a spoiling strategy).

This proves that u i |= ϕ ∧ Inv(q i ) and therefore that e is firable. So

ρ i+1 = ρ i a -→(q i+1 , u i+1 ) is a run of A. 3. If a ∈ R ≥0 ,
either the strategy F rob prescribes that output can delay infinitely in ((q i , r i ), u i ). This implies that Inv(q i ) is unbounded, and that proves immediately that ρ i+1 ∈ Runs( A sem ).

Otherwise output has a strategy that eventually performs an action. This is represented by the following sequence of edges in

A F rob : (q i , r i ) τ -→(q i , r i1 ) τ -→(q i , r i2 ) . . . (q i , r in ) o! -→(q i , r i ).
We consider that a is the maximum delay firable from ρ i , thus

ρ i+1 = ρ i a1 -→((q i , r i1 ), u i + a 1 ) τ -→((q i , r i2 ), u i + a 1 ) a2 -→ ((q i , r i2 ), u i + a 1 + a 2 ) τ -→ . . . ((q i , r in ), u i + a) o! -→((q i , r i ), u i )
, such that a = n j=1 a j . Then u i + a |= r in ∆ . and as in the previous case we can prove that u i + a |= ϕ ∧ Inv(q i ). This proves that ρ i+1 ∈ Runs( A sem ).

We now prove that all the states in A F rob o ∆ are safe, by mapping the runs of A F rob with the ones of A ∆ rob . We use another induction on the length on the run. Let assume that ρ i ∈ Runs( A F rob o ∆ sem ) is mapped to a run ρ i ∈ Runs( A ∆ rob sem ), such that if last( ρ i ) = ((q i , r i ), u i ), then last( ρ i ) = (q i , u i ), u i = u i|Clk , and (q i , u i ) is a winning state for the strategy F .

1. Either in ((q i , r i ), u i ) the strategy F rob allows delaying infinitely, and consequently the strategy F allows delaying infinitely in A ∆ rob without reaching an unsafe state. For any delay d ∈ R ≥0 , all the input actions i? firable from a state ((q i , r i ), u i + d) are also firable in (q i , u i + d) since the guards are the same. Therefore, ((q i , r i ),

u i + d) i?
-→((q i+1 , r i+1 ), u i+1 ), and (q i , u i + d) i?

-→(q i+1 , u i+1 ). Additionally, (q i+1 , u i+1 ) is also a winning state, since it is an outcome of the strategy F , and u i+1 = u i+1 , since the same clocks are reset. This proves the induction hypothesis 2. Otherwise, output has a strategy that eventually performs an action o! after a delay a. Let

ρ i+1 = ρ i a -→((q i , r i ), u i + a) o!
-→((q i+1 , r i+1 ), u i+1 ) (concealing τ transitions). This implies that there exists an edge e ∈ A that fires o! in q i+1 , the following edges exists in A ∆ rob : (q i , τ o! , ϕ, λ∪{y}, q α ie ), (q i , τ o! , {y = ∆}, {y}, q β ie ), (q α ie , o!, {y ≤ ∆}, {y}, q i+1 ) and (q β ie , o!, {y ≤ ∆}, {y}, q i+1 ). Since o! is firable in ((q i , r i ), u i + a), this means that F rob ((q i , r i )) = o! and u i + a |= r i ∆ . Then by construction of F rob , F (q α ie , r i ) = τ o! , and

q 0 x ≤ 2 q 1 x ≤ 2 q 2 a! b! (a) Specification S q 0 x ≤ 1 q 1 x ≤ 1 q 2 a! x ≥ 1 b! x ≥ 1 (b) Implementation I
there exists b ∈ R ≥0 s.t. (q i , u i ) b - →(q i , u i + b) (concealing τ o! transitions), and u i + b ∈ r i . Additionally, ∀δ ∈ [-∆, ∆].(q i , u i ) b+δ --→(q i , u i + b + δ) o! -→. This is in particular the case for b + δ = a since a ∈ r i ∆ . Therefore (q i , u i ) a -→ o!
-→(q i+1 , u i+1 ), and (q i+1 , u i+1 ) is winning since it is an outcome of F , and u i+1 = u i+1 , since the same clocks are reset. To finish the induction step, the same argument as in the first case is used to demonstrate that any input action firable from ((q i , r i ), u i ) after some delay d is also firable from (q i , u i ).

This construction shall serve as a tool for deciding robust consistency, synthesizing a robust implementation, and other operations of the specification theory with robustness which are detailed in next section.

Remark on completeness.

The robust game automaton is not a complete technique to solve robust timed games. Indeed, our notion of robustness introduces perturbations on the syntax of the automaton, whereas the robust game automaton modifies the semantics of the game. Therefore there exist specifications that can be robustly implemented, although they will be judged as non robust using the robust game automaton construction. For instance, the specification S in Fig. 9a is 1-robust consistent and it can be robustly implemented with the implementation I in Fig. 9b (the ∆-perturbation I 1 corresponds to the same TIOA as S). But for ∆ = 1 no robust strategy exists in the robust game automaton. Indeed, since clock x is not reset by the edge from q 0 to q 1 , the following run is possible in the semantics of I 1 : (q 0 , 0) [START_REF] Mcaffer | OSGi and Equinox: Creating Highly Modular Java Systems[END_REF]. Therefore in this run action b! must happen immediately. This is not robust according to the robust game automaton, as it cannot be perturbed.

2 -→ I (q 0 , 2) a! -→ I (q 1 , 2) b! -→ I (q 2 ,

Robust Consistency and Robust Compatibility

Robust Consistency

We now provide a method to decide the ∆-robust consistency of a specification and synthesize robust implementations by solving a robust timed safety game, in which the output player must avoid a set of immediate error states. From there, the computation of a robust strategy described in the previous section provides a method to synthesize an implementation of the specification that is robust with respect to outputs enlargement.

To account for input restrictions, we increase the set of error states err S . Intuitively a specification is ∆-robust with respect to input i?, if between enabling of any two i? edges at least 2∆ time passes, during which the reaction to i? is unspecified. So, if the two actions trigger ∆-too-late and ∆-too-early (respectively), there is no risk that the reaction is resolved non-deterministically in the specification.

In our input-enabled setup, lack of reaction is modeled using transitions to the universal (unpredictable) state. Formally, we say that ∆-robust specifications should admit ∆-latency of inputs. A state (q, u) satisfies the ∆-latency condition for inputs, iff for each edge e = (q, i?, ϕ, c, q ), where q = l u and e is enabled in (q, u) we have: q,i?,ϕ,c,q ) if e = e and (q, u) d -→(q, u + d) and e is enabled in (q, u + d) then q = l u Definition 16 For a specification S and ∆ ∈ R ≥0 , the set err S ∆ of error states for ∆-robust consistency is such that (q, u) ∈ err S ∆ iff one the following conditions is verified:

∀d ∈ [0, 2∆]. ∀e = (
• Violates independent progress:

(∃d ∈ R ≥0 . (q, u) d -→) and (∀d.∀o!. (q, u) d -→(q, u + d) ⇒ (q, u + d) o! -→)
• Violates ∆-latency of inputs: ∃e = (q, i?, ϕ, c, q ), with q = l u , enabled in (q, u), such that ∃d ∈ [0, 2∆].(q, u) d -→(q, u + d) and ∃e = (q, i?, ϕ, c, q ) enabled in (q, u + d), with e = e and q = l u .

Observe that err S ⊆ err S ∆ , because the error condition with robustness is weaker than in the classical case (cf. page 13).

The ∆-robust consistency game (S, W o (err S ∆ )) can be solved using the construction of Definition 15. This synthesizes a robust strategy F and its syntactic outcome S F . Then we build the robust implementation I F by applying the following transformation to S F :

• When we apply a ∆-perturbation on I F , a state ((q, r), u) can be reached even if u ∈ r ∨ r . However due to the region partitioning, the inputs edges available in I F might not be firable from r ∨ r . Then, in order to enforce the robust satisfaction relation between (I F ) ∆ and S, we add additional input edges to I F : for each location (q, r) in I F , for each edge e = ((q, r), i?, ϕ, λ, (q * , r * )) (with q * = l u ), and for each location (q , r ) that can be reach from (q, r) by a sequence of τ transitions, we add an edge e = ((q , r ), i?, ϕ, λ, (q * , r * )).

• To support restriction of input guards in (I F ) ∆ , we replaced in I F all guards ϕ of edges e = ((q, r), i?, ϕ, λ, (q , r )) with q = l u by their enlargement ϕ ∆ . Guards on edges to the l u location are adjusted in order to maintain action determinism and input-enableness.

Note that this construction adds many input edges to the implementation, out of which many are never enabled. This simplifies the construction and the proof of correctness. In practice, to efficiently synthesize implementations, coarser abstractions like zones should be used that do not include τ transitions, thus avoiding the multiplication of input edges.

Theorem 2 Let S be a specification. If F is a robust winning strategy in the ∆-robust consistency game, then I F sat ∆ S and S is ∆-robust consistent.

Proof 3 (Theorem 2) S is ∆-robust consistent if it admits a ∆-robust implementation. I F satisfies the independent progress condition since it corresponds to the outcome of the strategy F that avoids the inconsistent states in S. For the same reason it also verifies the ∆-latency condition, which permits to increase guards on input edges without adding non-determinism. Since F is a symbolic strategy it may authorize small delays in the regions where an output action must be fired, and therefore I F may not be output urgent. However, any point in these regions can be freely chosen to concretely implement I F We check now that I F sat ∆ S with the following relation

R = {(((q, r), u), (q, u)) ∈ (I F ) ∆ sem × S sem }
Note that since F is a robust winning strategy, the runs of S F o ∆ (and by construction the ones of (I F ) ∆ ) also belong to S. Finally we assume that S can accept τ transitions in any state as output transitions. Let consider (((q, r), u), (q, u)) ∈ R:

1. If ((q, r), u) d -→ (I F ) ∆ ((q, r), u + d) for some d ∈ R ≥0 , then since the runs of (I F ) ∆ are included into the ones of S, it is also the case that (q, u) d -→ S (q, u+ d).

If ((q, r), u)

o! -→ (I F ) ∆ ((q , r ), u ) for some o! ∈ Act o , then there exists an edge ((q, r), o!, ϕ, λ, (q , r )) in I F and also in S F . It also means that there exists a similar edge (q, o!, ϕ, λ, q ) in S. And since the runs of (I F ) ∆ are included into the ones of S, it implies that (q, u)

o! -→ S (q , u ). 3. If ((q, r), u) τ -→ (I F ) ∆ ((q, r ), u) then by assumption (q, u) τ -→ S (q, u). 4. If (q, u) i?
-→ S (q , u ) for some i? ∈ Act i , then there exists an edge e = (q, i?, ϕ, λ, q ) such that u |= ϕ. There also exists an edge (q, [u])

i? -→ G (q , [u ])
in the region graph of S. If u ∈ r then this edge also exists in I F . Otherwise u ∈ r ∨ r ∆ . This means that there exists a sequence of τ transitions in I F between r and [u], and by construction the input edge is copied in each location along this sequence, including (q, r). u |= ϕ implies that u |= ϕ ∆ ∆ , which proves that it is firable. Therefore ((q, r), u) i?

-→ I ∆ ((q , [u ]), u ).

Conjunction

A conjunction of two specifications captures the intersection of their implementation sets. The following conjunction operator has been proposed in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]:

Definition 17 Let S = (Loc S , q S 0 , Clk S , E S , Act, Inv S ) and T = (Loc T , q T 0 , Clk T , E T , Act, Inv T ) be specifications that share the same alphabet of actions Act. We define their conjunction, denoted S ∧ T , as the TIOA (Loc, q 0 , Clk, E,Act, Inv) where Loc = Loc S ×Loc T , q 0 = (q S 0 , q T 0 ), Clk = Clk S Clk T , Inv((q s , q t )) = Inv(q s )∧Inv(q t ), and the set of edges is defined according to the following rule: ((q s , q t ), a, ϕ s ∧ϕ t , λ s ∪ λ t , (q s , q t )) ∈ E iff (q s , a, ϕ s , λ s , q s ) ∈ E S and (q t , a, ϕ t , λ t , q t ) ∈ E T It turns out that this operator is robust, in the sense of precisely characterizing also the intersection of the sets of robust implementations. So not only conjunction is the greatest lower bound with respect to implementation semantics, but also with respect to the robust implementation semantics. More precisely: Theorem 3 For specifications S, T and ∆ ∈ Q >0 :

S ∧T ∆ mod = S ∆ mod ∩ T ∆ mod Proof 4
The theorem is a direct extension of Theorem 6 in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], but now for robust implementations. By definition of the robust implementation,

I ∈ S ∧T ∆ mod ⇔ I ∆ ≤ S ∧ T
According to Theorem 6 in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], items 1 and 2,

I ∆ ≤ S ∧ T ⇔ I ∆ ≤ S ∧ I ∆ ≤ T
And the last terms correspond to the definition of robust implementations.

We remark that due to the monotonicity of the refinement (Property 1), we can use two different delays ∆ 1 and ∆ 2 , such that:

S ∆1 mod ∩ T ∆2 mod ⊇ S ∧T max(∆1,∆2) mod
So requirements with different precision can be conjoined, by considering the smaller jitter. Robustness of the operator in Def. 17 is very fortunate. Thanks to this, large parts of implementation of theory of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] can be reused.

Parallel Composition and Robust Compatibility

Composition is used to build systems from smaller units. Two specifications S, T can be composed only iff Act S o ∩ Act T o = ∅. Parallel composition is obtained in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] by a product, where the inputs of one specification synchronize with the outputs of the other: Definition 18 Let S = (Loc S , q S 0 , Clk S , E S , Act S , Inv S ) and T = (Loc T , q T 0 , Clk T , E T , Act T , Inv T ) be two composable specifications. We define their parallel composition, denoted S T , as the TIOA (Loc, q 0 , Clk, E,

= Loc S × Loc T , q 0 = (q S 0 , q T 0 ), Clk = Clk S Clk T , Act = Act o ∪ Act i with Act o = Act S o Act T o and Act i = (Act S i \ Act T o ) ∪ (Act T i \ Act S o )
, Inv(q s , q t ) = Inv(q s )∧Inv(q t ), and the set of edges is defined by the three following rules:

• Let a ∈ Act S \Act T , for each q t ∈ Loc T , ((q s , q t ), a, ϕ s , λ s , (q s , q t )) ∈ E, iff (q s , a, ϕ s , λ s , q s ) ∈ E S .

• Let a ∈ Act T \Act S , for each q s ∈ Loc S , ((q s , q t ), a, ϕ t , λ t , (q s , q t )) ∈ E, iff (q t , a, ϕ t , λ t , q t ) ∈ E T .

• Let a ∈ Act S ∩ Act T , ((q s , q t ), a, ϕ s ∧ ϕ t , λ s ∪ λ t , (q s , q t )) ∈ E iff (q s , a, ϕ s , λ s , q s ) ∈ E S and (q t , a, ϕ t , λ t , q t ) ∈ E T .

We also recall the definition of the parallel product for two TIOTS S = (St S , s 0 , Σ S , → S ) and T = (St T , t 0 , Σ T , → T ). S ⊗ T = (St S × St T , (s 0 , t 0 ), Σ S⊗T , → S⊗T ), such that:

s a -→ S s a ∈ Σ S \Σ T (s, t) a -→ S⊗T (s , t) indep-l t a -→ T t a ∈ Σ T \Σ S (s, t) a -→ S⊗T (s, t ) indep-r s a -→ S s t a -→ T t a ∈ R ≥0 ∪ Σ S⊗T i ∪ (Σ S i ∩ Σ T o ) ∪ (Σ S o ∩ Σ T i ) (s, t) a -→ S⊗T (s , t ) sync Example 6
The two timed specifications in Fig. 1a and 1b can be composed together by synchronizing the outputs cof and tea of the Machine with the inputs of the Researcher. The resulting TIOA is a timed specification whose input is coin and outputs are pub, cof and tea. This composition scheme is illustrated in the diagram of Fig. 10.

In the input-enableness setting we model incompatibility by introducing a predicate describing undesirable states, here denoted by a set und. It should in general contain the universal location l u . For example, a communication failure can be modeled by redirecting an input edge to an undesirable location. In general any reachability objective, for example given by a temporal logic property, can serve as the set of undesirable behaviors und. It is important that such behaviors are avoided during the composition. For doing so, we propose to follow the optimistic approach to composition introduced in [START_REF] De Alfaro | Interface automata[END_REF] that is two specifications can be composed if there exists at least one environment in which they can work together. In the robustness setting we consider imprecise environments by applying a ∆-perturbation to their outputs. Then, in what follows, we say that a specification is ∆-robust useful if there exists an imprecise environment E that avoids the undesirable states, whatever the specification does.

Definition 19 A specification S is ∆-robust useful if there exists an environment E such that no undesirable states are reached in

E o ∆ S sem .
Remark that, contrary to robust implementations, we only apply a pertubation to the outputs of the environment. Indeed since the environment is a complement of the system, its inputs correspond to the output of the system, and therefore they are not perturbed to achieve robust compatibility.

Property 4 (Monotonicity)

Given ∆ 1 ≤ ∆ 2 , if S be a ∆ 2 -robust useful specification, then S is ∆ 1 -robust useful. Proof 5 (Property 4) If S is ∆ 2 -robust useful this means that there exists an environment E such that no undesirable states is reached in E o ∆2 S sem . Then for ∆ 1 ≤ ∆ 2 , E o ∆1 sem ⊆ E o ∆2 sem . This implies that E o ∆1 S sem ⊆ E o ∆2
S sem , which proves that S is also ∆ 1 -robust useful.

To check robust usefulness we solve the robust game (S, W i (und)), and determine if the input player has a robust strategy F that avoids the undesirable states. Let S F be the syntactic outcome of F in S. We build from S F a robust environment E F by permuting the input and output players, such that each input in S F becomes an output, and conversely. Finally, two specifications are compatible if their composition is useful.

Definition 20 Two composable specifications S and T are ∆-robust compatible if and only if S T is ∆-robust useful.

We now study the impact of adding ∆-perturbations introduced in previous section over parallel composition. It is important that the robust theory does not modify the definition of the operations themselves. This means that all the important properties of composition introduced in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] remain valid. Moreover, robustness distributes over parallel composition in the following fashion: Lemma 1 For any implementations I, J and a delay ∆ ∈ Q >0 :

(I J ) ∆ ≤ I ∆ J ∆ Proof 7 (Lemma 1)
In the following, we denote by (Loc k , q k 0 , Clk k , E k , Act k , Inv k ), with k ∈ {I, J, I J}, the TIOAs corresponding to I, J , or I J , respectively, and by (St k , (q k 0 , 0), Act k , → k ), with k ∈ {I, J, I J}, their semantics, and with k ∈ {I ∆ , J ∆ , [I J] ∆ }, their perturbed semantics. First let recall Theorem 11 from [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] that states that I ∆ J ∆ sem = I ∆ sem ⊗ I ∆ sem . Then we need to prove the refinement (I J ) ∆ sem ≤ I ∆ sem ⊗ J ∆ sem by witnessing the following relation:

R = (q i , q j ), u ij , ( q i , u i ), ( q j , u j ) ∈ St [I J] ∆ × (St I ∆ × St J ∆ ) | (q i = q i ∧ u i = u ij|Clk I ) ∨ q i = l u ∧ (q j = q j ∧ u j = u ij|Clk J ) ∨ q j = l u }
We prove by coinduction that R is a timed alternating relation. Let (q i , q j ), u ij , ( q i , u i ), ( q j , u j ) ∈ R.

1. If (q i , q j ), u ij d -→ [I J] ∆ (q i , q j ), u ij + d for some d ∈ R ≥0
, then by definition u ij |= Inv(q i , q j ) ∆ . By construction of the parallel composition Inv(q i , q j ) ∆ = Inv(q i ) ∧ Inv(q j ) ∆ = Inv(q i ) ∆ ∧ Inv(q j ) ∆ . Then, we can deduce that u i + d |= Inv(q i ) ∆ and u j + d |= Inv(q j ) ∆ . This implies that (q i , u i )

d -→ I ∆ (q i , u i + d) and (q j , u j ) d -→ J ∆ (q j , u j + d).
Besides, by definition of the universal state, for any valuation u of a TIOA is always true that (l u , u)

d -→(l u , u + d).
By definition of the sync rule from I ∆ sem ⊗ J ∆ sem ,

( q i , u i ), ( q j , u j ) d -→ I ∆ ⊗J ∆ ( q i , u i + d), ( q j , u j + d)
and the relation R is trivially preserved in the next states.

2. If (q i , q j ), u ij o! -→ [I J] ∆ (q i , q j ), u ij , then ∃e ∈ E I J .e = ((q i , q j ), o!, ϕ, c, (q i , q j )) such that u ij |= ϕ ∆ and u ij |= Inv(q i , q j ) ∆ , (a) And if o ∈ Act I o \Act J i (or conversely, if o ∈ Act J o \Act I i ;
this case is similar, so we will not consider it), then ∃e i ∈ E I . e i = (q i , o!, ϕ i , c i , q i ), and q j = q j , ϕ = ϕ i , c = c i , and u ij|Clk J = u j . Consequently,

u i |= ϕ i ∆ and u i = u ij|Clk I |= Inv(q i ) ∆ , which proves that (q i , u i ) o! -→ I ∆ (q i , u i ). Besides, by definition of the universal state, (l u , u i ) o! -→ I ∆ (l u , u i ).
Then, according to the indep-l rule, ( q i , u i ), ( q j , u j ) o! -→ I ∆ ⊗J ∆ ( q i , u i ), ( q j , u j ) . Moreover, either q i = q i and then q i = q i , or q i = l u = q i , which proves that the relation R is preserved.

(b) If o ∈ Act I o ∩ Act J i (the reverse case o ∈ Act J o ∩ Act I i is similar)
, then ∃e i ∈ E I . e i = (q i , o?, ϕ i , c i , q i ) and ∃e j ∈ E J . e j = (q j , o!, ϕ j , c j , q j ) and ϕ = ϕ i ∧ ϕ j , c = c i ∪ c j . On the side of I, since u ij |= ϕ ∆ and u ij |= Inv(q i , q j ) ∆ , we get that

u i |= ϕ i ∆ and u i = u ij|Clk I |= Inv(q i ) ∆ , which implies that (q i , u i ) o! -→ I ∆ (q i , u i ).
On the side of J , we also get that u j |= ϕ j ∆ and u j |= Inv(q j ) ∆ . If moreover u j |= ϕ j ∆ , then as previously it implies that (q j , u j ) o? -→ J ∆ (q j , u j ). Otherwise, a reductio ab absurdum argument allows us to prove that there exists no other edge e j = (q j , o?, ϕ j , c j , q j ) ∈ E J such that u j |= ϕ j ∆ (since u j |= ϕ j ∆ it implies that ∃ε ∈ [-∆, ∆].u j + ε |= ϕ j , but in the same time it would be the case that u j + ε |= ϕ j . This is a contradiction since J, as an implementation is supposed to be deterministic). However, by construction of J ∆ sem , inputenableness is preserved by linking the unexpected input to a universal location l u . So (q j , u j ) o? -→ J ∆ (l u , u j ). Then, according to the sync rule, ( q i , u i ), ( q j , u j ) o! -→ I ∆ ⊗J ∆ ( q i , u i ), ( q j , u j ) , and as previously, by construction we check that the relation is preserved.

3. Finally, if ( q i , u i ), ( q j , u j ) i? -→ I ∆ ⊗J ∆ ( q i , u i ), ( q j , u j ) , for i ∈ Act I i ∩ Act J i (the cases i ∈ Act I i \Act J i or i ∈ Act J i \Act I
i can be proved similarly by considering that only one component reacts, while the other stay in the same state), then from the definition of the composition:

• ( q i , u i ) i?

-→ I ( q i , u i ), and • ( q j , u j ) i? -→ J ( q j , u j ).

Besides, due to input-enableness, (q i , q j ), u ij i?

-→ [I J] ∆ (q i , q j ), u ij + d , which implies that:

• (q i , u i ) i?

-→ I (q i , u i ), with u i = u ij|Clk I , and

• (q j , u j ) i?
-→ J (q j , u j ), with u j = u ij|Clk J .

If q i = l u then q i = l u , and in this case the relation R is always preserved (and similarly for q j ). Otherwise q i = q i and u i = u i (and similarly for q j ). In this latter case, since I ∆ sem is deterministic, it implies that q i = q i and u i = u i , which also proves the induction for relation R.

Finally, we show in Theorem 5 that the independent implementability property of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] can be extended to robust implementability, which follows from Lemma 1 and Theorem 10 in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF].

Theorem 5 Let S and T be composable specifications and let I and J be ∆robust implementations of S and T (resp.), i.e. I sat ∆ S and J sat ∆ S. Then I J sat ∆ S T . Moreover if S and T are ∆-compatible then I and J are also ∆-compatible.

Proof 8 (Theorem 5)

The first part of the theorem is deduced from previous results:

• Due to lemma 1, (I J ) ∆ sem ≤ I ∆ sem ⊗ J ∆ sem .

• Then, Theorem 10 from [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] proves that refinement is a pre-congruence with respect to parallel composition: if S 1 ≤ S 2 and T is composable with S 1 , then S 1 ⊗ T ≤ S 2 ⊗ T . Observe that since S and T are composable, so are I and J , and their semantics. Thus we can apply it twice:

I ∆ sem ≤ S sem ⇒ I ∆ sem ⊗ J ∆ sem ≤ S sem ⊗ J ∆ sem , and
J ∆ sem ≤ T sem ⇒ S sem ⊗ J ∆ sem ≤ S sem ⊗ T sem .
• Finally Theorem 11 in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] allows to lift the result to the composition of TIOA specifications: S sem ⊗ T sem = S T sem .

Due to the transitivity of the refinement, we can concatenate the previous results, which proves that (I J ) ∆ sem ≤ S T sem , and therefore I J sat ∆ S T . We now prove the second part of the theorem. Since S and T are ∆-compatible, there exists an environment E such that E o ∆ (S T ) avoids reaching any undesirable states. From Theorems 10 and 11 in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], we get that I J ≤ S T . Again with Theorem 10 we get that (I J )

E o ∆ ≤ (S T ) E o ∆ .
Consequently, since no undesirable states are reached in (S T )

E o ∆ this is also the case in (I J ) E o ∆ , which proves that I J is ∆-useful and so I and J are ∆-compatible.

Additionally, due to the monotonicity of perturbations with respect to the refinement, two different delays can be used to implement specifications S and T . For two implementations I sat ∆1 S and J sat ∆2 T of the parallel components, their composition satisfies the composition of specifications with the smaller of the two precisions:

I J sat min(∆1,∆2) S T

Quotient

Quotient is a dual operator to composition, such that for two specifications T and S, T S is the specification of the components that composed with S will refine T . In other words, if T is the specification of a system, and S the specification of a subsystem, T S specifies the component that still needs to be implemented after having an implementation of S, in order to build an implementation of T . One possible application is when T is a system specification, and S is the plant, then a robust controller for a safety objective can be achieved by finding a ∆-consistent implementation of the quotient T S.

To apply quotienting, we require that Act S ⊆ Act T and Act S o ⊆ Act T o . The construction of a quotient requires the use of a universal location l u , as well as an inconsistent location l ∅ that forbids any outputs and forbids elapsing of time.

Definition 21 Let S = (Loc S , q S 0 , Clk S , E S , Act S , Inv S ) and T = (Loc T , q T 0 , Clk T , E T , Act T , Inv T ) be two specifications, with Act S ⊆ Act T and Act S o ⊆ Act T o .

Their quotient, denoted T S, is the TIOA (Loc, q 0 , Clk, E, Act, Inv) where Loc = Loc T × Loc S ∪ {l u , l ∅ }, q 0 = (q T 0 , q S 0 ),

Clk = Clk T Clk S {x new }, Act = Act i Act o with Act i = Act T i ∪ Act S o ∪ {i new } and Act o = Act T o \ Act S
o , Inv(q t , q s ) = Inv(l u ) = true and Inv(l ∅ ) = {x new ≤ 0}, and the set E of edges is defined by the following rules:

• ((q t , q s ), a, ¬Inv S (q s ), {x new }, l u ) ∈ E iff q t ∈ Loc T , q s ∈ Loc S , a ∈ Act.

• ((q t , q s ), i new , ¬Inv(q t ) ∧ Inv(q s ), {x new }, l ∅ ) ∈ E iff q t ∈ Loc T , q s ∈ Loc S .

• ((q t , q s ), a, ϕ T ∧ ϕ S , λ t ∪ λ s , (q t , q s )) ∈ E iff (q t , a, ϕ t , λ t , q t ) ∈ E T and (q s , a, ϕ s , λ s , q s ) ∈ E S .

• Let a ∈ Act S o and G T = {ϕ t | (q t , a, ϕ t , λ t , q t ) ∈ E T }, ((q t , q s ), a, ϕ S ∧ ¬G T , {x new }, l ∅ ) ∈ E iff (q s , a, ϕ s , λ s , q s ) ∈ E S .

• Let a ∈ Act S , ((q t , q s ), a, ϕ T , λ t , (q t , q s )) ∈ E iff ∀(q t , a, ϕ t , λ t , q t ) ∈ E T .

• Let a ∈ Act S o and G S = {ϕ s | (q s , a, ϕ s , λ s , q s ) ∈ E S }, ((q t , q s ), a, ¬G S , {}, l u ) ∈ E iff (q t , a, ϕ t , λ t , q t ) ∈ E T .

• (l ∅ , a, x new = 0, ∅, l ∅ ) ∈ E iff a ∈ Act i . • (l u , a, true, ∅, l u ) ∈ E iff a ∈ Act.
As stated in Theorem 12 of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], the quotient gives a maximal (the weakest) specification for a missing component. This theorem can be generalized to specifications that are locally consistent (see [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]), and used to argue for completeness of the quotient construction in the robust case. It turns out that this very operator is also maximal for the specification of a robust missing component, in the following sense: Theorem 6 Let S and T be two specifications such that the quotient T S is defined and let J be an implementation, then:

S J ∆ ≤ T iff J sat ∆ T S
Proof 9 (Theorem 6) First let remark that J ∆ is a locally consistent specification, as defined in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]. Then, we can apply Theorem 12 of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] to J ∆ which proves:

S J ∆ ≤ T iff J ∆ ≤ T S
According to the definition of ∆-robust satisfaction this proves the theorem.

Counter Strategy Refinement For Parametric Robustness

In the previous sections we define and solve robustness problems for a fixed delay, and we study the properties of these perturbations with respect to the different operators in the specification theory. Now we will propose a technique that evaluates the greatest possible value of the perturbation. We follow a counterexample refinement approach, a technique used for automatic abstraction refinement in [START_REF] Clarke | Counterexampleguided abstraction refinement[END_REF]. In our setting counterexamples are spoiling strategies computed for a given value of the perturbation. We replay these strategies on a parametric model of the robust game in order to refine the value of the perturbation.

The robustness problems that we consider in this sections are the parametric extension of the previously defined problems:

Robust Consistency. Given a specification S, determine the greatest value of ∆ such that S is ∆-robust consistent.

Robust Usefulness. Given a specification S, determine the greatest value of ∆ such that S is ∆-robust useful.

Parametric Timed Games

When we consider ∆ as a free parameter, the robust game automaton construction of Section 4 defines a Parametric Timed I/O Automata, in a similar manner as Parametric Timed Automata are defined in [START_REF] Alur | Parametric real-time reasoning[END_REF][START_REF] Hune | Linear parametric model checking of timed automata[END_REF]. We If A is a parametric TIOA and W o (Bad) is a safety objectives, then (A, W o (Bad)) is parametric timed game. For a given value δ ∈ Q of the parameter, we define the non-parametric TIOA A δ obtained by replacing each occurrence of the parameter ∆ in the parametric guards of A by the value δ.

A parametric symbolic state X is a set of triples (q, u, δ), where δ is a valuation of the parameter ∆ and (q, u) is a state in A δ sem . Operations on symbolic states can be extended to parametric symbolic states, such that X P , X P ,PPost a (X), PPred a (X) and PPred t (X, Y ) stands for the extensions of previously defined non-parametric operations. Formally: 1. either a ∈ Act i and ∃Z .F i ((q, Z )) = a and (q , Z ) = Post a ((q, Z ∩ Z )) Fi , 2. or a ∈ Act o and ∃Z .F i ((q, Z )) = delay and (q , Z ) = Post a ((q, Z ∩ Z )) Fi ,

X P ={(q, u + d, δ) | (q, u, δ) ∈ X, d ∈ R ≥0 } X P ={(q, u -d, δ) | (q, u, δ) ∈ X, d ∈ R ≥0 } PPost a (X) ={(q , u , δ) | ∃(q, u, δ) ∈ X. (q, u) a -→ A δ (q , u )} PPred a (X) ={(q, u, δ) | ∃(q , u , δ) ∈ X. (q, u) a -→ A δ (q , u )} PPred t (X, Y ) ={(q, u, δ) | ∃d ∈ R ≥0 . (q, u) d -→ A δ (q, u + d) and (q, u + d) ∈ X and ∀d ∈ [0, d]. (q, u + d , δ) ∈ Y }
for X = (q, Z) ∈ Z ∆ bad A do 3 if q ∈ Bad then 4 P W in[X] ← (q, Inv(q) ) 5 W aiting ← W aiting ∪ {Y | ∃ρ. ρ-→Y - →X ∈ Outcome(F i )} 6 else 7 P W in[X] ← ∅ 8 end 9 end 10 /* Backward exploration */ while (W aiting = ∅) ∧ (q 0 , 0) ∈ P W in[X 0 ]) do 11 X = (q, Z) ← pop(W aiting) 12 P Bad * ← (q, ¬ Inv(q) ) ∪ ( X a∈Act i ----→Y PPred a (W in[Y ])) 13 P Good * ← X a∈Acto -----→Y PPred a ((q, Inv(q) ) \ P W in[Y ]) 14 P W in[X] ←
The backward exploration ends when the set of winning states P W in[X 0 ] contains the initial state. Then, the projection (P W in[X 0 ] ∩ (q 0 , 0)) |∆ computes the set of all the valuations of ∆ such that the strategy F i is winning. The algorithm returns the infimum of these valuations.

Theorem 7 (Soundness) Algorithm 2 returns a value

∆ inf ∈ Q such that ∀∆ > ∆ inf the game (A ∆ rob , W o (Bad)) is lost.
Proof 10 (Theorem 7) Given a value ∆ ∈ Q, Algorithm 2 is similar to the timed games algorithm of TIGA described in [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF], but with less exploration steps since only the outcome of the spoiling strategy are explored. Therefore for that value

P W in[X 0 ] ⊆ W in[X 0 ].
By assumption, the game

(A ∆ bad rob , W o (Bad)) is lost, so ∆ bad ∈ (P W in[X 0 ] ∩ (q 0 , 0)) |∆ . Ab absurdo, if ∆ > ∆ inf is a good value, i.e. (A ∆ rob , W o (Bad)
) is winning, then (q 0 , 0) ∈ W in[X 0 ], and consequently (q 0 , 0) ∈ P W in[X 0 ]. This implies that (P W in[X 0 ] ∩ (q 0 , 0)) |∆ = ∅, which is a contradiction.

Theorem 7 ensures that RefineValues preserves the invariants of Algorithm 1.

Implementation and experiments

PyECDAR implementation

The specification theory described in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] is implemented in the tool EC-DAR [START_REF] David | ECDAR: An environment for compositional design and analysis of real time systems[END_REF]. In order to experiment with the methods proposed in the present paper, we have built a prototype tool in Python that reimplements the main functionalities of ECDAR and supports the analyses of the robustness of timed specifications [START_REF]Python implementation of ECDAR[END_REF]. Inside this tool, the theory presented in Sections 4 and 5 is implemented as a set of model transformations:

1. Computation of I ∆ , the ∆-perturbation of an implementation I for some ∆ ∈ Q ≥0 . 2. Computation of the robust game automaton A ∆ rob . 3. In order to add rational perturbations on the models I ∆ and A ∆ rob the tool scales all the constants in the TIOA. 4. Finally we transform the TIOA of a specification into a specific consistency game automaton (resp. usefulness game automaton), such that all non ∆-robust consistent (resp. non ∆-robust useful) states are observed by a single location.

By combining these transformations we can check in the tool the three problems: ∆-robust satisfaction, ∆-consistency and ∆-usefulness. The algorithms used are respectively the alternating simulation algorithm presented in [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] and the on-the-fly timed game algorithm presented in [START_REF] Bulychev | Efficient on-the-fly algorithm for checking alternating timed simulation[END_REF].

To solve the parametric robustness problems we have implemented the heuristic presented in Section 6 that approximates the maximum solution through a counter strategy refinement, and we have implemented a binary search heuristic to compare the efficiency. In the algorithm 2 operations on parametric symbolic states are handled with the Parma Polyhedra Library [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF]. We shall remark that using polyhedra increases the complexity of computations compared to Difference Bound Matrices (DBMs), but this is necessary due to the form of the parametric constraints that are beyond the scope of classical DBMs. This is not such a problem in our approach as parametric analysis is limited to spoiling strategies whose size is kept as small as possible. Nevertheless an interesting improvement can be to use Parametric DBMs as presented in [START_REF] Hune | Linear parametric model checking of timed automata[END_REF].

Experiments

We evaluate the performance of the tool to solve the parametric robustness problems on two examples. We compare in these experiments the Counter strategy Refinement (CR) approach with the Binary Search (BS) method. We presents benchmarks results for different values of the initial parameters ∆ init and .

Specification of a university. The toy examples featured in this paper are extracted from [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]. They are part of an overall specification of a university, composed by three specifications: the coffee machine (M) of Fig. 1a, the researcher (R) of Fig. 1b, and the Administration (A) (see [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]). We study the robust consistency and the robust compatibility of these specifications and their parallel composition. The results are presented in Tables 1 and2. The column game size displays the size of the robust game automaton used in the analysis in terms of locations (loc.) and edges. The next columns display the time spent to compute the maximum perturbation with different initial conditions. The analysis of these results first shows that the Counter strategy Refinement method is not sensitive to the values of the two initial parameters ∆ init and . This is not the case for Binary Search: the precision determines the number of games that must be solved, and the choice of ∆ init change the proportion of games that are winning. Comparing the results of the two methods shows that for most of the cases, especially the more complex one, the Counter strategy Refinement approach is more efficient. 3. Like in previous experiment, the results show that the Counter strategy Refinement method is not sensitive to the initial conditions and in general more efficient than Binary Search.

Specification of a Milner

Interpretation

Previous results are summarized in Fig. 11 in order to compare the performance of the two methods on the most complex examples.

The performance of the Binary Search method depends on the number of games that are solved and on the outcome of these games. Games that are winning (or games that are losing but with a value of ∆ close to the optimum value) are harder to solve, since in these cases the (almost) complete symbolic state space must be explored. Reducing the precision parameter implies that more games must be solved close to the optimum value, and therefore it increases the time of analysis. Moreover, changing, even slightly, the initial maximum value ∆ init may change the number of games, but most important the outcome of these games, and therefore the proportion of winning games. For instance in the last experiment, the expected result is 7.5. With an initial value of 30 the bisections performed by the Binary Search method arbitrarily imply that only 1 game is winning out of 9 (for = 0.1). With 31 this proportion is 6 out of 9, which increases the complexity of the analysis. With the Counter strategy Refinement approach proposed in this paper only losing games are solved until one is winning. The choice of ∆ init modifies the number of games that are solved, but in general the first games for large values of ∆ are easily solved. Consequently, the choice of ∆ init shows in the experiments almost no impact on the performances. With the parametric approach the parameter is only used when the value ∆ min computed by the refinement process is the minimum of the bad values. In that case, the next iteration solves the game with the value ∆ min -. The experiments shows this has no impact on the performances.

Parking controller

In this final case study we analyze the robustness of a parking controller. This component is part of parking system, described in [START_REF] Raclet | Contracts for the Design of Embedded Systems Part I: Methodology and Use Cases[END_REF], that model the behavior of a car park. The system is composed by an entry gate, an exit gate, a gate controller and a payment machine. We study the implementation of the gate controller whose task is to deliver entry tickets, whenever they are requested, and as long as the parking is not full. The specification Controller of this components is given in Figure 12 for a capacity N max of cars in the parking. It specifies that tickets must be delivered at most 10 time units after accepting a request and the request is accepted only if the parking is not full. It also specifies some assumptions about the environment by linking the unexpected behaviors to a universal location l u . These assumptions are that a vehicle may exit only when the parking is not empty, that it may enter only after receiving its entry tickets, and that tickets may be requested at least 6 time units after the previous one has been delivered.

We study the robust consistency of this specification in order to determine if we can implement it. The results are given in Table 4. For an increasing number N max of vehicles we list the maximum allowed perturbation ∆ max , and the time needed to compute it with two values of precision for each methods. The results show that the robustness of the specification decreases when the capacity of the parking increases. We also remark that the counterexample refinement method is less efficient than binary search to analyze this model. Indeed on this model the counterexample refinement method requires more games to determine that value of ∆ max .

This low robustness can be a problem to implement the controller for large number of vehicles. We can analyze spoiling strategies to find that the responsible executions involve a large number of vehicle exiting the parking within the short time interval before the entry ticket is issued. However this is unrealistic and therefore we propose to fix the model. We add an assumption on the environment that limits the number of vehicles that can exit within a given time interval. This assumption is specified in a new specification Assumption shown in Figure 13. It allows any behaviors, but, when a vehicle exit less than 10 time units before the previous one, it goes to the universal location. We add this assumption in conjunction with the controller specification. We analyse the robustness of the new specification Controller ∧ Assumption, and, as previously, we list the results in Table 5

Concluding Remarks

We have presented a compositional framework for reasoning about robustness of timed I/O specifications. Our theory builds on the results presented in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] combined together with a new robust timed game for robust specification theories. It can be used to synthesize an implementation that is robust with respect to a given specification, and to combine or compare specifications in a robust manner. In our approach, robustness is achieved through syntactic transformations, which allows reusing classical analysis technique and tools. In particular we extend the construction of [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] to the setting of specification theories, to solve robust games by reducing them to problems on classical timed games.

As a new contribution from [START_REF] Larsen | Robust specification of real time components[END_REF], we also study the parametric robustness problems and evaluate the maximum imprecision allowed by specifications. To this end we propose a counter example refinement approach that analyzes spoiling strategies in timed games. These contributions have been implemented in a prototype tool that has been used to evaluate the performances of our counter strategy refinement approach.

We have focused in this paper on solving robust consistency and robust compatibility problems. This provides a constructive approach to synthesize robust implementations. In a future version of our tool we would like to apply the counter example refinement approach on the alternating simulation game, in order to solve the parametric satisfaction problem for an existing implementation.

In future we plan to extend our approach to different models, like timed automata with stochastic semantics [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF]. In this context we could give a stochastic definition of robustness that would allow a more expressive quantitative analysis than the worst case scenario used in this paper.

Figure 1 :Figure 2 :

 12 Figure 1: Timed specifications with timed I/O automata

•

  time determinism: whenever s d -→ S s and s d -→ S s then s = s • time reflexivity: s 0 -→ S s for all s ∈ St S • time additivity: for all s, s ∈ St S and all d 1 , d 2 ∈ R ≥0 we have s d1+d2 ----→ S s iff s d1 -→ S s and s d2 -→ S s for s ∈ St S

Example 2

 2 In the example of Fig. 1b a possible run starting from initial locationIdle is (Idle, (0))cof?

Figure 3 :

 3 Figure 3: Implementation for a researcher

Figure 4 :

 4 Figure 4: Refinement between specifications: T ≤ S, but U S

Definition 5 (

 5 Satisfaction) An implementation I satisfies a specification S, denoted I sat S, iff I sem ≤ S sem . We write S mod for the set of all implementations of S: S mod = {I | I sat S and I is an implementation} Definition 6 A specification S is consistent iff there exists an implementation I such that I sat S.

•

  Whenever f o (s) = delay then s d -→s for some d > 0 and state s , and f o (s ) = delay.

Figure 5 :

 5 Figure 5: Consistent specification with error states

Figure 6 :

 6 Figure 6: Illustration of the ∆-perturbation of an implementation I by ∆ = 1.

Figure 7 :

 7 Figure 7: ∆-perturbation of the researcher implementation.

Figure 8 :

 8 Figure 8: Illustration of the construction of the robust game automaton A ∆rob , from an automaton A, with one location q and incident edges e = (q, o!, ϕ o , λ o , q 1 ) and (q, i?, ϕ i , λ i , q 2 ).

Figure 9 :

 9 Figure 9: Specification with 1-robust implementation, but with no robust strategy in the robust game automaton.

Figure 10 :

 10 Figure 10: Diagram for the parallel composition of a coffee machine and a researcher

Theorem 4 Proof 6 (Theorem 4 )

 464 Let S be a specification. If F is a robust winning strategy in the ∆-robust usefulness game, then S is ∆-robust useful in the environment E F . The theorem directly follows from the definition of the robust strategy. S F i ∆ sem ⊆ S sem which implies that E F o ∆ synchronizes with every action of S in their parallel composition. Therefore, only the states belonging to S F i ∆ sem can be reached in the composition, and by definition they are not undesirable.

  denote by B ∆ (Clk) the set of parametric guards with parameter ∆ over a set of clocks Clk. Parametric guards in B ∆ (Clk) are generated by the following grammar ϕ ::= x ≺ l | x-y ≺ l | ϕ∧ϕ, where x, y ∈ Clk, ≺ ∈ {<, ≤, >, ≥} and l = a + b * ∆ is a linear expression such that a, b ∈ Q. Definition 22 A Parametric TIOA with parameter ∆, is a TIOA A such that guards and invariants are replaced by parametric guards.

∆ init = 8 =Figure 11 :

 811 Figure 11: Comparisons of the performances between the two methods Counter strategy Refinement (CR) and Binary Search (BS)

Figure 12 :

 12 Figure 12: Specification of the parking controller

  First, observe that for any clock valuation u and guard ϕ, if u |= ϕ ∆1 then u |= ϕ ∆2 , and conversely if u |= ϕ ∆2 then u |= ϕ ∆1 . We now check the refinement between I ∆1 sem and

Proof 1 (Property 1)

Algorithm 2 :

 2 Counter strategy refinement

		Input: (A ∆ rob , W o (Bad)): parametric robust timed game, (Z ∆ bad A , X 0 , -→): symbolic graph computed for (A ∆ bad rob , W o (Bad)) F i : spoiling strategy for input in (A ∆ bad rob , W o (Bad))
		Output: Infimum of the values ∆ bad such that F i is a spoiling strategy in (A ∆ bad rob , W o (Bad))
	1	begin
		/* Initialisation */
	2	W aiting ← ∅

Table 1 :

 1 Robust consistency of the university specifications

				∆init = 8		∆init = 6	∆init = 8	∆init = 6
	Game size		= 0.1		= 0.1	= 0.01	= 0.01
	Model	loc. edges	CR		BS		CR	BS	CR	BS	CR	BS
	M	9	21	119ms 314ms	119ms 262ms	119ms 438ms	119ms 437ms
	R	11	27	188ms 303ms	188ms 299ms	188ms 419ms	188ms 523ms
	A	9	22	133ms 316ms	133ms 287ms	133ms 441ms	133ms 483ms
	M A	41	158	10.1s	10.1s	10.1s	9.6s	10.4s	17.5s	10.4s	17.6s
	R A	48	201	14.1s	12.1s	12.5s	11s	14.1s	19.6s	12.5s	19.4s
	M R	44	152	10s		15.5s	9.81s	15.8s	10.3s	22.9s	9.78s	29.2s
	M R A	180 803	54.4s	56.3s	54.6s	112s	55s	58.8s	55.7s	216s
						∆init = 8	∆init = 6	∆init = 8	∆init = 6
			Game size		= 0.1	= 0.1	= 0.01	= 0.01
	Model		loc. edges		CR	BS	CR	BS	CR	BS	CR	BS
	M R		21	90	2.64s 4.34s	1.72s 4.02s	2.64s 5.5s	1.72s 5.45s
	M R A	75	399		48s	65s	42.7s 74.2s	48.2s 78.1s	42.9s 120s

Table 2 :

 2 Robust compatibility between the university specifications

  Scheduler. The second experiment studies a real time version of Milner's scheduler previously introduced in[START_REF] David | ECDAR: An environment for compositional design and analysis of real time systems[END_REF]. The model consists

				∆init = 30	∆init = 31	∆init = 30	∆init = 31
		Game size	= 0.5	= 0.5	= 0.1	= 0.1
	Model	loc. edges	CR	BS	CR	BS	CR	BS	CR	BS
	1 Node	13	35	0.97s	0.68s	1.09s	0.72s	0.97s	1.03s	1.09s	1.09s
	2 Nodes	81	344	10.7s	10.3s	11.2s	12.6s	10.5s	15.8s	11.1s	19.4s
	3 Nodes	449 2640	1m58 2m25	2m06 2m26	1m57 3m39	2m05 3m45
	4 Nodes	2305 17152	17m38 24m12	17m38 27m46	17m41 37m57	17m37 41m50

Table 3 :

 3 Robust consistency of Milner's scheduler nodes

Table 4 :

 4 Robust consistency of the parking controller

  . It shows that the robustness now remains constant for any number

	entry_ticket_issue!
	vehicle_enter?		L0	vehicle_exit? y<=10	lu
	request_enter?
			y>10
			vehicle_exit?
			y=0
	Figure 13: Assumption on the environment of the parking controller
	of vehicles
			= 0.1	= 0.01
	Number of vehicles	∆max CR	BS	CR	BS
	1	5	205ms 619ms	205ms 883ms
	2	2.5	1.11s	1.7s	1.11s	2.52s
	5	2.5	2.42s	3.26s	2.42s	4.34s
	10	2.5	5.6s	6.53s	5.61s	7.69s
	15	2.5	8.91s	9.86s	8.93s	11.2s
	20	2.5	12.7s	14s	12.7s	15.5s

Table 5 :

 5 Robust consistency of the parking's controller with assumption

The region graph of an automaton with rational constants can be built by scaling all constants of the automaton to work only with integers.

$ The research presented in this paper has been supported by MT-LAB, a VKR Centre of Excellence for the Modeling of Information Technology.

Parametric Robustness Evaluation

Let (A ∆ rob , W o (Bad)) be a parametric timed game that solve a robustness problem (either robust consistency or robust usefulness). We define ∆ max = Sup{∆ | (A ∆ rob , W o (Bad)) has a winning strategy}. Computing ∆ max would in general require to solve a parametric timed game. This problem is undecidable as it has been shown that parametric model-checking problem is undecidable [START_REF] Alur | Parametric real-time reasoning[END_REF]. In this paper we propose to compute an approximation of this maximum value. Due to the monotonicity of the robustness problems (Properties 1 and 4), we can apply an iterative evaluation procedure that searches for the maximum value until it belongs within a given precision interval. This basic procedure is describe in Algorithm 1 for the parametric game (A ∆ rob , W o (Bad)) for output (again it applies symmetrically to input). The algorithm assumes that the game (A 0 rob , W o (Bad)) is won, and on contrary that (A ∆init rob , W o (Bad)) is lost. If ∆ max is not infinite, then the maximum constant in the automaton can be used for ∆ init . At the heart of the algorithm the procedure RefineValues solves the game (A δ rob , W o (Bad)) for a value δ ∈ [∆ good , ∆ bad ]. It updates the variables ∆ good and ∆ bad according to the result.

Different algorithms can be used to implement RefineValues. A basic method is binary search. In that case RefineValues chooses the middle point ∆ mid of the interval [∆ good , ∆ bad ] and solves the game (A ∆ mid rob , W o (Bad)). According to the results it updates either ∆ good or ∆ bad . This algorithm has several drawbacks. First, the number of games it needs to solve heavily depends on the precision parameter. Second, depending on the initial maximum value a high proportion of the games played may be winning, which implies that they explore completely the state-graph of the model.

Correctness and termination.

The algorithm is correct if two invariants are satisfied: ∆ good is a lower bound for ∆ max , and ∆ bad is an upper bound. These invariants must be preserved by the implementation of RefineValues.

The algorithm terminates if at each iteration RefineValues reduces the length of the interval [∆ good , ∆ bad ] by some fixed minimum amount.

Counter Strategy Refinement

We propose an alternative method that analyzes the spoiling strategies computed when the game is lost and refine the value of the variable ∆ bad . With this algorithm only the last game is winning. The different steps are the following.

Solve the game (A ∆ bad

rob , W o (Bad)). 2. If the game is won, return the values (∆ bad , ∆ bad ). 3. Else extract a counter strategy F i for the input player. 4. Replay F i on the parametric game using Algorithm 2; it returns the value ∆ min = Inf{∆ | F i is a spoiling strategy in (A ∆ rob , W o (Bad))}. 5. If ∆ min is not a minimum (F i is not a spoiling strategy in (A ∆min rob , W o (Bad))) and ∆ bad -∆ min > , return the values (∆ good , ∆ min ). 6. Else return the values (∆ good , ∆ min -).

The goal of Algorithm 2 is to replay the spoiling strategy F i on the parametric game and compute the maximum value of ∆ such that this strategy becomes unfeasible. It takes as inputs the parametric game automaton A ∆ rob , the symbolic graph (Z ∆ bad A , X 0 , -→) computed for the game (A ∆ bad rob , W o (Bad)), and the spoiling strategy F i . It returns the infimum of the values ∆ bad such that F i is a spoiling strategy in the game (A ∆ bad rob , W o (Bad)). The algorithm is similar to the timed game algorithm proposed in [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] and implemented in the tool TIGA [START_REF] Behrmann | Uppaal-tiga: Time for playing games![END_REF]. However only the backward analysis is applied on parametric symbolic states, starting from the "bad" locations. Additionally the algorithm only explores the states that belongs to the outcome of F i . Since F i is a spoiling strategy in a safety game, its outcome contains a set of finite runs that eventually reach the "bad" locations. This ensures that a backward exploration restricted to this set of finite runs will terminate.

Formally, we define the outcome of a symbolic spoiling strategy F i for input. First, for a symbolic state X ∈ Z ∆ bad A , we define its timed successors restricted by the symbolic strategy F i as:

X Fi is computed by taking the intersection of the timed sucessors of X with the symbolic states on which is defined the strategy. Outcome(F i ) is the subset of runs in the symbolic graph defined inductively by: • (q 0 , X 0 Fi ) ∈ Outcome(F i ),

• if ρ ∈ Outcome(F i ) and last(ρ) = (q, Z), then ρ = ρ-→(q , Z ) ∈ Outcome(F i ) iff ∃(q, a, ϕ, λ, q ) ∈ E and one of the following condition holds: