Léo Henry

Thierry Jéron

Nicolas Markey

Control strategies for off-line testing of timed systems

Partial observability and controllability are two well-known issues in test-case synthesis for interactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. Building on the tioco timed testing framework, we extend a previous game interpretation of the test-synthesis problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We exhibit strategies of a game that tries to minimize both control losses and distance to the satisfaction of a test purpose, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method.

Introduction

Real-time interactive systems are systems interacting with their environment and subject to timing constraints. Such systems are encountered in many contexts, in particular in critical applications such as transportation, control of manufacturing systems, etc. Their correctness is then of prime importance, but it is also very challenging due to multiple factors: combination of discrete and continuous behaviours, concurrency aspects in distributed systems, limited observability of behaviours, or partial controllability of systems.

One of the most-used validation techniques in this context is testing, with variations depending on the design phases. Conformance testing is one of those variations, consisting in checking whether a real system correctly implements its specification. Those real systems are considered as black boxes, thereby offering only partial observability, for various reasons (e.g. because sensors cannot observe all actions, or because the system is composed of communicating components whose communications cannot be all observed, or again because of intellectual property of peer software). Controllability is another issue when the system makes its own choices upon which the environment, and thus the tester, have a limited control. One of the most-challenging activities in this context is the design of test cases that, when executed on the real system, should produce meaningful information about the conformance of the system at hand with respect to its specification. Formal models and methods are a good candidate to help this test-case synthesis [START_REF] Tretmans | Conformance testing with labelled transition systems: Implementation relations and test generation[END_REF]. Timed Automata (TA) [START_REF] Alur | A theory of timed automata[END_REF] form a class of model for the specification of timed reactive systems. It consists of automata equipped with real-valued clocks where transitions between locations carry actions, are guarded by constraints on clock values, and can reset clocks. TAs are also equipped with invariants that constrain the sojourn time in locations. TAs are popular in particular because reachability of a location is decidable using symbolic representations of sets of configurations by zones. In the context of testing, it is adequate to refine TAs by explicitly distinguishing (controllable) inputs and (uncontrollable) outputs, giving rise to TAIOs (Timed Automata with Inputs and Outputs). In the following, this model will be used for most testing artifacts, namely specifications, implementations, and test cases. Since completeness of testing is hopeless in practice, it is helpful to rely on test purposes that describe those behaviours that need to be tested because they are subject to errors. In our formal testing framework, an extension of TAIOs called Open TAIOs (or OTAIOs) is used to formally specify those behaviors. OTAIOs play the role of observers of actions and clocks of the specification: they synchronize on actions and clock resets of the specification (called observed clocks), and control their proper clocks. The formal testing framework also requires to formally define conformance as a relation between specifications and their possible implementations. In the timed setting, the classical tioco relation [START_REF] Krichen | Conformance testing for real-time systems[END_REF] states that, after a timed observable trace of the specification, the outputs and delays of the implementation should be specified.

Test-case synthesis from TAs has been extensively studied during the last 20 years (see [COG98,CKL98,SVD01,ENDK02,NS03,BB04,LMN04,KT09], to cite a few). As already mentioned, one of the difficulties is partial observation. In offline testing, where the test cases are first computed, stored, and later executed on the implementation, the tester should anticipate all specified outputs after a trace. In the untimed framework, this is tackled by determinization of the specification. Unfortunately, this is not feasible for TAIO specifications since determinization is not possible in general [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Finkel | Undecidable problems about timed automata[END_REF]. The solution was then either to perform online testing where subset construction is made on the current execution trace, or to restrict to determinizable sub-classes. More recently, some advances were obtained in this context [START_REF] Bertrand | Offline test selection with test purposes for non-deterministic timed automata[END_REF] by the use of an approximate determinization using a game approach [START_REF] Bertrand | A game approach to determinize timed automata[END_REF] that preserves tioco conformance. Partial observation is also dealt with by [DLL + 10] with a variant of the TA model where observations are described by observation predicates composed of a set of locations together with clock constraints. Test cases are then synthesized as winning strategies, if they exist, of a game between the specification and its environment that tries to guide the system to satisfy the test purpose.

The problem of test synthesis is often informally presented as a game between the environment and the system (see e.g. [START_REF] Yannakakis | Testing, optimization, and games[END_REF]). But very few papers effectively take into account the controllability of the system. In the context of testing for timed-automata models [START_REF] David | A gametheoretic approach to real-time system testing[END_REF], proposes a game approach where test cases are winning strategies of a reachability game. But this is restricted to deterministic models and controllability is not really taken into account. In fact, like in [DLL + 10], the game is abandonned when control is lost, and it is suggested to modify the test purpose in this case. This is mitigated in [START_REF] David | Cooperative testing of timed systems[END_REF] with cooperative strategies, which rely on the cooperation of the system under test to win the game. A more convincing approach to the control problem is the one of [START_REF] Ramangalahi | Strategies for comformance testing[END_REF] in the untimed setting, unfortunately a quite little-known work. The game problem consists in satisfying the test purpose (a simple sub-sequence), while trying to avoid control losses occurring when outputs offered by the system leave this behaviour. The computed strategy is based on a rank that measures both the distance to the goal and the controls losses.

The current paper adapts the approach proposed in [START_REF] Ramangalahi | Strategies for comformance testing[END_REF] to the timed context using the framework developed in [START_REF] Bertrand | Offline test selection with test purposes for non-deterministic timed automata[END_REF]. Compared to [START_REF] Ramangalahi | Strategies for comformance testing[END_REF], the model of TA is much more complex than transition systems, the test purposes are also much more powerful than simple sub-sequences, thus even if the approach is similar, the game has to be completely revised. Compared to [DLL + 10], our model is a bit different since we do not rely on observation predicates, but partial observation comes from internal actions and choices. We do not completely tackle non-determinism since we assume determinizable models at some point. In comparison, [DLL + 10] avoids determinizing TAs, relying on the determinization of a finite state model, thanks to a projection on a finite set of observable predicates. Cooperative strategies of [START_REF] David | Cooperative testing of timed systems[END_REF] have similarities with our fairness assumptions, but their models are assumed deterministic. Our approach takes controllability into account in a more complete and practical way with the reachability game and rank-lowering strategies.

The paper is organized as follows. Chapter 2 introduces basic models: TAs, TAIOs and their open counterparts OTAs, OTAIOs, and then timed game automata (TGA). Chapter 3 is dedicated to the testing framework with hypothesis on models of testing artifacts, the conformance relation and the construction of the objective-centered tester that denotes both non-conformant traces and the goal to reach according to a test purpose. Chapter 4 constitutes the core of the paper. The test synthesis problem is interpreted as a game on the objectivecentered tester. Rank-lowering strategies are proposed as candidate test cases, and a fairness assumption is introduced to make such strategies win. Finally properties of test cases with respect to conformance are proved.

Timed automata and timed games

In this section, we introduce our models for timed systems and for concurrent games on these objects, along with some useful notions and operations.

Timed automata with inputs and outputs

Timed automata (TAs) [START_REF] Alur | A theory of timed automata[END_REF] are one of the most widely-used classes of models for reasoning about computer systems subject to real-time constraints. Timed automata are finite-state automata augmented with real-valued variables (called clocks) to constrain the occurrence of transitions along executions. In order to adapt these models to the testing framework, we consider TAs with inputs and outputs (TAIOs), in which the alphabet is split between input, output and internal actions (the latter being used to model partial observation). We present the open TAs (and open TAIOs) [START_REF] Bertrand | Offline test selection with test purposes for non-deterministic timed automata[END_REF], which allow the models to observe and synchronize with a set of non-controlled clocks.

Given a finite set of clocks X, a clock valuation over X is a function v : X → R ≥0 . We note 0 X (and often omit to mention X when clear from the context) for the valuation assigning 0 to all clocks in X. Let v be a clock valuation, for any t ∈ R ≥0 , we denote with v + t the valuation mapping each clock x ∈ X to v(x) + t, and for a subset X ⊆ X, we write v [X ←0] for the valuation mapping all clocks in X to 0, and all clocks in X \ X to their values in v.

A clock constraint is a finite conjunction of atomic constraints of the form x ∼ n where x ∈ X, n ∈ N, and ∼ ∈ {<, ≤, =, ≥, >}. That a valuation v satisfies a clock constraint g, written v |= g, is defined in the obvious way. We write C(X) for the set of clock constraints over X.

Definition 1. An open timed automaton (OTA) is a tuple 1 A = (L A , l A 0 , Σ A , X A p X A o , I A , E A ) where: -L A is a finite set of locations, with l A 0 ∈ L A the initial location, -Σ A is a finite alphabet, -X A = X A p X A
o is a finite set of clocks, partitionned into proper clocks X A p and observed clocks X A o ; only proper clocks may be reset along transitions.

-I A : L A → C(X A ) assigns invariant constraints to locations. -E A ⊆ L A × C(X A ) × Σ A × 2 X A
p × L A is a finite set of transitions. For e = (l, g, a, X , l ) ∈ E A , we write act(e) = a.

An Open Timed Automaton with Inputs and Outputs (OTAIO) is an OTA in which

Σ A = Σ A ? Σ A ! Σ A
τ is the disjoint union of input actions in Σ A ? (noted ?a, ?b, ...), output actions in Σ A ! (noted !a, !b, ...), and internal actions in Σ A τ (noted τ 1 , τ 2 , ...) We write Σ obs = Σ ? Σ ! for the alphabet of observable actions. Finally, a Timed Automaton (TA) (resp. a Timed Automaton with Inputs and Outputs (TAIO)) is an OTA (resp. an OTAIO) with no observed clocks.

TAIOs will be sufficient to model most objects, but the ability of OTAIOs to observe other clocks will be essential for test purposes (see Section 3.1), which need to synchronize with the specification. Let A = (L, l 0 , Σ, X p X o , I, E) be an OTA. Its semantics is defined as an infinite-state transition system T A = (S A , s A 0 , Γ A , → A ) where: An OTA has no control over its observed clocks, the intention being to synchronize them later in a product (see Def. 2). Hence, when a discrete transition is taken, any set X o of observed clocks may be reset. When dealing with plain TAs, where X o is empty, we may write (l, v) e -→ (l , v ) in place of (l, v)

-S A = {(l, v) ∈ L × R X ≥0 | v |= I(l)} is the (infinite) set of configurations, with initial configuration s A 0 = (l 0 , 0 X ). -Γ A = R ≥0 (E × 2 Xo ) is the set of transitions labels. -→ A ⊆ S A × Γ A × S A
(e,∅) ---→ (l , v ).
A partial run of A is a (finite or infinite) sequence of transitions in T A ρ = ((s i , γ i , s i+1 )) 1≤i<n , with n ∈ N ∪ {+∞}. We write first(ρ) for s 1 and, when n ∈ N, last(ρ) for s n . A run is a partial run starting in the initial configuration s A 0 . The duration of ρ is dur(ρ) = γi∈R ≥0 γ i . In the sequel, we only consider TAs in which any infinite run has infinite duration. We note Ex(A) for the set of runs of A and pEx(A) the subset of partial runs.

State s is reachable from state s when there exists a partial run from s to s. We write Reach(A, S ) for the set of states that are reachable from some state in S , and Reach(A) for Reach(A, {s A 0 }). The (partial) sequence associated with a (partial) run ρ = ((s i , γ i , s i )) i is seq(ρ) = (proj(γ i )) i , where proj(γ) = γ if γ ∈ R ≥0 , and proj(γ) = (a, X p ∪ X o ) if γ = ((l, g, a, X p , l ), X o ). We write pSeq(A) = proj(pEx(A)) and Seq(A) = proj(Ex(A)) for the sets of (partial) sequences of A. We write s µ -→ s when there exists a (partial) finite run ρ such that µ = proj(ρ), first(ρ) = s and last(ρ) = s , and write dur(µ) for dur(ρ). We write s µ -→ when s µ -→ s for some s. If A is a TAIO, the trace of a (partial) sequence corresponds to what can be observed by the environment, namely delays and observable actions. The trace of a sequence is the limit of the following inductive definition, for δ i ∈ R ≥0 , a ∈ Σ obs , τ ∈ Σ τ , X ⊆ X, and a partial sequence µ:

Trace(δ 1 ...δ k ) = k i=1 δ i (in particular Trace( ) = 0) Trace(δ 1 ...δ k .(τ, X ).µ) = ( k i=1 δ i ) • Trace(µ) Trace(δ 1 ...δ k .(a, X ).µ) = ( k i=1 δ i ) • a • Trace(µ)
We note Traces(A) = Trace(Seq(A)) the set of traces corresponding to runs of A and pTraces(A) the subset of traces corresponding to partial runs. Two OTAIOs are said to be trace-equivalent if they have the same sets of traces. We furthermore define, for an OTAIO A, a trace σ and a configuration s:

-A after σ = {s ∈ S | ∃µ ∈ Seq(A), s 0 µ -→ s ∧ Trace(µ) = σ}
is the set of all configurations that can be reached when σ has been observed from

s A 0 . -enab(s) = {e ∈ E A | s e -→} is the set of transitions enabled in s. -elapse(s) = {t ∈ R ≥0 | ∃µ ∈ (R ≥0 ∪ (Σ τ × 2 X )) * , s µ -→ ∧dur(µ) = t}
is the set of delays that can be observed from location s without any observation. -out(s) = {a ∈ Σ ! | ∃e ∈ enab(s), act(e) = a} ∪ elapse(s) is the set of possible outputs and delays that can be observed from s. For S ⊆ S, we note out(S ) = s∈S out(s). -in(s) = {a ∈ Σ ! | ∃e ∈ enab(s), act(e) = a} is the set of possible inputs that can be proposed when arriving in s. For S ⊆ S, we note in(S ) = s∈S in(s).

We now define some useful sub-classes of OTAIOs. An OTAIO A is said deterministic if for all σ ∈ T races(A), A after σ is a singleton; determinizable if there exists a trace-equivalence deterministic OTAIO; complete if S = L×R X ≥0 (i.e., all invariants are always true) and for any s ∈ S and any a ∈ Σ, it holds s a,X ---→ for some X ⊆ X; input-complete if for any s ∈ Reach(A), in(s) = Σ ? ; non-blocking if for any s ∈ Reach(A) and any non-negative real t, there is a partial run ρ from s involving no input actions (i.e., proj(ρ

) is a sequence over R ≥0 ∪ (Σ ! ∪ Σ τ ) × 2 X
) and such that dur(ρ) = t; repeatedly observable if for any s ∈ Reach(A), there exists a partial run ρ from s such that Trace(ρ) / ∈ R ≥0 .

The product of two OTAIOs extends the classical product of TAs.

Definition 2. Given two OTAIOs

A = (L A , l A 0 , Σ ? Σ ! Σ τ , X A p X A o , I A , E A ) and B = (L B , l B 0 , Σ ? Σ ! Σ τ , X B p X B o , I B , E B ) over the same alphabets, their product is the OTAIO A × B = (L A × L B , (l A 0 , l B 0 ), Σ ? Σ ! Σ τ , (X A p ∪ X B p ) ((X A o ∪ X B o ) \ (X A p ∪ X B p )), I, E) where I : (l 1 , l 2 ) → I A (l 1 ) ∧ I B (l 2 ) and E is the (smallest) set such that for each (l 1 , g 1 , a, X 1 p , l 1 ) ∈ E A and (l 2 , g 2 , a, X 2 p , l 2 ) ∈ E B , E contains ((l 1 , l 2 ), g 1 ∧ g 2 , a, X 1 p ∪ X 2 p , (l 1 , l 2 )).
The product of two OTAIOs corresponds to the intersection of the sequences of the orginal OTAIOs, i.e.

Seq(A × B) = Seq(A) ∩ Seq(B) [BSJK15].

Timed games

We introduce timed game automata [START_REF] Asarin | Controller synthesis for timed automata[END_REF], which we later use to turn the test artifacts into games between the tester (controlling the environment) and the implementation, on an arena constructed from the specification.

Definition 3. A timed game automaton (TGA) is a timed automaton G = (L, l 0 , Σ c Σ u , X, I, E) where Σ = Σ c Σ u is partitioned into actions that are controllable (Σ c
) and uncontrollable (Σ u ) by the player.

All the notions of runs and sequences defined previously for TAs are extended to TGAs, with the interpretation of Σ c as inputs and Σ u as outputs.

Definition 4. Let G = (L, l 0 , Σ c Σ u , X, I, E) be a TGA. A strategy for the player is a partial function f :

Ex(G) → R ≥0 × (Σ c ∪ {⊥}) \ {(0, ⊥)} such that for any finite run ρ, letting f (ρ) = (δ, a), δ ∈ elapse(last(ρ)
) is a possible delay from last(ρ), and there is an a-transition available from the resulting configuration (unless a = ⊥).

Strategies give rise to sets of runs of G, defined as follows:

Definition 5. Let G = (L, l 0 , Σ, X, I, E) be a TGA, f be a strategy over G, and s be a configuration. The set of outcomes of f from s, noted Outcome(s, f ), is the smallest subset of partial runs starting from s containing the empty partial run from s (whose last configuration is s), and s.t. for any ρ ∈ Outcome(s, f ), letting f (ρ) = (δ, a) and last(ρ) = (l, v), we have

-ρ•((l, v), δ, (l, v +δ ))•((l, v +δ ), e, (l , v )) ∈ Outcome(s, f ) for any 0 ≤ δ ≤ δ and act(e) ∈ Σ u such that ((l, v + δ ), e, (l , v )) ∈ pEx(A); -and • either a = ⊥, and ρ • ((l, v), δ, (l, v + δ)) ∈ Outcome(s, f ); • or a ∈ Σ c , and ρ • ((l, v), δ, (l, v + δ)) • ((l, v + δ), e, (l , v )) ∈ Outcome(s, f ) with act(e) = a;
An infinite partial run is in Outcome(s, f ) if infinitely many of its finite prefixes are.

In this paper, we will be interested in reachability winning conditions (under particular conditions). In the classical setting, the set of winning configurations can be computed iteratively, starting from the target location and computing controllable predecessors in a backward manner. The computation can be performed on regions, so that it terminates (in exponential time) [AMPS98,CDF + 05]. We extend this approach to our test-generation framework in Section 4.

Testing framework

We now present the testing framework, defining (i) the main testing artifacts i.e. specifications, implementations, test purposes, and test cases, along with the assumptions on them; (ii) a conformance relation relating implementations and specifications. The combination of the test purposes and the specification and the construction of an approximate deterministic tester is afterward explained.

Test context

We use TAIOs as models for specifications, implementations and test cases, and OTAIOs for test purposes. This allows to define liberal test purposes, and on a technical side, gives a unity to the manipulated objects.

In order to enforce the occurrence of conclusive verdicts, we equip specifications with restart transitions, corresponding to a system shutdown and restart, and assume that from any (reachable) configuration, a restart is always reachable. Definition 6. A specification with restarts (or simply specification) on (Σ ? , Σ ! , Σ τ ) is a non-blocking, repeatedly-observable TAIO S = (L S , l S 0 , (Σ ? ∪ {ζ}) Σ ! Σ τ , X S p , I S , E S ) where ζ / ∈ Σ ? is the restart action. We let

Restart S = E S ∩ (L S × G M S (X S ) × {ζ} × {X S p } × {l S 0 }
) be the set of ζ-transitions, and it is assumed that from any reachable configuration, there exists a finite partial execution containing ζ, i.e. for any s ∈ Reach(S), there exists µ s.t.

s µ•ζ --→ s S 0 .
The non-blocking hypothesis rules out "faulty" specifications having no conformant physically-possible implementation. Repeated-observability will be useful for technical reasons, when analyzing the exhaustiveness property of test cases. Our assumption on ζ-transitions entails: Proposition 7. Let S be a specification with restarts. Then Reach(T S ) is stronglyconnected.

Example 1. Figure 1 is an example of specification for a conveyor belt. After a maximum time of 2 units (depending for example on their weight), packages reach a sorting point where they are automatically sorted between packages to reject and packages to ship. Packages to reject go to waste, while packages to ship are sent to a boarding platform, where an operator can send them to two different destinations. If the operator takes more than 3 units of time to select a destination, the package goes past the boarding platform and restarts the process. In practice, test purposes are used to describe the intention of test cases, typically behaviours one wants because they must be correct and/or an error is suspected. In our formal testing framework, we describe them with OTAIOs that observe the specification together with accepting locations.

Definition 8. Given a specifica- tion S = (L S , l S 0 , (Σ ? ∪ {ζ}) Σ ! Σ τ , X S p , I S , E S
Restart), a test purpose for S is a pair (T P, Accept T P ) where T P = (L T P , l T P 0 , Σ ? ∪{ζ} Σ ! Σ τ , X T P p X S p , I T P , E T P ) is a complete OTAIO together with a subset Accept T P ⊆ L T P of accepting locations, and such that transitions carrying restart actions ζ reset all proper clocks and return to the initial state (i.e., for any ζ-transition (l, g, ζ, X , l ) ∈ E, it must be X = X T P p and l = l T P 0 ).

In the following, we may simply write T P in place of (T P, Accept T P ). We force test purposes to be complete because they should never constrain the runs of the specification they observe, but should only label the accepted behaviours to be tested. Test purposes observe exactly the clocks of the specification in order to synchronize with them, but cannot reset them.

Example 2. Figure 2 is a test purpose for our conveyor-belt example. We want to be sure that it is possible to ship a package to destination 2 in less than 5 time units, while avoiding to go in waste. The Accept set is limited to a location, named Accept. We note oth the set of transitions that reset no clocks, and is enabled for an action other than ζ when no other transition is possible for this action. This set serves to complete the test purpose. The test purpose has a proper clock y. In practice, conformance testing links a mathematical model, the specification, and a blackbox implementation, that is a real-life physical object observed by its interactions with the environment. In order to formally reason about conformance, one needs to bridge the gap between the mathematical world and the physical world. We then assume that the implementation corresponds to an unknown TAIO.

Definition 9. Let S = (L S , l S 0 , (Σ ? ∪ {ζ}) Σ ! Σ τ , X S p , I S , E S ∪ Restart) be a specification TAIO. An implementation of S is an input-complete and nonblocking TAIO I = (L I , l I 0 , (Σ ? ∪ {ζ}) Σ ! Σ I τ , X I p , I I , E I ). We note I(S) the set of possible implementations of S.

The hypotheses made on implementations are not restrictions, but model real-world contingencies: the environment might always provide any input and the system cannot alter the course of time.

Having defined the necessary objects, it is now possible to introduce the timed input-output conformance (tioco) relation [START_REF] Krichen | Conformance testing for real-time systems[END_REF]. Intuitively, it can be understood as "after any specified behaviour, outputs and delays of the implementation should be specified".

Definition 10. Let S be a specification and I ∈ I(S). We say that I conforms to S for tioco, and write I tioco S when: ∀σ ∈ Traces(S), out(I after σ) ⊆ out(S after σ) Note that it is not assumed that restarts are well implemented: if they are not, it is significant only if it induces non-conformant behaviours.

Combining specifications and test purposes

Now that the main objects are defined, we explain how the behaviours targeted by the test purpose T P are characterized on the specification S by the construction of the product OTAIO P = S × T P. Since S is a TAIO and the observed clocks of T P are exactly the clocks of S, the product P is actually a TAIO. Furthermore, since T P is complete, Seq(P) = Seq(S). This entails that I tioco S is equivalent to I tioco P. Note in particular that ζ of S synchronize with ζ of T P, which are available everywhere.

By defining accepting locations in the product by Accept P = L S × Accept T P , we get that sequences accepted in P are exactly sequences of S accepted by T P. We make one final hypothesis: we consider only pairs of specifications S and test purposes T P whose product P can be exactly determinized by the determinization game presented in [START_REF] Bertrand | A game approach to determinize timed automata[END_REF]. This restriction is necessary for technical reasons: if the determinization is approximated, we cannot ensure that restarts are still reachable in general. Notice that it is satisfied in several classes of automata, such as strongly non-zeno automata, integer-reset automata, or event-recording automata.

Given the product P = S × T P, let DP be its exact determinization. In this case, Traces(DP) = Traces(P), hence the reachability of ζ transitions is preserved. Moreover the traces leading to Accept DP and Accept P are the same.

Accounting for failure

At this stage of the process, we dispose of a deterministic and fully-observable TAIO DP having exactly the same traces as the original specification, and having a subset of its localities labelled as accepting for the test purpose. From this TAIO, we aim to build a tester, that can be able to monitor the implementation, feeding it with inputs and selecting verdicts from the returned outputs.

DP models the accepted traces with Accept DP . In order to also explicitely model faulty behaviours (unspecified outputs after a specified trace), we now complete DP with respect to its output alphabet, by adding an explicit Fail location. We call this completed TAIO the objective-centered tester.

Definition 11. Given a deterministic TAIO DP = (L DP , l DP 0 , Σ ? Σ ! Σ τ , X DP p , I DP , E DP ), we construct its objective-centered tester OT = (L DP ∪ {Fail}, l DP 0 , Σ ? Σ ! Σ τ , X DP p , I OT , E OT ) where I OT (l) = true. The set of transitions E OT is defined from E DP by:

E OT = E DP ∪ l∈L DP a∈Σ DP ! {(l, g, a, ∅, Fail) | g ∈ G a,l } ∪ {(Fail, true, a, ∅, Fail) | a ∈ Σ DP }
where for each a and l, G a,l is a set of guards complementing the set of all valuations v for which an a-transition is available from (l, v) (notice that G a,l generally is non-convex, so that it cannot be represented by a single guard).

Verdicts are defined on the configurations of OT as follows:

-Pass = l∈Accept DP ({l} × I DP (l)),

-Fail = {Fail} × R ≥0 ∪ l∈L DP {l} × R Xp ≥0 \ I DP (l) .
Notice that we do not define the usual Inconclusive verdicts (i.e. configurations in which we cannot conclude to non-conformance, nor accept the run with respect to the test purpose) as we will enforce the apparition of Pass or Fail . Pass corresponds to behaviours accepted by the test purpose, while Fail corresponds to non-conformant behaviours. Note that OT inherits the interesting structural properties of DP. More importantly, ζ is always reachable as long as no verdict has been emited, and OT is repeatedly-observable out of Fail .

It remains to say that OT and DP model the same behaviours. Obviously, their sets of traces differ, but the traces added in OT precisely correspond to runs reaching Fail . We now define a specific subset of runs, sequences and traces corresponding to traces that are meant to be accepted by the specification. Definition 12. A run ρ of an objective-centered tester OT is said conformant if it does not reach Fail. We note Ex conf (OT ) the set of conformant runs of OT , and Seq conf (OT ) (resp. Traces conf (OT )) the corresponding sequences (resp. traces). We note Ex fail (OT ) = Ex(OT ) \ Ex conf (OT ) and similarly for the sequences and traces.

The conformant traces are exactly those specified by DP, i.e. Traces(DP) = Traces conf (OT ) and correspond to executions tioco-conformant with the specification, while Ex fail are runs where a non-conformance is detected.

Translating objectives into games

In this section, we interpret objective-centered tester into games between the tester and the implementation and propose strategies that try to avoid control losses. We then introduce a scope in which the tester always has a winning strategy, and discuss the properties of the resulting test cases (i.e. game structure and built strategy).

We want to enforce conclusive verdicts when running test cases, i.e. either the implementation does not conform to its specification (Fail verdict) or the awaited behaviour appears (Pass verdict). We thus say that an execution ρ is winning for the tester if it reaches a Fail or Pass configuration and note Win(G) the set of such executions. In the following, we consider the TGA G OT = (L OT , l OT 0 , Σ OT ? Σ OT ! , X p , I OT , E OT ) where the controllable actions are the inputs Σ c = Σ OT ? and the uncontrollable actions are the outputs Σ u = Σ OT ! .

Rank-lowering strategy

In this part, we restrict our discussion to TGAs where Pass configurations are reachable (when seen as plain TAs). Indeed, if none can be reached, and we will discuss the fact that the proposed method can detect this fact, trying to construct a strategy seeking a Pass verdict is hopeless. This is a natural restriction, as it only rules out unsatisfiable test purposes.

The tester cannot force the occurrence of a non-conformance (as he does not control outputs and delays), and hence cannot push the system into a Fail configuration. A strategy for the tester should thus target the Pass set in a partially controlable way, while monitoring Fail . For that purpose, we define a hierarchy of configurations, depending on their "distance" to Pass. This uses a backward algorithm, for which we define the predecessors of a configuration.

Given a set of configurations S ⊆ S of G OT , we define three kinds of predecessors, letting V denote the complement of V :

discrete predecessors by a sub-alphabet Σ ⊆ Σ:

Pred Σ (S ) = {(l, v) | ∃a ∈ Σ , ∃(l, a, g, X , l ) ∈ E, v |= g∧(l , v [X ←0] ) ∈ S }
timed predecessors, while avoiding a set V of configurations:

tPred(S , V ) = {(l, v) | ∃δ ∈ R ≥0 , (l, v+δ) ∈ S ∧∀ 0 ≤ δ ≤ δ. (l, v+δ ) / ∈ V }
We furthermore note tPred(S ) = tPred(S , ∅). final timed predecessors are defined for convenience (see below):

ftPred(S ) = tPred(Fail , Pred Σu (S )) ∪ tPred(Pred Σ (S ))
The final timed predecessors correspond to situations where the system is 'cornered', having the choice between taking an uncontrollable transition to S (as no uncontrollable transition to S will be available) or reach Fail . Such situations are not considered as control losses, as the system can only take a beneficial transition for the tester (either by going to S or to Fail ). Note that tPred and ftPred need not return convex sets, but are efficiently computable using Pred and simple set constructions [CDF + 05]. Now, using these notions of predecessors, a hierarchy of configurations based on the 'distance' to Pass is defined.

Definition 13. The sequence (W j i ) j,i of sets of configurations is defined as:

-W 0 0 = Pass -W j i+1 = π(W j i ) with π(S ) = tPred S ∪ Pred Σc (S ), Pred Σu (S ) ∪ ftPred(S ) -W j+1 0 = tPred(W j ∞ ∪ Pred Σ (W j ∞ )
) with W j ∞ the limit2 of the sequence (W j i ) i . In this hierarchy, j corresponds to the minimal number of control losses the tester has to go through (in the worst case) in order to reach Pass, and i corresponds to the minimal number of steps before the next control loss (or to Pass). The W j+1 0 are considered 'control losses' as the implementation might take an output transition leading to an undesirable configuration (higher on the hierarchy). On the other hand, in the construction of W j i the tester keep a full control, as it is not possible to reach such bad configuration with an incontrolable transition. Notice that the sequence (W j i ) is an increasing sequence of regions, and hence can be computed in time exponential in X OT and linear in L OT .

We then have the following property: Proposition 14. There exists i, j ∈ N such that Reach(G OT ) \ Fail ⊆ W j i .

As explained above, this property is based on the assumption that the Pass verdict is reachable. Nevertheless, if it is not it will be detected during the hierarchy construction that will converge to a fixpoint not including s G 0 . As all the configurations in which we want to define a strategy are covered by the hierarchy, we can use it to define a partial order.

Definition 15. Let s ∈ Reach(G OT ) \ Fail. The rank of s is:

r(s) = (j s = arg min j∈N (s ∈ W j ∞ ), i s = arg min i∈N (s ∈ W js i ))
For r(s) = (j, i); j is the minimal number of control losses before reaching an accepting state, and i is the minimal number of steps in the strategy before the next control loss. We note s s when r(s) ≤ N 2 r(s ), where ≤ N 2 is the lexical order on N 2 .

Proposition 16. is a partial order on Reach(G OT ) \ Fail.

We dispose of a partial order on configurations, with Pass being the minimal elements. We use it to define a strategy trying to decrease the rank during the execution. For any s ∈ S, we write r -(s) for the largest rank such that r -(s) < N 2 r(s), and W -(s) for the associated set in (W j i ) j,i . We (partially) order pairs (δ, a) ∈ R ≥0 × Σ according to δ. Definition 17. A strategy f for the tester is rank-lowering if, for any finite run ρ with last(ρ) = s = (l, v), it selects the lesser delay satisfying one of the following constraints:

-if s ∈ tPred(Pred Σc (W -(s))),then f (ρ) = (δ,
-if s ∈ tPred(W -(s)),then f (ρ) = (δ, ⊥) such that s δ -→ t with t ∈ W -(s)
, and δ is minimal in the same sense as above; otherwise f (ρ) = (δ, ⊥) where δ is maximal in the same sense as above (maximal delay-successor region).

The two first cases follow the construction of the W j i and propose the shortest behaviour leading to W -. The third case corresponds, either to a configuration of Pass, where W -is undefined, or to a ftPred. Notice that (possibly several) rank-lowering strategies always exist. Example 5. An example of a rank-lowering strategy on the automaton of Fig. 4 is: in (D 2 , A), play ⊥ (as W 0 0 has been reached); in St, play (0, ship 2 ?); in any other state, play (0, ζ). Note that Fig. 4 has not been completed in a objective-centered tester. This does not impact the strategies, as the transition to the failstates lead to a victory, but are not targeted by the strategies.

It is worth noting that even in a more general setup where the models are not equipped with ζ-transitions, as in [START_REF] Bertrand | A game approach to determinize timed automata[END_REF], rank-lowering strategies may still be useful: as they are defined on the co-reachable set of Accept, they can still constitute test cases, and the configurations where they are not defined are exactly the configurations corresponding to a Fail verdict or to an Inconclusive verdict, i.e., no conclusions can be made since an accepting configuration cannot be reached.

Making rank-lowering strategies win

A rank-lowering strategy is generally not a winning strategy: it relies on the implementation fairly exploring its different possibilities and not repeatedly avoiding an enabled transition. In this section, fair runs are introduced, and the rank-lowering strategies are shown to be winning in this subset of the runs.

Lemma 18. If OT is repeatedly-observable, then for all ρ = ((s i , γ i , s i+1 )) i∈N ∈ Ex(G) ending with an infinite sequence of delays, we have

3 ρ ∈ Ex fail (G) ∨ ∃e ∈ E G , ∞ ∃ i ∈ N, e ∈ enab(s i ).
This lemma ensures that we cannot end in a situation where no transitions can be taken, forcing the system to delay indefinitely. It will be used with the support of fairness. In order to introduce our notion of fairness, we define the infinite support of a run. Definition 19. Let ρ be an infinite run, its infinite support Inf(ρ) is the set of regions appearing infinitely often in ρ.

Inf((s

i , γ i , s i+1 ) i∈N ) = {r | ∞ ∃ i ∈ N, s i ∈ r ∨ (γ i ∈ R ≥0 ∧ ∃s i ∈ r, ∃δ i < γ i , s i δi -→ s i )}
The notion of enabled transitions and delay transitions are extended to regions as follows: for a region r, we let enab(r) = enab(s) for any s in r, and write r t -→ r for all time-successor region r of r.

Definition 20. An infinite run ρ in a TGA G = (L, l 0 , Σ u Σ c , X, I, E) (with timed transitions system T = (S, s 0 , Γ, → T )) is said to be fair when:

∀e ∈ E, (act(e) ∈ Σ u ⇒ (∃r ∈ Inf(ρ), r e -→ r ⇒ r ∈ Inf(ρ))) ∧ ∀r ∈ Inf(ρ), ∃γ ∈ (enab(r) ∩ {e | act(e) ∈ Σ c }) ∪ {t}), r γ -→ r ∧ r ∈ Inf(ρ)
We note Fair(G) the set of fair runs of G.

3 In this expression, ∞ ∃ i ∈ N, φ(i) means that φ(i) is true for infinitely many integers.

Fair runs model restrictions on the system runs corresponding to strategies of the system. The first part of the definition assures that any infinitely-enabled action of the implementation will be taken infinitely many times, while the second part ensures that the implementation will infinitely often let the tester play, by ensuring that a delay or controlable action will be performed. It matches the "strong fairness" notion used in model checking. Restricting to fair runs is sufficient to ensure a winning execution when the tester uses a rank-lowering strategy. Intuitively, combined with Lemma 18 and the repeated-observability assumption, it assures that the system will keep providing outputs until a verdict is reached, and allows to show the following property.

Proposition 21. Rank-lowering strategies are winning on Fair(G) (i.e., all fair outcomes are winning).

Under the hypothesis of a fair implementation, we thus have identified a test-case generation method, starting from the specification with restarts and the test purpose, and constructing a test case as a winning strategy on the game created from the objective-centered tester. The complexity of this method is exponential in the size of DP. More precisely: Proposition 22. Given a deterministic product DP, OT can be linearly computed from DP, and the construction of a strategy relies on the construction of the W j i and is hence exponential in X DP and linear in L DP . Note that if DP is obtained from P by the game presented in [START_REF] Bertrand | A game approach to determinize timed automata[END_REF], then L DP is doubly exponential in the size of X S X T P X DP (notice that in the setting of [START_REF] Bertrand | A game approach to determinize timed automata[END_REF], X DP is a parameter of the algorithm).

Properties of the test cases

Having constructed strategies for the tester, and identified a scope of implementation behaviours that allows these strategies to enforce a conclusive verdict, we now study the properties obtained by the test generation method presented above. We call test case a pair (G, f ) where G is the game corresponding to the objectivecentered tester OT , and f is a rank-lowering strategy on G. We note T C(S, T P) the set of possibles test cases generated from a specification S and a test purpose T P, and T C(S) the test cases for any test purpose. Recall that it is assumed that the test purposes associated with a specification are restricted to those leading to a determnizable product. Behaviours are defined as the possible outcomes of a test case combined with an implementation, and model their parallel composition.

Definition 23. Given a test case (G, f ) and an implementation I, their behaviours are the runs ((s i , s i ), (e i , e i ), (s i+1 , s i+1 )) i such that ((s i , e i , s i+1 )) i is an outcome of (G, f ), ((s i , e i , s i+1 )) i is a run of I, and for all i, either e i = e i if e i ∈ R ≥0 or act(e i ) = act(e i ) otherwise. We write Behaviour(G, f, I) for the set of behaviours of the test case (G, f ) and of the implementation I.

We say that an implementation I fails a test case (G, f ), and note I fails (G, f ), when there exists a run in Behaviour(G, f, I) that reaches Fail . Our method is sound, that is, a conformant implementation cannot be detected as faulty.

Proposition 24. The test-case generation method is sound: for any specification S, it holds ∀I ∈ I(S), ∀(G, f ) ∈ T C(S), (I fails (G, f ) ⇒ ¬(I tioco S)).

The proofs of this property and the following one are based on the exact correspondance between Fail and the faulty behaviours of S, and use the trace equivalence of the different models (DP, P and S) to conclude. As they exploit mainly the game structure, fairness is not used.

We define the notion of outputs after a trace in a behaviour, allowing to extend tioco to these objects and to state a strictness property. Intuitively, when a non-conformance appears it should be detected.

Definition 25. Given a test case (G, f ) and an implementation I, for a trace σ: Proposition 27. The test case generation method is precise: for any specification S and test purpose T P it can be stated that ∀(G, f ) ∈ T C(S, T P), ∀σ ∈ Traces(Outcome(s G 0 , f )), G after σ ∈ Pass ⇔ (σ ∈ Traces(S) ∧ T P after σ ∩ Accept T P = ∅) Lastly, this method is exhaustive in the sense that for any non-conformance, there exist a test case that allows to detect it, under fairness assumption.

out(Behaviour(G, f, I) after σ) = {a ∈ Σ ! ∪ R ≥0 | ∃ρ ∈ Behaviour(G, f, I), Trace(ρ) = σ • a}
Proposition 28. The test generation method is exhaustive: for any exactly determinizable specification S and any implementation I ∈ I(S) making fair runs ¬(I tioco S) ⇒ ∃(G, f ) ∈ T C(S), I fails (G, f ).

To demonstrate this property, a test purpose is tailored to detect a given non-conformance, by targeting a related conformant trace.

Conclusion

This paper proposes a game approach to the controllability problem for conformance testing from timed automata (TA) specifications. It defines a test synthesis method that produces test cases whose aim is to maximize their control upon the implementation under test, while detecting non-conformance. Test cases are defined as strategies of a game between the tester and the implementation, based on the distance to the satisfaction of a test purpose, both in terms of number of transitions and potential control losses. Fairness assumptions are used to make those strategies winning and are proved sufficient to obtain the exhaustiveness of the test synthesis method, together with soundness, strictness and precision.

This paper opens numerous directions for future work. First, we intend to tackle partial observation in a more complete and practical way. One direction consists in finding weaker conditions under which approximate determinization [START_REF] Bertrand | A game approach to determinize timed automata[END_REF] preserves strong connectivity, a condition for the existence of winning strategies. One could also consider a mixture of our model and the model of [DLL + 10] whose observer predicates are clearly adequate in some contexts. Quantitative aspects could also better meet practical needs. The distance to the goal could also include the time distance or costs of transitions, in particular to avoid restarts when they induce heavy costs but longer and cheaper paths are possible. The fairness assumption could also be refined. For now it is assumed on both the specification and the implementation. If the implementation does not implement some outputs, a tester could detect it with a bounded fairness assumption [START_REF] Ramangalahi | Strategies for comformance testing[END_REF], adapted to the timed context (after sufficiently many experiments traversing some region all outputs have been observed), thus allowing a stronger conformance relation with egality of output sets. A natural extension could also be to complete the approach in a stochastic view. Finally, we plan to implement the results of this work in an open tool for the analysis of timed automata, experiment on real examples and check the scalability of the method.

Proof. The proof is the same as the one of Prop. 7, using Lemma A.6. Lemma A.8. For a repeatedly-observable specification S, Reach(OT ) \ Fail is repeatedly-observable.

Proof. We know that Traces(S) = Traces(P), hence for all σ ∈ Traces(P), out(P after σ) = out(S after σ). As Traces(DP) = Traces(P) by assumption, we also know that for all σ ∈ Traces(DP), out(P after σ) ⊆ out(DP after σ).

B Games

In this part the previous propositions are used to ensure that the sequence (W j i ) i,j defines a partial order, and covers the reachable part of our game. Proposition 14. There exists i, j ∈ N such that Reach(G OT ) \ Fail ⊆ W j i .

Proof. Let s ∈ Reach(G) \ Fail be a reachable configuration. Since i) Pass is reachable from s T 0 (by hypothesis); ii) there is a path from s back to the initial configuration (Corollary A.7), then Pass is reachable from s. Moreover, there is such a path with length bounded by the number of regions.

For each s ∈ Reach(G) \ Fail , we fix a finite path to Pass, and reason by induction on the length n of this path in order to prove that s ∈ W n 0 :

-Case n = 0: in this case s ∈ Pass = W 0 0 -Inductive case: we assume that the result holds for n, and take s with a path to Pass of length n + 1. Then s e -→ s for some e with act(e) ∈ Γ , and there is a path from s to Pass of length at most n, so that s ∈ W n 0 . Hence in the worst case s ∈ W n+1 0 . This proves our result.

Proposition 16.

is a partial order on Reach(G OT ) \ Fail.

Proof. is an order because it directly inherits the properties of ≤ N 2 . It is not total because several configurations can have the same rank.

The following lemma is the key allowing to ensure that rank-lowering strategies are winning on fair executions. Suppose there exists an infinite run ρ ∈ Outcome(s 0 , f ) ∩ Fair(G) such that ρ / ∈ Win(G). We denote r min the minimal rank obtained in Inf(ρ) and reg ∈ Inf(ρ) such that r(reg) = r min . For each prefix ν of ρ ending in a configuration s = (l, v) ∈ reg, we let (δ ν , a ν ) = f (ν). We consider three cases, following the definition of rank-lowering strategies:

-Assume last(ν) ∈ tPred(Pred Σc (W -(last(ν)))) and a ν ∈ Σ c . By Lemma B.9, there exists reg ∈ Inf(ρ) such that ν δν -→ s ν and s ν ∈ reg . Hence there exists a transition e such that act(e) = a ν . The system cannot delay more by definition of Outcome(s 0 , f ) and by fairness, reg e -→ reg and reg ∈ W -(last(ν))∩Inf(ρ), which contradicts the minimality of r min .

-Assume last(ν) ∈ tPred(W -(last(ν))) and a ν = ⊥. By Lemma B.9, there exists reg ∈ Inf(ρ) such that ν δν -→ s ν and s ν ∈ reg . By definition of the case, reg ∈ W -(last(ν)), thus the minimality of r min is contradicted.

-We finally consider the last case: as the duration in this one is maximal, we have last(ν) / ∈ tPred(W -(last(ν)) ∪ Pred Σc (W -(last(ν)))) and there are two cases to consider:

• if (W -(last(ν)) is undefined, then r(last(ρ)) = (0, 0) and ρ is winning, which is a contradiction; • otherwise, by Proposition 14, last(ν) ∈ tPred(Pred Σu (W -(last(ν)))) (this corresponds either to ftPred or to a W j+1 0

). Furthermore a ν = ⊥ and δ ν leads to the maximal delay successor region, which we call reg . By Lemma B.9, reg ∈ Inf(ρ). Hence, by definition of Inf, all regions between reg and reg are in Inf(ρ). In particular, a region reg ∈ Inf(ρ) such that reg e -→ reg ∈ W -(last(ρ)) and act(e) ∈ Σ u exists by definition of the case. Hence by fairness, reg ∈ Inf(ρ) and the minimality of r min is contradicted.

C Test case properties

Proposition 24. The test-case generation method is sound: for any specification S, it holds

∀I ∈ I(S), ∀(G, f ) ∈ T C(S), (I fails (G, f ) ⇒ ¬(I tioco S)).
Proof. Let S be a specification, I ∈ I(S) and (G, f ) ∈ T C(S). Suppose that I fails (G, f ), we will prove that ¬(I tioco S).

Since I fails (G, f ), there is a finite run ρ of Behaviour(G, f, I) such that last(ρ) ∈ Fail × S I and it is the first configuration of ρ in this set. Let σ = Trace(ρ). By construction of Fail , either σ = σ • δ (if the configuration of Fail reached corresponds to a faulty invariant) or σ = σ • a with a ∈ Σ ! (and Fail is reached). In both cases out(I after σ ) out(DP after σ ), and by definition ¬(I tioco DP).

As Traces(P) = Traces(DP) by exact-determinizability hypothesis, ¬(I tioco P). Finally, as Traces(P) = Traces(S), we have ¬(I tioco S), which concludes the proof.

Remark 1. Note that this proof is more general than the property, as it does not rely on the strategy. It hence proves the property for any strategy f and not only for rank-lowering ones. The key reason lies in fact in the structure of G, and ensures that any run reaching Fail has the correct form. Note that once again, the properties of the strategy are not used.

Proposition 27. The test case generation method is precise: for any specification S and test purpose T P it can be stated that ∀(G, f ) ∈ T C(S, T P), ∀σ ∈ Traces(Outcome(s G 0 , f )), G after σ ∈ Pass ⇔ (σ ∈ Traces(S) ∧ T P after σ ∩ Accept T P = ∅)

Proof. Let σ be in Traces(Outcome(s G 0 , f )). Then G after σ ∈ Pass if, and only if, the run ρ such that Trace(ρ) = σ (which is unique by determinism of G outside Fail ) is such that last(ρ) ∈ Pass, i.e. ρ ∈ Ex(DP) and last(ρ) ∈ Accept DP . Hence DP after σ ∈ Accept DP and as the determinization is exact, σ ∈ Traces(P) and P after σ ∈ Accept P , which gives by definition σ ∈ Traces(S) ∧ T P after σ ∩ Accept T P = ∅.

The proof uses only properties of the game, and once more does not rely on the precise strategy used. Proof. Let S be a specification, and I ∈ I(S) a non-conformant implementation. By definition of ¬(I tioco S), there exists σ ∈ Traces(S) and a ∈ R ≥0 ∪ Σ ! such that a ∈ out(I after σ) and a / ∈ out(S after σ). As S is repeatedly-observable, there exists δ ∈ R ≥0 and b ∈ Σ S obs such that σ • δ • b ∈ Traces(S). Because S is also non-blocking, if a is a delay, we can take b ∈ Σ S ! . Indeed, otherwise there would be no trace controlled by the implementation for any finite time (say, for time a).

It is possible to build a test purpose T P that accepts exactly the trace σ • δ • b. It suffices to send every transition that is not part of this trace to a sink location. As σ • δ • b ∈ Traces(S) it is also a trace of the product P = S × T P. As S is exactly determinizable and T P is deterministic, P is exactly determinizable by allowing enough resources to DP.

  is the transition relation. It is defined as the union of • the set of transitions corresponding to time elapses: it contains all triples ((l, v), δ, (l , v )) ∈ S A × R ≥0 × S A for which l = l and v = v + δ. By definition of S A , both v and v satisfy the invariant I(l). • the set of transitions corresponding to discrete moves: it contains all triples ((l, v), (e, X o ), (l , v )) ∈ S A × (E × 2 Xo ) × S A such that, writing e = (m, g, a, X p , m ), it holds m = l, m = l , v |= g, and v = v [X p ∪X o ←0] . Again, by definition, v |= I(l) and v |= I(l ).

Fig. 1 .

 1 Fig. 1. A conveyor belt specification.

y

  Fig. 2. A test purpose for the conveyor belt.

Example 3 .Fig. 3 .

 33 Fig. 3. Product of the conveyor belt specification and the presented test purpose.

Example 4 .

 4 Fig. 4. A deterministic approximation of the product.

  a) with a ∈ Σ c s.t. there exists e ∈ E with act(e) = a and s δ -→ e -→ t with t ∈ W -(s), and δ is minimal in the following sense: if s δ -→ e -→ t with t ∈ W -(s) and δ ≤ δ, then v + δ and v + δ belong to the same region;

Proposition 26 .

 26 The test generation method is strict: given a specification S,∀I ∈ I(S), ∀(G, f ) ∈ T C(S), ¬(Behaviour(G, f, I) tioco S) ⇒ I fails (G, f )This method also enjoys a precision property: traces leading the test case to Pass are exactly traces conforming to the specification and accepted by the test purpose. The proof of this property uses the exact encoding of the Accept states and the definition of Pass. As the previous two, it then propagates the property through the different test artifacts.

  It comes ∀σ ∈ Traces(OT ), out(S after σ) ⊆ out(OT after σ) as OT only adds traces to DP. Hence for all s ∈ Reach(S OT ) \ Fail , there exists µ ∈ Seq(OT ) s.t. s µ -→ ∧Trace(µ) / ∈ R ≥0 . Indeed, there exists σ ∈ Traces conf (OT ) such that s = OT after σ (as OT is deterministic outside of Fail ) and for s ∈ S after σ, there exists µ such that s µ -→ ∧Trace(µ ) / ∈ R ≥0 . It suffices to take µ ∈ pSeq(OT ) such that Trace(µ) = Trace(µ ), and by the previous trace-inclusion property, such a trace exists.

Proposition 26 .

 26 The test generation method is strict: given a specification S, ∀I ∈ I(S), ∀(G, f ) ∈ T C(S), ¬(Behaviour(G, f, I) tioco S) ⇒ I fails (G, f ) Proof. Let S be a specification, I ∈ I(S) and (G, f ) ∈ T C(S). Suppose that ¬(Behaviour(G, f, I) tioco S). We want to show that I fails (G, f ). By definition of ¬(Behaviour(G, f, I) tioco S), there exist σ ∈ Traces(S) and a ∈ out(Behaviour(G, f, I) after σ) \ out(S after σ) Since DP is an exact determinization of P we have the following equalities: Traces(S) = Traces(P) = Traces(DP) = Traces conf (OT ). Since a ∈ R ≥0 ∪ Σ ! , σ • a ∈ Traces(OT ) as invariants have been removed, and the automaton has been completed on Σ ! with transitions to Fail). Hence σ • a ∈ Traces(Ex fail (OT )). Thus, for ρ ∈ Behaviour(G, f, I) such that Trace(ρ) = σ • a, last(ρ) ∈ Fail and I fails (G, f ).

Proposition 28 .

 28 The test generation method is exhaustive: for any exactly determinizable specification S and any implementation I ∈ I(S) making fair runs ¬(I tioco S) ⇒ ∃(G, f ) ∈ T C(S), I fails (G, f ).

  We thus obtain Traces(DP) = Traces(P) and σ • δ • b ∈ Traces(DP). Hence, the minimal elements of Pass are OT after σ • δ • b.From OT a test case (G, f ) can be built, with f a rank-lowering strategy. By assumption, the implementation is playing fair runs, hence f is winning. So there exists ρ ∈ Outcome(s G 0 , f ) such that Trace(ρ) = σ • δ • b, and thus there exists ρ ∈ Outcome(s G 0 , f ) such that Trace(ρ ) = σ. By assumption, σ • a ∈ Traces(I), and depending on the nature of a:-If a ∈ Σ ! then σ • a ∈ Outcome(s G 0 , f ) as G is complete on Σ ! . Hence σ • a ∈ Behaviour(G,f, I) and as σ • a / ∈ Traces(S) and the determinization is exact, σ • a / ∈ Traces conf (OT ) and G after σ • a ∈ Fail . Hence I fails (G, f ). -If a is a delay, then a > δ, and b ∈ Σ ! . As b is controlled by the implementation, and there is no invariant in G, σ • a ∈ Outcome(s G 0 , f ). Hence σ • a ∈ Behaviour(G, f, I) and as σ • a / ∈ Traces(S) and the determinization is exact, σ • a / ∈ Traces conf (OT ) and G after σ • a ∈ Fail . Hence I fails (G, f ).

For this and the following definitions, we may omit to mention superscripts when the corresponding automaton is clear from the context.

The sequence (W j i )i is non-decreasing, and can be computed in terms of clock regions; hence the limit exists and is reached in a finite number of iterations [CDF + 05].

Appendix

We conduct here the proofs of the different claims. They are separated according to the corresponding parts of the article: testing framework, games, and test-case properties.

A Test framework

First, we prove the claim on the strong-connectivity of the reachable part of a specification semantics. This property is made quite intuitive by the introduction of always-reachable ζ-transitions. As it grounds our approach, we still provide a formal proof.

Proposition 7. Let S be a specification with restarts. Then Reach(T S ) is stronglyconnected.

Proof. Let s be a configuration of T S reachable from s S 0 . By hypothesis, there exists a finite partial execution starting in s which trace contains ζ. This trace leads to the configuration s S 0 hence any reachable configuration of T S is reachable from s, and we conclude that the reachable part of T S is strongly-connected.

We now prove some properties of the product between specifications and test purposes.

Proposition A.1. Let S be a specification and T P a test purpose on this specification. Then Seq(S × T P) = Seq(S)

Proof. It suffices to note that the set of sequences of the product of two OTAIOs is the intersection of the sequences of the two original OTAIOs [START_REF] Bertrand | A game approach to determinize timed automata[END_REF], so that Seq(S × T P) = Seq(S) ∩ Seq(T P); we also note that T P is complete, and hence it accepts any sequence. By projection on traces, we immediately get:

Corollary A.2. Let S be a specification, and T P a test purpose. S and S × T P are trace-equivalent.

Corollary A.3. Let S be a specification, T P a test purpose and T S×T P its associated timed transition system. The reachable part of T S×T P is stronglyconnected.

Proof. This proof is derived from the proof of Prop. 7. Although they are really close, we have to do it again as the product does not ensure any relation on the semantics. Let ((l 1 , l 2 ), v) be a reachable configuration of T S×T P . There exists a finite partial execution starting in (l 1 , v) whose trace contains ζ, and thus by Corollary A.2 there exists a finite partial execution starting in ((l 1 , l 2 ), v) whose trace contains ζ. Hence this transition leads to the configuration s 0 = (l S×T P 0 , 0). It comes that there exists a finite partial execution from ((l 1 , l 2 ), v) to s 0 . Hence any reachable configuration of T S×T P is reachable from ((l 1 , l 2 ), v). It can then be concluded that the reachable part of T S is strongly-connected.

The following properties concern the objective-centered tester. They mainly amount to proving that the objective-centered tester keeps the interesting properties of the product, and that its traces are related to those of the previous automata.

Proposition A.4. Let DP be the exact determinization of the product P between a specification and a test purpose, and OT its associated objective-centered tester. Then Traces(DP) = Traces conf (OT ).

Proof. An execution is in Ex conf (OT ) if it avoids the verdict Fail . This amounts to avoiding the location Fail and respecting the invariants of DP. By construction of OT , this corresponds exactly to the runs of DP.

Lemma A.5. Given an objective-centered tester OT , we have

Proof. Let ρ ∈ Ex fail (OT ). Consider the longest prefix ρ of ρ that does not reach Fail , and let e be the transition taken after ρ in ρ. Two cases should be considered:

-If e is a delay transition, then it violates the invariant of the location in DP.

By determinism of DP, DP after Trace(ρ ) is a singleton. Hence the same delay is not available after ρ in DP.

-If act(e) ∈ Σ ! then this output is not specified in the current location of DP.

By determinism of DP, DP after Trace(ρ ) is a singleton. Hence transition e is not possible after ρ in DP.

In both cases Trace(ρ) / ∈ Traces conf (OT ). As this holds for any run of Ex fail (OT ) we have the desired property.

Lemma A.6. Let OT be an objective-centered tester. For any location l in L OT \ {Fail} there exists a finite partial execution ρ ∈ pEx(OT ) starting in l and containing a ζ.

Proof. The same result holds from any state in S, and Traces(S) = Traces(S ×T P). The result follows by exact determinizability of the product S × T P.

This lemma is the reason why our method assumes exact determinizability, as we can't ensure in general that the restart will remain reachable: if determinization is approximated, some traces might be lost.

Corollary A.7. Let OT be an objective-centered tester and T OT its associated timed transition system. Then Reach(T OT ) \ Fail is strongly-connected.

Lemma 18. If OT is repeatedly-observable, then for all ρ = ((s i , γ i , s i+1 )) i∈N ∈ Ex(G) ending with an infinite sequence of delays, we have

Proof. We show this lemma by contradiction. Assume that for some ρ ∈ Ex(G), we have

Let ρ max be the shortest prefix such that no transition is enabled after this prefix along ρ (it exists because E is finite and there is only a finite number of these prefixes per element of E). Consider any prefix ρ of ρ strictly containing ρ max ; there is no partial sequence µ such that last(ρ ) µ -→ and Trace(µ) / ∈ R ≥0 , as there is no time successor of last(ρ ) with an enabled transition. This contradicts the repeated-observability of OT out of Fail (as G and OT are the same automaton).

Proposition 21. Rank-lowering strategies are winning on Fair(G) (i.e., all fair outcomes are winning).

In order to make this proof, we reason on regions. For this purpose we extend to regions the notions of executions and enabled transitions. We furthermore note that a region is included in any W j i it intersects. We first prove the following lemma: Lemma B.9. Let ρ ∈ Fair(G) be a fair execution and reg ∈ Inf(ρ). For any prefix ν of ρ ending in reg, and any rank-lowering strategy f , noting f (ν) = (δ, a), we have ν δ -→ s ∈ reg and reg ∈ Inf(ρ).

Proof. By definition of a rank-lowering strategy, δ is a possible delay after last(ν). Hence there exists s and reg such that ν δ -→ s ∈ reg . By definition of rank-lowering strategies, it is always the same reg for each ν. If reg = reg then we have our result. Otherwise, by definition of outcomes, there is no transition labelled with a controllable transition leaving reg, and by our fairness assumption, there exists a (strict) time successor reg t -→ reg of reg such that reg ∈ Inf(ρ). If reg = reg we have our result; otherwise, by defintion of outcomes, reg is a time predecessor of reg , and applying the same arguments to reg will create an induction (as by definition of rank-lowering strategies, the strategy after going from ν to reg is to delay to reg ). As there is only finitely-many regions between reg and reg , we have our result by the induction principle.

With this lemma, the proof of the main proposition is made easier.

Proof (of Prop. 21). Let T = (S, s 0 , Γ, → T ) be the timed transition system associated with G = (L, l 0 , Σ u Σ c , X, I, E). Let f be a rank-lowering strategy. We want to prove that Outcome(s 0 , f ) ∩ Fair(G) ⊆ Win(G). We proceed by contradiction.


Yue Wang
email: yue.wang@inria.fr

Gang Zheng ab Denis Efimov Abc
email: denis.efimov@inria.fr

Wilfrid Perruquetti
email: wilfrid.perruquetti@inria.fr

Differentiator Application in Altitude Control for an Indoor Blimp Robot

Keywords: Differentiator, Flying robots, Output feedback control, Control of switched system

This paper presents design of altitude controller with disturbance compensation for an indoor blimp robot and its realisation. Due to hardware restrictions, the altitude control behaviour of blimp is modelled as a switched system with a constant time-delay complemented with uncertain bounded disturbances. In order to achieve state estimation, four differentiators are applied and compared, then HOMD (homogeneous finite-time) differentiator is chosen as an observer for vertical velocity and switching signal estimation. Next, a predictor-based controller is conceived, and in order to compensate the perturbation, the method for disturbance evaluation is designed still with the help of HOMD differentiator. Control scheme is implemented by Matlab Simulink, and finally, the performance of blimp altitude controller is verified in experiments.

Introduction

Robotics is a quickly developing area of science and technology nowadays. Frequently, robots are developed for replacing humans in dangerous operating conditions or for optimisation of manufacturing expenses. According to their operating environment, robots can be classified into two types: indoor or outdoor, since depending on that they have different restrictions on dimensions, noise level, actuators and sensors used. Among the flying robots it is worth to mention airships or blimps which are lighterthan-air (LTA) aircrafts, for their long endurance in air, high payload-to-weight ratio, and low noise level features, compare with fixed-wing aircrafts and rotor-wing aircrafts [START_REF] Li | Airship dynamics modeling: A literature review[END_REF].

In the present work, a small blimp robot for indoor operation is considered. This robot has to possess a good autonomy operation time and demonstrate a low noise production level. The blimp can be used to do indoor long-term monitoring, or unknown dangerous environment exploring etc. In order to accomplish those complex goals, it has to be well controlled under different scenarios, and stabilising the blimp at a desired altitude is the basic requirement. Thus, the problem of robust altitude stabilisation is considered in this work. To this end, based on real data obtained for the blimp platform available in our laboratory, a switched time-delay model of altitude dynamics is identified. Different differentiators are applied and compared for state and disturbance estimation purposes. Next, predictor-based control is designed. The obtained solutions are experimentally verified.

This paper is organised as follows. In the next section, some related works are introduced and discussed. Structure of our blimp system is presented in section 3, the altitude model and its parameter identification are also discussed in this section. In section 4, in order to realise state observation, four differentiators are briefly reviewed and compared to select the most appropriate one. A controller design based on predictor is illustrated; moreover, the method to estimate and compensate disturbance of system is conceived. Afterwards, we focus on the real blimp, and using a motion capture system to enhance the control scheme, experiment results are presented in section 5. Finally, conclusion comes in section 6.

Related Works

Researchers have put increasing attention on autonomous blimp robots over the last few years; they use airships as experiment platforms to study information acquisition, robot control and navigation algorithms.

Many of these blimps are of large scale, which can only be tested outdoor. They normally have a payload of several kilograms, which allow them to carry plenty of high-precision sensors to do experiments. For instance, [START_REF] Hygounenc | The autonomous blimp project of laas-cnrs: Achievements in flight control and terrain mapping[END_REF] used blimp in their terrain mapping research, achieved positioning of blimp in the three-dimensional space with a centimetre accuracy. [START_REF] Kantor | Collection of environmental data from an airship platform[END_REF] discussed the use of solar energy as a renewable source of power for airships, which they used for environmental data sampling and monitoring. [START_REF] Rao | A flight control and navigation system of a small size unmanned airship[END_REF] proposed a fuzzy logic controller which was based on the dynamics of the vehicle for heading angle and altitude control; their robot realised 3D path tracking with acceptable error.

Furthermore, other researchers made various studies of blimps in indoor environments, such as localisation of robot, obstacle avoidance algorithm, trajectory planning and path tracking control. [START_REF] Wyeth | An autonomous blimp[END_REF] used landmark navigation system to navigate their blimp. [START_REF] Fukao | Image-based tracking control of a blimp[END_REF] installed a camera on airship for surveillance system and illustrated an image-based tracking control for an indoor blimp. [START_REF] Green | A competition to identify key challenges for unmanned aerial robots in near-earth environments[END_REF] also used camera on blimp to realise obstacle avoidance function. [START_REF] Zufferey | Flying over the reality gap: From simulated to real indoor airships[END_REF] used neuronal controllers in simulation to map visual input into motor commands to accelerate the movement of flying robot while avoiding collisions. [START_REF] Ko | Gaussian processes and reinforcement learning for identification and control of an autonomous blimp[END_REF] combined their Gaussian processes enhanced model to reinforcement learning and designed a controller for blimp's yaw and yaw rate control. Rottmann, Zitterell, Burgard, Reindl, and Scholl (2007) also used reinforcement learning to design a controller which can be used to control blimp's altitude without knowing the specific dynamics of the system or other environmental parameters. López [START_REF] López Fernández | Developing a low-cost autonomous indoor blimp[END_REF] designed PID controller together with fuzzy logic controller to realise airship's altitude control; the ultrasonic sensor information is used to accomplish collision avoidance.

As we can see from the related works, some of them did not propose models for indoor blimp robot, while the others built complex models, which need lots of experimental data to identify the parameters but there are still disturbances from the environment which cannot be modelled. Since an indoor blimp robot is considered in this work, it has to be sufficiently small, and its payload is limited. This limits possible quantity of sensors mounted on the robot and computational complexity of the control and estimation algorithms. That is why we intend to use a simple model for blimp's altitude control task, and design a controller which can estimate and compensate the disturbances in real time [START_REF] Guerra | ε-invariant output stabilization: Homogeneous approach and dead zone compensation[END_REF], so that the accuracy of control is assured while the complexity is reduced to a minimum. Our developed modelling, estimation and control algorithms are based on real data measurements and experimental validation performed on real platform, which is described in the next section.

Blimp System

We will consider a blimp robot for indoor operation, with a Mylar balloon of 110cm length and 70cm of maximum diameter. Helium is used to inflate the balloon so it has a payload of about 160 grams. Therefore, only low-weight sensors and actuators can be integrated in an embedded micro-system, which means the measurement of on-board sensors cannot be very accurate. On the latest control board, the micro-controller used is STM32, which controls four mini motors -two work in the horizontal plane and the other two work in the vertical direction. The wireless communication between control board on blimp and ground PC is realised by a pair of XBee modules. In order to improve the altitude measurement accuracy, the high-precision position and pose capturing system OptiTrack is applied to enhance the blimp system. It uses infrared waves to capture the markers mounted on blimp control board, and solves the blimp position with a precision of 1mm.

Altitude Control Model

In order to develop the control of blimp, the 6 DOF kinematic model is considered. Fig.

(1) shows the coordinate and symbols of blimp variables [START_REF] Rao | A flight control and navigation system of a small size unmanned airship[END_REF].

navigation frame R n (O n , X n , Y n , Z n ) is denoted as η = x y z φ θ ψ T .
The kinematic model between frame R b and R n is given by η = J(η)ξ (1)

where J(η) is the transition matrix from R b to R n . Following investigation of [START_REF] Hygounenc | The autonomous blimp project of laas-cnrs: Achievements in flight control and terrain mapping[END_REF] that the state parameters of airship dynamics in lateral and longitudinal motions are weakly dependent, the dynamics of blimp can be split into two subsystems: the one within longitudinal plane (η long = x z θ T , ξ long = U W Q T ), and the one within lateral plane (η lat = y φ ψ T , ξ lat = V P R T ). For blimp dynamics in longitudinal plane, it is imperative to stabilise the airship at a desired altitude since it is the fundamental demand of blimps to perform complex tasks. In fact, altitude control is already a complex task as a blimp is really sensitive to environment changes and its behaviour is easily influenced by many factors like the payload change, battery level, air flow disturbances, and temperature. First, in this work, we intend to model the altitude control behaviour of blimp and identify the parameters. To this end, the dynamical equation in the vertical axis is considered. The blimp is subjected to its gravity, buoyancy, the propulsive force by its vertical motor, and the air resistance when it moves. So for the dynamical equation along the vertical axis, based on Newtonian principles, there is

mz = F p + F b -G -F r (2)
where z is the altitude of blimp to the reference plane, F p , F b , G, F r represent propulsive force, buoyancy, gravity, and air resistance, respectively. The equation is simplified with the following assumptions:

• the buoyancy and gravity of blimp do not change wherever it is in the testing environment; • the buoyancy and gravity of blimp are approximately equal;

• the air resistance is proportional to blimp velocity (the blimp has low speed);

• the propulsive force is proportional to square of motor rotation speed, which is modelled as input; • the delay between emission of control signal and the rotation speed change of the motor is denoted as τ .

So, Equation ( 2) is simplified as

z(t) = a ż(t) + bu(t -τ ) + c (3)
where c represents the resultant force of buoyancy and gravity of blimp, a, b, and τ are the parameters which have to be estimated to validate the model.

Parameter Identification

In order to identify the model parameters, the input u for vertical motor is set as a step signal, and blimp altitude is measured using the OptiTrack system with a rate of 100Hz. In our tests there is a time-varying delay measured from 0.2 to 0.4s in blimp control loop due to the wireless transmission and motor settling time; therefore, the delay has to be manually measured in different tests.

After the delay τ is measured, the parameters a, b can be identified. For a step input with gain N , assume at the beginning, blimp is static, i.e. ż(0) = 0, c = 0, using Laplace transform at the differential equation (3), we get

Z(s) = N b s 2 (s -a) e -τ s + z(0) s (4)
Using inverse Laplace transform, we get

z(t) = z(0) + N ( b a 2 e a(t-τ ) - b a 2 - b a (t -τ )) (5)
Then, the Levenberg-Marquardt nonlinear least squares algorithm is used to estimate parameters in the given function [START_REF] Seber | Nonlinear regression[END_REF].

It is worth to mention that the motor rotation speed is not the same in practice when it rotates in forward/backward direction with the same input value due to motor defect. Besides, the air resistance coefficient differs when the blimp moves upward and downward on account of the installation of control board at bottom of balloon.

Therefore, step input tests with positive and negative final value are made to separately identify parameters a and b; they have to be switched according to blimp state (direction of movement) and motor command. See Table 1 for the parameter identification result. Note that a is related to the air-resistant coefficient, and b is related to the propulsive force.

System Description

The parameter identified in Section 3.2 can be used to establish a nominal model for blimp altitude control system. Then we intend to use a disturbance term to represent the errors between nominal model and real one, which includes the errors caused by:

• Nominal model parameter identification inaccuracy;

• Difference between blimp buoyancy force and gravity;

• Helium leak of the balloon;

• Airflow perturbation to balloon;

• Variation of time-delay in the control loop;

• Temperature change in testing environment;

• Other environmental disturbances which are impossible to be accurately modelled.

Therefore, the blimp altitude control system studied in this paper is considered as a switched system with a constant time-delay complemented with uncertain bounded disturbances [START_REF] Guerra | ε-invariant output stabilization: Homogeneous approach and dead zone compensation[END_REF]. Blimp altitude z and velocity in vertical axis ż are chosen as the state vector X = z ż T ; the system can be written in state-space form as the combination of nominal model and real-time estimated disturbance term:

Ẋ(t) = A σ X(t) + B σ u(t -τ nom ) + B σ d(t) y(t) = CX(t) σ ∈ P = {1, 2, 3, 4} (6)
where

A σ = 0 1 0 a σ , B σ = 0 b σ ,
σ =       
1, u ≥ 0 and ż ≥ 0 2, u ≥ 0 and ż < 0 3, u < 0 and ż ≥ 0 4, u < 0 and ż < 0 (7)

From the results in Section 3.2, there is (Table 1)

a 1 = a 3 = -0.035 a 2 = a 4 = -0.0366 b 1 = b 2 = 0.0628 b 3 = b 4 = 0.0424 (8)

Altitude Controller Design

In order to solve the altitude stabilisation problem for system (6), an output feedback should be designed. For this purpose, in this work, the following steps are proposed:

1) Design an observer which can estimate state and switching signal of time-delay switched system (6). 2) Design a controller which stabilises the system in the nominal disturbance-free case. 3) Modify or develop the control algorithm to compensate the disturbance.

Differentiator Observer Design

As the sensors in system can only measure blimp altitude, in order to use state feedback to design the closed-loop system, both components of the state z and ż have to be known. Moreover, the switching signal σ has to be also estimated to give commutation information about the system. As σ is determined by the velocity ż and command u (see criteria ( 7)), ż has to be calculated.

The system studied is a switched system with a constant time-delay complemented with uncertain bounded disturbances as described in Section 3.3. A Luenberger observer can be used to estimate all the states, but the switching feature of system increases the complexity of observer design and the precision of estimation result cannot be guaranteed. Considering the fact that required state is the first-order derivative of measurement, a differentiator is more suitable for the state estimation task.

For this purpose four different differentiators are considered: High-Gain, HOSM (high-order sliding mode), HOMD (homogeneous finite-time), and algebraic-based (ALIEN) differentiator. First, a brief overview of these differentiators is given, and then, tests are made to compare their performances in our application scenario.

ALIEN Differentiator

The algebraic differentiator is proposed in the paper of Sira-Ramirez and [START_REF] Sira-Ramirez | An algebraic state estimation approach for the recovery of chaotically encrypted messages[END_REF]. Consider a signal x(t) which is assumed to be analytic on a finite-time interval. The truncated Taylor expansion of x(t) is

x N (t) = N k=0 x (k) (0) t k k! (9)
The Laplace transform of ( 9) is

X N (s) = N k=0 x (k) (0) s k+1 (10)
Multiplying both sides of (10) by d ν ds ν s N , ν = 0, 1, . . . , N , we get

d ν s N ds ν X N (s) = d ν ds ν ( N k=0 x (k) (0)s N -k-1 ) (11)
According to Fliess and Sira-Ramírez ( 2003), ( 11) is independent of unknown initial conditions and x(0), . . . , x (k) (0) are linearly identifiable. Therefore, the k-th-order derivative x (k) (0) can be estimated by taking inverse Laplace transform of (11) over a time window T .

The ALIEN differentiator has the following form according to [START_REF] Mboup | A revised look at numerical differentiation with an application to nonlinear feedback control[END_REF]:

     x1 = 2 1 0 (2 -3τ )y(t -τ T )dτ x2 = -6 T 1 0 (1 -2τ )y(t -τ T )dτ x3 = 60 T 2 1 0 (1 -6τ + 6τ 2 )y(t -τ T )dτ (12)
where T represents the selected window, y(t) is the signal and x1 , x2 , x3 , respectively, represent the zero-, first-, and second-order derivative estimation. This algebraic differentiator does not require any knowledge about the noise, and it provides explicit formula, and hence it is easy to be implemented in real-time applications. It is worth to notice that the integrals in formulas can be considered as low-pass filters, so high-frequency noises in the measurement signal can be attenuated by them. In addition, the estimates are obtained in a finite time T .

High-Gain Differentiator

Consider a single-input-single-output nonlinear system, having a uniform relative degree equal to the dimension of the state vector (A. [START_REF] Dabroom | Numerical differentiation using high-gain observers[END_REF], then it can be transformed into normal form [START_REF] Isidori | Nonlinear control systems[END_REF]:

ẋ = Ax + B[a(x)u + b(x)] y = Cx (13)
where (A, B, C) are canonical form matrices, and a, b : R n → R are Lipschitz continuous functions. Let u : R + → R be a bounded known input, then the observer equations take the following form:

ẋ = Ax + B[a 0 (x)ψ(x, t) + b 0 (x)] + H(y -C x) (14)
where a 0 (x) and b 0 (x) are nominal models of nonlinear functions a(x) and b(x), and H is the observer gain. It is shown in [START_REF] Esfandiari | Output feedback stabilization of fully linearizable systems[END_REF] that when the observer gain is chosen as

H T = α1 α2 2 . . . αn n (15)
then, the state reconstruction is achieved, where is a small positive parameter, and the positive constants α i are chosen to make the roots of

s n + α 1 s n-1 + • • • + α n-1 s + α n = 0 (16)
having negative real parts (see A. M. [START_REF] Dabroom | Discrete-time implementation of high-gain observers for numerical differentiation[END_REF]. The choice of H sets the eigenvalues of (A-HC) at 1/ times the roots of ( 16). According to [START_REF] Esfandiari | Output feedback stabilization of fully linearizable systems[END_REF], the estimation error will decay to O( ) after a short transient period.

HOSM Differentiator

The HOSM differentiator is proposed by [START_REF] Levant | Higher-order sliding modes, differentiation and output-feedback control[END_REF]. Let input signal f (t) be consisting of a bounded Lebesgue-measurable noise with unknown features, and a unknown base signal f 0 (t) with the n-th derivative having a known Lipschitz constant L > 0. Then, a recursive scheme can be used to get the n-th-order differentiator:

ż0 = v 0 , v 0 = -λ 0 |z 0 -f (t)| n/(n+1) sign(z 0 -f (t)) + z 1 , ż1 = v 1 , v 1 = -λ 1 |z 1 -v 0 | (n-1)/n sign(z 1 -v 0 ) + z 2 , . . . żn-1 = v n-1 , v n-1 = -λ n-1 |z n-1 -v n-2 | 1/2 sign(z n-1 -v n-2 ) + z n żn = -λ n sign(z n -v n-1 ) (17)
Note that for l < k, the k-th-order differentiator provides for a better accuracy of l-th order derivative, than the l-th-order differentiator. So, in this paper, a secondorder differentiator is used to estimate the first-order derivative of blimp's altitude as proposed by [START_REF] Levant | Higher-order sliding modes, differentiation and output-feedback control[END_REF], for input f with | ...

f | ≤ L: ż0 = v 0 , v 0 = -3L 1/3 |z 0 -f | 2/3 sign(z 0 -f ) + z 1 ż1 = v 1 , v 1 = -1.5L 1/2 |z 1 -v 0 | 1/2 sign(z 1 -v 0 ) + z 2 ż2 = -1.1Lsign(z 2 -v 1 ) (18)

HOMD Differentiator

Consider a nonlinear system of the form:

ξ = η(ξ, u) y = h(ξ) ( 19
)
where ξ is the state, u is the control input which is sufficiently smooth, and y is the output. Assume that ( 19) is locally observable and there exists a local state coordinate transformation and an output coordinate transformation which transform the nonlinear system (19) into the following canonical form:

ẋ1 = x 2 + f 1 (x 1 , u, u, . . . , u (r) ) ẋ2 = x 3 + f 2 (x 1 , u, u, . . . , u (r) ) . . . ẋn = f n (x 1 , u, u, . . . , u (r) ) y = x 1 (20)
where x ∈ R n is the new state and r ∈ N. The observer is designed as follows:

dx 1 dt = x2 + f 1 (x 1 , u, u, . . . , u (r) ) -χ 1 (x 1 -x1 ) dx 2 dt = x3 + f 2 (x 1 , u, u, . . . , u (r) ) -χ 2 (x 1 -x1 ) . . . dx n dt = f n (x 1 , u, u, . . . , u (r) ) -χ n (x 1 -x1 ) (21)
where the functions χ i will be defined in such a way that the observation error e = x-x tends to zeros in finite time (see [START_REF] Perruquetti | Finite-time observers: application to secure communication[END_REF]:

χ i (e 1 ) = -k i e 1 αi (22)
where for any real number x ∈ R:

x α = |x| α sign(x) (23)
and the parameters α i can be chosen as

α 1 = α ∈ n -1 n , 1 , α 2 = 2α -1, α 3 = 3α -2, . . . α n = nα -(n -1) (24)
Then, the error dynamics of observer ( 21) become

ė1 = e 2 -k 1 e 1 α ė2 = e 3 -k 2 e 1 2α-1 . . . ėn = -k n e 1 nα-(n-1) (25)
Consider a dilation with weights (r 1 , r 2 , . . . , r n ) = (1, α 1 , . . . , α n-1 ), system (25) is homogeneous of degree d = α -1 with respect to these weights [START_REF] Bernuau | On homogeneity and its application in sliding mode control[END_REF]. In order to prove stability and convergence of this differentiator the following Lyapunov function can be used:

V α (e) = σ T P σ, σ = e 1 1/r1 e 2 1/r2 . . . e n 1/rn T = e 1 e 2 1/α . . . e n 1/((n-1)α-(n-2)) T ( 26
)
where P is the solution of the Lyapunov equation:

A T 0 P + P A 0 = -I A 0 =      -k 1 1 0 0 -k 2 0 . . . 0 . . . . . . . . . 1 -k n 0 . . . 0      (27)
and the gains k i are chosen such that A 0 is Hurwitz. Then, there exists ∈ [1-1 n-1 , 1), such that, for all α ∈ (1 -, 1), system (25) is globally finite-time stable [START_REF] Perruquetti | Finite-time observers: application to secure communication[END_REF].

Differentiator Comparison

The High-Gain, HOSM and HOMD differentiator can be written in a similar formulation according to [START_REF] Perruquetti | Homogeneous finite time observer for nonlinear systems with linearizable error dynamics[END_REF]. In our case, the second-order differentiator can be written as

ẋ1 = -k 1 x 1 -y α + x 2 ẋ2 = -k 2 x 1 -y 2α-1 + x 3 ẋ3 = -k 3 x 1 -y 3α-2 (28)
where y represents the measurement, x 1 , x 2 , and x 3 , respectively, represent the zero-, first-, and second-order derivative estimation.

The gains k 1 ,k 2 and k 3 are selected in order to ensure that the corresponding polynomial is Hurwitz, and:

• For High-Gain differentiator α = 1; • For HOMD differentiator α ∈ ( 2 3 , 1); • For HOSM differentiator α = 2
3 . This formula is easy to be implemented, and the parameter of HOMD differentiator is chosen as α = 5 6 in tests.

Step altitude control is applied to compare the performances of the four differentiators.

First, it is the comparison of zero-order derivative estimation result: Then it is the comparison of first order derivative estimation result: The 'Real' curve is generated using the model with parameters identified in Section 3.3, and the sampling rate is 100Hz. In the 'Measurement' of altitude a white noise is added to simulate measuring error, which has a signal-to-noise ratio (SNR) of 25dB.

From Fig. 2, it is clear that all the four differentiators can estimate the altitude signal after certain periods, but the ALIEN converges slower than the three others. This is due to the use of integrator which introduces delay of estimation in realtime applications. ALIEN differentiator can converge faster if the window T of ( 12) is smaller, but then it would be more sensitive to the noise. As the system studied in this paper has a time-varying delay which is non-ignorable, it is preferable to use a differentiator which converges faster.

As shown in Fig. 3, the HOMD, HOSM and High-Gain differentiator have similar performances. But it is worth to mention that HOSM has bigger fluctuation than the others after they converge, which means that HOSM is less robust to noises. HOMD has finite-time stability compared to High-Gain differentiator.

Therefore, in consideration of the convergence time and robustness to noises, the HOMD differentiator is used in this paper for ż estimation. Then, the value of σ can be evaluated by the sign of u and ż using criteria: where σ is estimated according to (29), and d is an estimate of the disturbance, which is described below. 2) Assign the controller output based on predictor result, disturbance term and desired state X set :

X = [ x1 x2 ] T σ =        1, u ≥ 0
u(t) = K σ(X set -X(t + τ nom )) -d(t + τ nom ). (31)
From ( 30) and (31), it is clear that the disturbance term d(t) has to be estimated in real time and predicted for the time interval [t, t + τ nom ].

P -1 0 P -1 (A σ -B σ K) T + (A σ -B σ K)P -1 ≺ 0, ∀σ ∈ P (36) Let W = KP -1 P -1 0 P -1 A T σ -W T B T σ + A σ P -1 -B σ W ≺ 0, ∀σ ∈ P (37)
where decision variables are P -1 and W . If there exists solution for LMI (37), then the switched system ( 6) is globally uniformly exponentially stable.

A feasible solution of P and K can be solved by YALMIP toolbox of Matlab [START_REF] Löfberg | Yalmip : A toolbox for modeling and optimization in matlab[END_REF]:

   P = 0.

Implementation on Real Blimp

As it has been indicated in Section 3, when implementing the designed altitude control algorithm on the real blimp, the OptiTrack camera system is used to improve the altitude measurement accuracy.

OptiTrack-Enhanced Control System

The enhanced control system scheme is shown in Fig. 4. According to this scheme, first, OptiTrack captures and tracks the blimp, then it reconstructs the position and pose of blimp (cameras are calibrated and reference frame is set beforehand in software) and sends message to PC where the controller is implemented in Matlab Simulink. In Simulink program, the differentiator in observer calculates ż and observer gives estimation of switching signal σ (Section 4.1). Next, disturbance is estimated in real time by the filter (Section 4.3), then compensated in predictor-based controller (Section 4.2). Finally, the command of motors is sent to blimp control board via XBee wireless communication and the control loop is closed.

As presented in Section 4, the designed altitude controller is not complex; it has less than 100 lines of code, and it does not require high computational capacity to solve the command signal. Moreover, the size of program is less than 64kB. Therefore, the Simulink program can be easily transformed to be used on embedded microprocessor.

Results

Experiments are made in a normal office room of height 3m. Five infrared cameras are installed on ground to form a circle, with their optic axis inclined upward to the vertical axis which passes the centre of the circle. The blimp floats inside the circle formed by the camera system, and when it moves to reach the desired altitude, it does not leave the view of cameras.

In the experiments, we have to adjust the additional weight for the blimp, in order to introduce disturbance for blimp system; the additional weight is set to make the blimp buoyancy force greater than its gravity, which means the blimp keeps rising if there is no command signal. A lightweight string has been attached to blimp control board to avoid the blimp from hitting the ceiling, and the string does not affect the blimp movement except when the blimp altitude exceeds the upper bound. Fig. 6(a) shows another test in which we add some additional weight to the blimp at 44.6s to make the blimp gravity greater than buoyancy force. It is shown in the figure that the blimp altitude control is adapted to the disturbance change, and blimp returns to desired altitude with an error less than ±5cm within 7s. Fig. 6(b) shows the disturbance estimation result d(t + τ nom ). It is clear that d(t + τ nom ) can reflect the disturbance caused by difference between blimp buoyancy force and gravity. Before the moment of 44.6s, the c term in dynamical equation ( 3) is positive, and then it changes the sign, as with the disturbance estimation result.

Experiment results confirm that our designed altitude control method with disturbance compensation can successfully deal with the error between nominal model and blimp real situation. It improves the performance of blimp altitude controller.

A video of experimental result can be found here: https://drive.google.com/ drive/folders/1YmksewRW0odrUsALI--CyPM4qWGIUWv6?usp=sharing.

Conclusion and Future Work

In this paper, the study of indoor small blimp robot's altitude control is presented. The work started from the modelling of indoor blimp robot, presenting an efficient way to identify the model's parameters. The model is identified as a switched system with a constant time-delay complemented with uncertain bounded disturbances. Next, in order to achieve full state estimation, HOMD, HOSM, High-Gain and ALIEN differentiators are discussed and compared, and HOMD differentiator is finally used to evaluate the blimp's vertical velocity. Then, a predictor-based controller is designed for altitude stabilising task. In order to compensate the disturbance in the model, a method to estimate and predict the disturbance is proposed with the help of HOMD differentiator again. When it comes to realisation on real blimp, the high-precision motion capture system is combined with the blimp system to improve measurement accuracy. Finally, we got a satisfying result in real tests, and demonstrated the performance of disturbance compensation of our controller in blimp altitude stabilising task.

The altitude control of indoor small blimp robot is just the first step of our final objective. In the future, we will continue the study on blimp robot, develop useful applications like long-term monitoring, or unknown environment exploring. To achieve that, we have to make the blimp system more autonomous, realise accurate position and pose estimation with information only coming from inside the system, and make the blimp more robust to disturbances.

Figure 1 .

 1 Figure 1. Coordinate and symbols of blimp The motion of blimp is referenced to a body-fixed orthogonal frame R b (O, X b , Y b , Z b ); blimp linear and angular velocities are given by ξ =

Table 1 .

 1 Parameter identification result Case ż ≥ 0 ż < 0 u ≥ 0 a = -0.035 b = 0.0628 a = -0.0366 b = 0.0628 u < 0 a = -0.035 b = 0.0424 a = -0.0366 b = 0.0424

Figure 2 .

 2 Figure 2. Altitude estimation comparison.

Figure 3 .

 3 Figure 3. Velocity estimation comparison.

  and x2 ≥ 0 2, u ≥ 0 and x2 < 0 3, u < 0 and x2 ≥ 0 4, u < 0 and x2 < 0 (29) 4.2. Predictor-based Controller Design Considering the system is time-delayed, a predictor-based controller is designed. It has two parts: 1) Predict state at time t + τ with Smith (1959) predictor: X(t + τ nom ) = e Aστnom X(t) + 0 -τnom e -Aσs B σu(t + s)ds + 0 -τnom e -Aσs B σ d(t + τ nom + s)ds (30)

Figure 4 .

 4 Figure 4. Scheme of Optitrack-enhanced blimp control system

Figure 5 .Figure 6 .

 56 Figure 5. Blimp altitude controller performance comparison: (a) without disturbance compensation; (b) with disturbance compensation.

Acknowledgements

The PhD student is sponsored by China Scholarship Council (CSC). Thanks to our team's engineer Mr. Xin Jin for his work on the development of blimp's first prototype. Thanks to Paul Lesur for his work on the communication interface between Simulink and OptiTrack and his help during tests.

Disturbance estimation and prediction

The disturbance term in system description (6) represents the error between nominal model and blimp real situation.

In order to estimate the disturbance d(t) in real time, a filter is designed:

where L = l 1 l 2 T is the gain of filter. It is obvious that the filter has a similar form as a Luenberger observer for nominal model, i.e. ( 6) without disturbance term. Let e(t) = X(t) -X fil (t) be the error between state vector of ( 6) and that of filter (32). Taking the time derivative of e(t), we get

where δ(t) = (A σ -A σ)X (t). After simplification and assumption that σ(t) = σ(t), the expression of disturbance estimation is obtained:

, so e 1 is the difference between altitude measurement and filter output, and it is available for measurements. In order to assure the stability, the filter matrix A σ -LC needs to be Hurwitz, and the gain L can be chosen to make the filter converges five to six times faster than (6). The calculation of ė1 (t) and ë1 (t) is also realised by HOMD differentiator (28).

As it has been observed in experiments, the estimated disturbance signal is rather noisy; in order to decrease the chattering, we choose to use a time polynomial to fit d(t) in a sliding window, then the polynomial is used to predict d(t + τ nom ).

Determination of controller gain

As system (6) is time-delayed with an uncertain bounded disturbance, a predictorbased controller (31) with disturbance compensation is designed. The problem remains to determine a gain of controller K σ which can make the closed-loop system Ẋ(t) = (A σ -B σ K σ )X(t) stable.

Assume the gains of controller of switched system are chosen to be the same for all σ, i.e. K σ = K, to simplify calculation.

According to [START_REF] Liberzon | Basic problems in stability and design of switched systems[END_REF], if there exists a matrix P and gain K, with P = P T , such that P 0 (A σ -B σ K) T P + P (A σ -B σ K) ≺ 0, ∀σ ∈ P (35) is satisfied, then the closed-loop switched system is stable. Transform (35) to