Hana M'hemdi
email: hana.mhemdi@femto-st.fr

Jacques Julliand
email: jacques.julliand@femto-st.fr

Pierre-Alain Masson
email: pierre-alain.masson@femto-st.fr

Riadh Robbana

Test Generation from Timed Pushdown Automata with Inputs and Outputs

Keywords: Timed Pushdown Automata, Reachability Timed Automata, Clock Constraints Backward Closure, Test Generation from Automata, Conformance Relation for TPAIO. Transitions Paths (l 0 , , g 0 , ∅, l 3

We consider in this paper the model of Timed Pushdown Automata with Inputs and Outputs (TPAIO), for which state reachability can only be solved in exponential time. We compute by means of a polynomial algorithm a reachability timed automaton (RTA), thus partial, of a TPAIO. When the algorithm is applied to untimed pushdown automata, the reachability is equivalent in both automata. But with the addition of clock constraints, reachability in the RTA is only a sufficient condition. To decide if a succession of timed transitions can be executed, we compute the backward closures of the clock constraints, and evaluate them by means of satisfiability decision procedures. Additionally, we compute a path table that relates a feasible transition of the RTA to the corresponding path of the TPAIO. We accept the incompleteness of our method as a price to pay for efficiency. It can be used in test generation since testing is incomplete by nature. Test generation relies on unfolding the transitions of the reachability timed automaton thanks to the path table.

I. INTRODUCTION

Systems are commonly modelled by various types of transition systems including finite automata, pushdown automata (PA), timed automata (TA), etc. The verification of these systems, as well test generation from their models, are very active research areas [START_REF] Krichen | Conformance testing for real-time systems[END_REF], [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF], [START_REF] Héam | A random testing approach using pushdown automata[END_REF].

PA [START_REF] Autebert | Context-free languages and pushdown automata[END_REF] are equipped with a stack, and can model recursive systems. The reachability problem is the problem of deciding whether an automaton can reach a particular location from an initial location. This problem is decidable [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF] [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF]. TA were introduced by Alur and Dill [START_REF] Alur | A theory of timed automata[END_REF], and have become a standard modelling formalism for real-time systems. They are equipped with a finite set of real-valued clocks, in which constraints on the clocks are used to restrict the behaviours of the automata. One of the most basic problems in TA is the location reachability problem. Reachability in TA is a decidable problem [START_REF] Alur | Model-checking in dense real-time[END_REF].

In this paper we consider TPA, i.e. TA equipped with a stack. with inputs and outputs to model for example recursive procedure calls in real time systems. Theoretically, the reachability problem is solved [START_REF] Bouajjani | On the automatic verification of systems with continuous variables and unbounded discrete data structures[END_REF], [START_REF] Abdulla | Dense-timed pushdown automata[END_REF]. Although reachability in PA can be verified in polynomial time, adding clocks provokes an exponential blow up in complexity (see for example [START_REF] Chadha | Complexity bounds for the verification of real-time software[END_REF]), so that reachability in TPA can only be verified in exponential time. Besides, the usual approach to deal with TA, that are space infinite due to the infinite domains of the clocks, is to perform a region graph partitioning. This provides a finite representation of the TA, but the number of regions grows exponentially with the number of clocks. The use of -transitions and backward closures of clock constraints, as in [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF], allows to express the successive constraints as a SAT problem over the clock constraints.

In this paper, we propose an approach for computing tests from the TPAIO model. Following [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF], we propose a set of rules to build a reachability timed automaton (RTA) from a TPA. The RA is computed in [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF] from a PA in polynomial time, and location reachability is equivalent in both models. In our case, we have adapted the rules to take clock constraints into account in addition to stack ones. Applying these rules until saturation would theoretically result in computing an RTA where location reachability is equivalent to that of the TPA. But not only the computation time becomes exponential, it may also not terminate. Hence our proposition is an incomplete method. We propose an algorithm that applies the rules with a termination criterion based on transitions coverage. It operates in polynomial time and is guaranteed to terminate. Reachability in the RTA becomes only a sufficient condition to reachability in the TPA. While in verification completeness is usually a must, test generation can deal with some incompleteness, as software testing is an incomplete activity by nature. By applying to a TPA a polynomial transformation into a RTA, and with the use of SMT solvers to solve the backward closures of clock constraints, our method can efficiently generate a set of tests from a TPAIO. To summarize, our contributions are to: (i) define tpioco: a conformance relation for the TPAIO model; (ii) adapt the reachability computation of [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF] to the case of TPAIO in the goal to generate tests; (iii) define a method that is incomplete but polynomial to compute a partial RTA of a TPA; (iv) generate test cases by covering the reachable locations and transitions of the TPAIO. To our knowledge, these problems solved for the TA and the PA had not been handled for the TPA yet.

The paper is organized as follows. Section II presents the TA, the conformance relation tioco and the backward closure in TA. Section III presents our TPAIO model, a conformance relation for TPAIO and an illustrative example of a TPAIO. Section IV applies transition merging to TPA and gives rules to define a complete RTA of a TPA. It also presents the polynomial algorithm to compute a partial RTA and a path table from a TPA. Our method for generating tests from a TPAIO and a conformance relation is presented in Section V. In Section VI, we illustrate the soundness, incompleteness and test coverage of our method. We conclude and indicate future work in Section VII.

II. BACKGROUND

This section defines TA, the timed input-output conformance relation and the backward closure in TA.

A. Timed Automata

Let Grd(X) be the language of clock guards defined by the following grammar g ::

= x ∼ n | g ∧g | g ∨g | true | false where ∼ ∈ {<, ≤, >, ≥, =}, X is a set of clocks, x is a clock in X taking its values in R + and n is a constant in N.
Definition 1 (Timed Automaton): A TA is a tuple T = L, l 0 , Σ, X, ∆, F where L is a finite set of locations, l 0 is an initial location, Σ is a finite set of labels, X is a finite set of clocks, F ⊆ L is a set of accepting locations and

∆ ⊆ L × Σ × Grd(X) × 2 X × L is a finite set of transitions.
A transition is a tuple (l, a, g, X , l ) denoted by l a,g,X ----→ l where l, l ∈ L are respectively the source and target locations, a (∈ Σ) is an action symbol, X (⊆ X) is a set of resetting clocks and g is a guard. The operational semantics of a TA T is an infinite transition system S T , s T 0 , ∆ T whose states in S T are pairs (l, v) ∈ L × (X → R + ) where l is a location and v is a clock valuation. s T 0 is the initial state and ∆ T is the set of transitions. There are two kinds of transitions in ∆ T : timed and discrete. Timed transitions are in the shape of (l, v) → δ (l, v + δ) where δ ∈ R + is a delay, so that v + δ is the valuation v where each clock is augmented by the delay δ. Discrete transitions are in the shape of (l, v) → a (l , v ) where a ∈ Σ and (l, a, g, X , l ) ∈ ∆, and such that v satisfies g and v = v[X := 0] is obtained by resetting to zero all the clocks in X and leaving the others unchanged. A path π of a TA is a finite sequence of its transitions:

l 0 a0,g0,X0 -----→ l 1 a1,g1,X1 -----→ l 2 • • • l n-1 an-1,gn-1,Xn-1 -----------→ l n . A run of a TA is a path of its semantics.σ = (l 0 , v 0 ) → δ0 (l 0 , v 0 + δ 0 ) → a0 (l 1 , v 1 ) → δ1 (l 1 , v 1 + δ 1 ) → a1 (l 2 , v 2 ) → δ2 ... → an-1 (l n , v n ) where δ i ∈ R + and a i ∈ Σ for each 0 i n -1 is a run of π if v i |= g i for 0 i < n.
A run alternates timed and discrete transitions. Its trace is ρ = δ 0 a 0 δ 1 a 1 ...δ n a n , a finite sequence of (Σ ∪ R + ) * . We denote RT (Σ) the set of finite traces (Σ ∪ R) * on Σ. P Σ1 (ρ) is a trace that is the projection of a trace ρ on Σ 1 with preserved delays and where Σ 1 ⊆ Σ. For example, if ρ = 5a4b2, then, P {a} (ρ) = 5a42 = 5a6. T ime(ρ) is the sum of all the delays in ρ. For example, T ime(5a42) = 11. s T 0 → ρ s means that the state s is reachable from the initial state s T 0 if there exists a run σ from s T 0 to s such that ρ is its trace. s T 0 → ρ means that there exists s such that s T 0 → ρ s .

Timed Automata with Inputs and Outputs (TAIO) extend the TA model by distinguishing between input and output actions. A TAIO is a tuple L, l 0 , Σ in ∪ Σ out ∪ {τ }, X, ∆, F where Σ in is a set of input actions, Σ out is a set of output actions and τ is an internal and unobservable action. This distinction is widely used in the domain of test. It models the controllable (∈ Σ in ) and observable (∈ Σ out ) interactions between the environment and the system. The environment, thus the tester, sends the commands of Σ in and observes the output of Σ out . The implementation under test (IU T ), sends the observable actions of Σ out and accepts the commands of Σ in .

Let Σ = Σ in ∪ Σ out and Σ τ = Σ ∪ {τ }. A TAIO is deterministic if for all location l in L, for all action a in Σ τ and for all couple of distinct transitions t 1 = (l, a, g 1 , X 1 , l 1 ) and t 2 = (l, a, g 2 , X 2 , l 2 ) in ∆ then g 1 ∧ g 2 is not satisfiable. It is observable if no transition is labelled by τ . The set of reachable states of a TAIO T , denoted Reach(T ), is the set:

{s T ∈ S T | ∃ρ.(ρ ∈ RT (Σ) ∧ s T 0 → ρ s T }. A TAIO T is non blocking if ∀(s, δ).(s ∈ Reach(T ) ∧ δ ∈ R + ⇒ ∃ρ.(ρ ∈ RT (Σ out ∪ {τ }) ∧ T ime(ρ) = δ ∧ s → ρ )).
A TAIO is called input-complete if it accepts any input at any state.

B. Timed Input-Output Conformance Relation tioco

We first present the conformance theory for timed automata based on the conformance relation tioco [START_REF] Krichen | Conformance testing for real-time systems[END_REF]. tioco is an extension of the ioco relation of Tretmans [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF]. The main difference between tioco and ioco is that ioco uses the notion of quiescence. In [START_REF] Krichen | Conformance testing for real-time systems[END_REF], the tioco relation doesn't use quiescence because the timeouts are explicitly specified. The assumptions are that the specification of the system to be tested is a nonblocking TAIO, and that its implementation is a non-blocking and input-complete TAIO. This last requirement ensures that the execution of a test case on the IU T does not block the verdicts to be emitted. To present the conformance relation for a TAIO T = L, l 0 , Σ in ∪ Σ out ∪ {τ }, X, ∆, F , we need to define the following notations in which ρ ∈ RT (Σ):

• T after ρ = {s ∈ S T | ∃ρ .(ρ ∈ RT (Σ τ )∧s T 0 → ρ s∧ P Σ (ρ ) = ρ)} is the
set of all states of T reachable by a trace ρ whose projectionP Σ (ρ ) on the controllable and observable actions is ρ.

• ObsTTraces(T ) = {P Σ (ρ) | ρ ∈ RT (Σ τ ) ∧ s T 0 → ρ } is the set of observable timed traces of a TAIO T . • elapse(s) = {δ | δ > 0 ∧ ∃ρ.(ρ ∈ RT ({τ }) ∧ T ime(ρ) = δ ∧ s → ρ )}
is the set of all delays which can elapse from the state s with no observable action. • out(s) = {a ∈ Σ out | s → a } ∪ elapse(s) is the set of outputs and delays that can be observed from the state s. Definition 2 (tioco: Timed Input-Output Conformance Relation ): Let T = (L, l 0 , Σ τ , X, ∆, F ) be a specification and I = (L I , l I 0 , Σ I τ , X I , ∆ I , F I ) be an implementation of T . Formally, I conforms to T , denoted I tioco T iff ∀ρ.(ρ ∈ ObsT T races(T ) =⇒ out(I af ter ρ)

⊆ out(T af ter ρ)). It means that the implementation I conforms to the specification T if and only if after any timed trace enabled in T , each output or delay of I is specified in T .

C. Backward Closure in Timed Automata

As in [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF], our method for computing location reachability introduces -transitions. An -transition in a PA goes from a location to another without modifying the stack content. It is used to represent by means of a single transition a succession of push and pop ones that leave the stack unchanged at the end. Our intention is to merge a sequence of consecutivetransitions in the TPA case. The successive clock constraints have to be accumulated and their verification shifted backward to the beginning of the sequence. We use for this the backward closure of constraints as in [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF].

Definition 3 (Backward closure of a constraint): Let g be a clock constraint and X be a set of clocks. The backward closure of g on X, denoted by ←g X , is a formula that is satisfied by a clock valuation v if g will be satisfiable after the clocks of X have been reset, and a delay δ has passed:

v ← -g X if ∃δ • (δ ≥ 0 ∧ v[X := 0] + δ g).

III. TPAIO AND CONFORMANCE RELATION

In this section, we first define the TPAIO model, then a conformance relation for a TPAIO. We also present an example of a TPAIO that models a recursive program.

A. Timed Pushdown Automata with Inputs and Outputs

A TPA T = L, l 0 , Σ, Γ, X, ∆, F is a TA equipped with a stack. Its operational semantics is a transition system < S T , s T 0 , ∆ T > where the locations called states are configurations made of three components (l, v, p) where l is a location of the TPA, v is a clock valuation in X → R + and p is a stack content in Γ * . In this paper, we consider TPA with Inputs and Outputs (TPAIO).

Definition 4 (TPAIO): A TPAIO is a tuple L, l 0 , Σ, Γ, X, ∆, F where L is a finite set of locations, l 0 is an initial location, Σ = Σ in ∪ Σ out where Σ in is a finite set of input actions, Σ out is a finite set of output actions, Γ is a stack alphabet

(Σ out ∩Σ in = ∅, Σ in ∩Γ = ∅ and Σ out ∩Γ = ∅), X is a finite set of clocks, F ⊆ L is a set of accepting locations, ∆ ⊆ L × (Σ in ∪ Σ out ∪ Γ +-) × Grd(X) × 2 X × L is a finite set of transitions where Γ +-= {a + | a ∈ Γ} ∪ {a -| a ∈ Γ}.
The symbols of Γ +-represent either a push operation (of the symbol a) denoted a + , or a pop operation denoted a -.

A transition is a tuple (l, a, g, X , l ) denoted by l a,g,X ----→ l where l, l ∈ L are respectively the source and target locations, a ∈ Σ ∪ Γ +-is either a label or a stack action, X (⊆ X) is a set of resetting clocks and g is a guard. There are two kinds of transitions in the semantics: timed and discrete. Timed transitions are in the shape of (l, v, p) → δ (l, v + δ, p). For a transition (l, act, g, X , l ), there are three types of discrete transitions when v satisfies g: (1) push when

act = a + : (l, v, p) → a + (l , v[X := 0], p.a) where a ∈ Γ, (2) pop when act = a -: (l, v, p.a) → a -(l , v[X := 0], p) where a ∈ Γ, (3) output or input when act = A ∈ Σ: (l, v, p) → A (l , v[X := 0], p).
A TPAIO is normalized if it executes separately push and pop operations. All TPAIO can be normalized since all PA can be normalized [START_REF] Sénizergues | L(a) = l (b) ? decidability results from complete formal systems[END_REF]. In the remainder of the paper, we consider that TPAIO are always normalized deterministic TPAIO and we denote a the actions of Γ, and A the actions of Σ.

We define our conformance relation denoted tpioco for the TPAIO as an extension of the conformance relation tioco [START_REF] Krichen | Conformance testing for real-time systems[END_REF]. It is the same relation as tioco for TAIO considering that the whole alphabet is Σ ∪ Γ +-instead of Σ ∪ {τ } (there is no observable action τ ), the output alphabet is Σ out ∪Γ +-instead of Σ out and the input alphabet remains Σ in .

B. Modelling of Recursive Programs

Figure 1 shows a TPAIO that is an abstraction of a function called pow that computes x n . The location labels correspond to control point in the body of the function between each atomic instruction. pow + is a recursive call (push). pow -is a return (pop) of a recursive call. Thus, Γ = {pow}. The atomic instructions and conditions are abstracted by the letters A to H so:

A def = int res, B def = n = 0, C def = n = 0, D def = return 1, E def = n mod 2 = 0, F def = return res * res, G def = n mod 2 = 0 and H def = return res * res * x.
All executions of atomic instructions are in Σ in . All executions of conditions are in Σ out . Thus, Σ in = {A, D, F, H} and Σ out = {B, C, E, G}. We use the notation !act to denote act as an output action of Σ out and ?act to denote act as an input action of Σ in .

IV. RTA DEFINITION AND COMPUTATION From a TPA, we define a Reachability Timed Automaton (RTA) that is a TA whose the set of transitions can be infinite and each of them is labelled by . We extend for that a set of rules for PA issued from [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF] to the TPA case, by taking the clock constraints into consideration. The sequences made of successive push and pop transitions are merged intotransitions. Then, according to Def. 5, the successive resulting -transitions are merged, etc. The clock constraints are accumulated during this process by computing their backward closure. This preserves reachability as proved by Lemma 1. Let GrdB(X) the language of clock guards with backward closures defined by the following grammar gb ::

= g | g ∧ b where g ∈ Grd(X), b ::= ← -g X | ← - gb X and X is a subset of clocks of X.

Definition 5 (Merging of two successive merged transitions):

The successive transitions:

t 1k = l1 ,g 1 ∧ ← -------------- g 2 ∧ ... ...∧ ← --- g k-1 X k-2 X 1 ,X k-1 ---------------------→ l k and t kn = l k ,g k ∧ ← ---------------- g k+1 ∧ ... ...∧ ← --- g n-1 X n-2 X k ,X n-1 -----------------------→ ln are merged into the -transition t1n = l1 ,g 1 ∧ ← ------------------------------------------------ g 2 ∧ ... ...∧ ← -------------------------------- g k-1 ∧ ← ---------------------- g k ∧ ← ---------------- g k+1 ∧ ... ...∧ ← --- g n-1 X n-2 X k X k-1 X k-2 ,X n-1 X 1 --------------------------------------------→
ln where k 2 and n k + 1.

For example, the case where k = 2 and n = 3 merges the two -transitions l 1

,g1,X1 -----→ l 2 ,g2,X2 -----→ l 3 into the -transition l 1 ,g1∧ ← - g2 X 1 ,X2 ---------→ l 3 .
Lemma 1: Let t 1k , t kn and t 1n be the transitions as defined in Def. 5. The location l n is reachable from l 1 by applying successively the transition t 1k and the transition t kn iff l n is reachable from l 1 by applying the transition t 1n .

Proof: We first prove the left to right implication. We assume that the location l n is reachable from the location l 1 by applying successively t 1k and t kn . This means that there exists a valuation v 1 and a succession of delays δ 1 , δ 2 , ..., δ k-1 , ..., δ n-1 such that there exists the following two runs:

σ 1k = (l 1 , v 1 ) → δ1 (l 1 , v 1 + δ 1 ) → (l 2 , v 2 ) → δ2 (l 2 , v 2 + δ 2 ) → (l 3 , v 3 ) → • • • → δ k-1 (l k-1 , v k-1 + δ k-1 ) → (l k , v k ) and σ kn = (l k , v k ) → δ k (l k , v k + δ k ) → (l k+1 , v k+1 ) . . . → δn-1 (l n-1 , v n-1 + δ n-1 ) → (l n , v n ) where v i = (v i-1 + δ i-1 )[X i-1 := 0] for 0 < i ≤ n.
Under this assumption, the transition t 1n is fireable as the values v 1 , δ 1 , δ 2 , ..., δ n-1 make its guard satisfiable. Thus l n is reachable by the run that is the concatenation of σ 1k and σ kn . Proof of the right to left implication is similar. ----→ l is a transition that reaches the location l from the location l without modifying the stack content. The reachable locations of the RTA are those that are reachable from its initial location by an -transition whose guard is satisfiable. We propose in Def. 6 the rules RA 1 to RA 4 that, applied repeatedly, define a RTA.

l0 l1 l2 l4 l3 l5 l6 l7 l8 l9 ?A, x 2 !B, x 1, {x} !C, x 1, {x} ?D, x 2 !E, x 1, {x} ?F, x 3 !G, x 1, {x} ?H, x 3 pow + , x 3, {x} pow -, x 2, {x} pow -, x 2, {x} pow -, x 2, {x}
Definition 6 (RTA of a TPA):

The RTA of a TPA L, l 0 , Σ, Γ, X, ∆, F is the TA L, l 0 , { }, X, ∆ R , F where ∆ R ⊆ L × { } × GrdB(X) × 2 X ×
L is the relation that satisfies the rules given in Table I.

Lemma 2: The transitions of the RTA that result from the rules RA 1 to RA 4 are fireable iff the TPA transitions that they merge are fireable.

Proof: The proof is by induction and by cases on each rule. The induction assumption is that the RTA transitions are sound before they are merged into new transitions. We prove this assumption to be true by proving that the rules RA 1 and RA 2 , that create RTA transitions only from TPA ones, are sound. Then we prove that the rules RA 3 and RA 4 preserve that soundness.

• RA 1 case: l 1 A,g1,X1 -----→ l 2 ∈ ∆ is fireable if there exists a clocks valuation v 1 such that v 1 |= g 1 . Thus the transition l 1 ,g1,X1 -----→ l 2 ∈ ∆ R is also fireable from v 1
. This is obviously true in the opposite direction.

• RA 2 case: first, regarding the stack constraints, the transitions are successively fireable because it is always possible to pop a after the label a has been pushed. As for the clock constraints, l 1

a + ,g1,X1 ------→ l 2 ∈ ∆ and l 2 a -,g2,X2
------→ l 3 ∈ ∆ are fireable if there exists a clocks valuation v 1 and a delay δ 2 such that v 1 |= g 1 and v 1 [X 1 := 0] + δ 2 |= g 2 . These are exactly the conditions for which the transition

l 1 ,g1∧ ← - g2 X 1 ,X2 ---------→ l 3 ∈ ∆ R is fireable, i.e. v 1 |= g 1 ∧ ← - g 2 X1 . This condition is equivalent to v 1 |= g 1 and v 1 |= ← - g 2 X1 . From Def. 3, v 1 |= ← - g 2 X1 is satisfied if ∃δ 2 .(δ 2 0 ∧ v 1 [X 1 := 0] + δ 2 |= g 2 ) is satisfied.
• RA 3 case: the stack constraints are satisfied for the same reasons as in the previous case, because antransition leaves the stack content unchanged. The clock constraints are also satisfied for the following reasons: the sequence of three transitions l1 -------------------------- ---------------------

a + ,g 1 ,X 1 ------→ l2 ∈ ∆ , l2 ,g 2 ∧ ← -------------- g 3 ∧ ... ...∧ ← --- g k-1 X k-2 X 2 ,X k-1 ---------------------→ l k ∈ ∆ R and l k a -,g k ,X k ------→ l k+1 ∈ ∆ are fireable if there exists v 1 , δ 2 , ..., δ k such that v 1 |= g 1 and v 2 = v 1 [X 1 := 0], v 2 + δ 2 |= g 2 and v 3 = (v 2 + δ 2 )[X 2 := 0], v k + δ k |= g k . For such values the transition l1 ,g 1 ∧ ← -
g 2 ∧ ← -
g 3 ∧ ... ...∧ ← ----------- g k-1 ∧ ← - g k X k-1 X k-2 X 2 X 1 ,X k ------------------------------→ l k+1 ∈ ∆ R
is fireable because its guard defined by Def. 3 is satisfied. From Def. 3 this condition is the following

v 1 |= g 1 ∧ ← ------ g 2 ∧ ← - g 3 X2 X1 ≡ v 1 |= g 1 ∧ ∃δ 2 .(δ 2 0 ∧ v 1 [X 1 := 0] + δ 2 |= g 2 ∧ ← - g 3 X2 ≡ v 1 |= g 1 ∧ ∃δ 2 .(δ 2 0 ∧ v 1 [X 1 := 0] + δ 2 |= g 2 ∧ ∃δ 3 .(δ 3 0 ∧ (v 1 [X 1 := 0] + δ 2 )[X 2 := 0] + δ 3 |= g 3 )).
Our assumption is exactly this condition: there exists v 1 , δ 2 , δ 3 such that v 1 |= g 1 and v 2 = v 1 [X 1 := 0] and v 2 + δ 2 |= g 2 and v 3 = (v 2 + δ 2 )[X 2 := 0] and v 3 + δ 3 |= g 3 .

• RA 4 case: it is a direct consequence of Lemma 1 as the rule RA 4 is the rule of Def. 5.

Remark 1:

The rule RA 4 is the merging rule of Def. 5. Due to the rules RA 3 and RA 4 , the repeated application of these rules may not converge in the case where a cycle oftransition is created on a location l. Merging this cycle with another -transition that enters (or leaves) l from (or towards) a location l creates a new -transition between these two locations, that still can be merged again with the cycle, and so on. . . Such a cycle is satisfiable or not in terms of clock constraints. This satisfiability does not depend on the number of times the cycle is taken. Thus, to ensure its termination, an algorithm applying these rules repeatedly should take care of not taking a cycle of -transition more than once. Our algorithm of Fig. 3 in the next section takes this care.

B. Algorithm to Compute a Finite Partial RTA

We present an algorithm that applies finitely the rules RA 1 to RA 4 for building a finite partial RTA from a TPA. It is an adaptation of the algorithm [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF], which originally computes a reachability automaton from a PA. The principle is to first gather into single -transitions the successive push and pop transitions, and then to incrementally explore how thesetransitions can be combined to each other and to the remaining transitions. We extend this algorithm to the TPA case. Thetransitions are merged the same way w.r.t. the stack constraints,

RA1 l1 ,g 1 ,X 1 -----→ l2 ∈ ∆ R if l1 A,g 1 ,X 1 -----→ l2 ∈ ∆ RA2 l1 ,g 1 ∧ ← - g 2 X 1 ,X 2 ---------→ l3 ∈ ∆ R if l1 a + ,g 1 ,X 1 ------→ l2 ∈ ∆ and l2 a -,g 2 ,X 2 ------→ l3 ∈ ∆ RA3 l1 ,g 1 ∧ ← --------------------------- g 2 ∧ ← ---------------------- g 3 ∧ ... ...∧ ← ----------- g k-1 ∧ ← - g k X k-1 X k-2 X 2 X 1 ,X k ------------------------------→ l k+1 ∈ ∆ R if l1 a + ,g 1 ,X 1 ------→ l2 ∈ ∆, l2 ,g 2 ∧ ← -------------- g 3 ∧ ... ...∧ ← --- g k-1 X k-2 X 2 ,X k-1 ---------------------→ l k ∈ ∆ R and l k a -,g k ,X k ------→ l k+1 ∈ ∆ RA4 l1 ,g 1 ∧ ← ------------------------------------------- g 2 ∧ ... ...∧ ← -------------------------------- g k-1 ∧ ← ---------------------- g k ∧ ← ---------------- g k+1 ∧ ... ...∧ ← --- g n-1 X n-2 X k X k-1 X k-2 X 1 ,X n-1 --------------------------------------------→ ln ∈ ∆ R if l1 ,g 1 ∧ ← -------------- g 2 ∧ ... ...∧ ← --- g k-1 X k-2 X 1 ,X k-1 ---------------------→ l k ∈ ∆ R and l k ,g k ∧ ← ---------------- g k+1 ∧ ... ...∧ ← --- g n-1 X n-2 X k ,X n-1 -----------------------→ ln ∈ ∆ R TABLE I. RTA Building Rules
but we have additional rules for computing their time constraint backward closure at merging time. The resulting -transitions carry a guard w.r.t. the clocks. The satisfiability evaluation of these guards is postponed to a second phase, when all the merging have been performed. Additionally, our algorithm computes a path table, which associates each transition of the RTA with one or many paths of the TPA. Our modifications of the algorithm of [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF] are summarized as follows.

1) We compute not only the -transitions in the RTA but also their paths. Any -transition in the RTA corresponds to one or many paths in the TPA. 2) Because the problem addressed in [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF] is to check the locations reachability, the redundant -transition between two locations l and l are not recorded in the result, although they have been computed. We record them as alternative possibilities for the clock constraints to be satisfiable. 3) We add the rule RA 1 because these transitions may carry some clock constraints that we cannot ignore, contrarily to the context of PA without clock constraint considered by Finkel et al. 4) The reflexive -transitions are not used in [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF] to extend (on their right or on their left) the existing -transitions, because they do not change anything regarding accessibility. There again, we cannot ignore them due to their clock constraints.

To ensure the termination of our algorithm (see Remark 1), a new transition (l, , g, X, l ) is added only if its path covers a new transition of the TPA between the locations l and l . The algorithm is given in Fig. 3. It computes the transitions of ∆ R in the table paths. Its input is a TPA. It returns a path table which associates each transition of the RTA with a set of paths of the TPA. To present this algorithm, we define the type PATHS = Seq(∆) that is a sequence of transitions of the TPA, and the type PATH TABLES =∆ R set of P AT HS that is a surjective function that maps a set of paths to each transition of the RTA. This algorithm computes the transitive closure of -transitions only once by storing information in the data structures C Direct and C T rans on how the -transitions can be obtained. The algorithm enumerates all the possible pairs of locations, and searches for each of them if it can be exploited to form an -transition of the RTA.

The algorithm is in two steps: an initialization step from lines 1 to 16, and a processing step from line 17 to line

(a) l l l 2 , g 1 , X 1 , g , X , g n , X n . . . (b) l 1 l l , g 1 , X 1
, gn, Xn , g, X . . . For each pair of locations (l, l ), the set C Direct(l, l ) is initialized by a sequence of two transitions: a push transition a + and a pop transition a -(lines 10-12). The C T rans structure associates a set to each possible pair of transitions. It is used to apply the rule RA 4 . Its initialization is performed by lines 13-16. In its second step (lines 17-46), the algorithm processes each transition popped off the stack, and determines its consequences when considering C Direct and C T rans. For an -transition and its path π between the locations l and l , the algorithm examines the two possibilities for computing other -transitions:

• By using C Direct((l, l )) (line 33-35): for every ((l 1 , l 2 ), [(l 1 , a + , g 1 , X 1 , l), (l , a -, g , X , l 2 )]) in C Direct((l, l )), our algorithm adds a newtransition between l 1 and l 2 where its path is [(l 1 , a + , g 1 , X 1 , l)ˆπˆ(l , a -, g , X , l 2 )] where tˆπ denotes the concatenation of the transition t with the path π. • By using C T rans((l, l )) (line 36-44): for every ((l 1 , l 2 ), (l 3 , l 4 )) in C T rans((l, l )): for each path π 1 that forms an -transition between l 1 and l 2 : our algorithm adds an -transition as illustrated in

INPUT: A TPA L, l0, Σ, Γ, X, ∆, F OUTPUT: paths ∈ P AT H T ABLE VARIABLES: stack ∈ L × L ↔ P AT HS; C Direct ∈ L × L set of L × L ↔ P AT HS; C T rans ∈ L × L set of L × L L × L; l, l , l1, l2, l3, l4 ∈ L; π, π1 ∈ P AT HS; tr ∈ ∆ R ; t ∈ ∆ ; coveredT ransitions ∈ L × L set of ∆ BEGIN 1:
for every transition (l, A, g, X, l ) ∈ ∆ where A ∈ Σ do 2:

push ((l, l ), [(l, A, g, X, l )]) on stack /* implements the rule RA1*/ 3: end for 4: for every location l ∈ L do 5:

push ((l, l), ∅) on stack 6: end for 7: for every pair (l, l ) ∈ (L × L) do 8:

C Direct(l, l ) ← ∅; C T rans(l, l ) ← ∅ ; coveredT ransitions(l, l ) ← ∅ 9: end for 10: for every pair (l1

a + ,g 1 ,X 1 -------→ l2,l3 a -,g 3 ,X 3 -------→ l4) ∈ (∆ × ∆)
where a ∈ Γ do

11:

C Direct(l2, l3) ← C Direct(l2, l3) ∪ {((l1, l4), [(l1, a + , g1, X1, l2), (l3, a -, g3, X3, l4)])}

12: end for 13: for every triplet (l, l , l ) ∈ (L × L × L) do 14:

C T rans(l, l ) ← C T rans(l, l ) ∪ {((l , l ), (l, l ))}

15:

C T rans(l, l ) ← C T rans(l, l ) ∪ {((l , l), (l , l ))} 16: end for 17: while stack = emptyStack do 18:

((l, l ), π) ← pop(stack)
19:

tr ← M ergeT ransitions(π)

20:

if isN ewT ransitions(π, coveredT ransitions((l, l ))) then 21:

if π = []

30:

coveredT ransitions((l, l )) ← coveredT ransitions((l, l )) ∪ {t}

31:

end if

32:

end for

33:

for ((l1, l2), [(l1, a + , g1, X1, l), (l , a -, g , X , l2)]) in C Direct((l, l )) do

34:

push ((l1, l2), (l1, a + , g1, X1, l)ˆπˆ(l , a -, g , X , l2) on stack /* where tˆπ denote the concatenation of t and π */

35:

end for

36:

for ((l1, l2), (l3, l4)) in C T rans((l, l )) do

37:

for each π1 in getP aths(l1, l2, paths) do

38:

if l = l1 then 39:

push ((l, l2), πˆπ1) on stack 40: Our algorithm presented in Fig. 3 uses the following functions: (i) M ergeT ransitions(π) that returns antransition and merges all the transitions of its input path π, (ii) isN ewT ransitions(π, ∆) that verifies if the sequence of transitions π contains a transition which is not in the set of transitions ∆ and (iii) getP aths(l, l , paths) that returns the subset of paths in paths that lead from l to l .

To ensure the termination of our algorithm, the adding of a new transition (l, , g, X, l ) is performed only if its path covers a new transition. Our algorithm uses the data structure coveredT ransitions that associates a set of transitions to a pair of locations. For every new transition between two locations l and l , coveredT ransitions stores the new covered transitions between l and l (lines 29-32).

The algorithm of [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF] operates in O(n 3 ) where n is the number of locations of the PA. As a TPA contains output transitions that our algorithm treats differently than that of [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF], and as the termination of our algorithm depends on the number of transitions between two locations, our algorithm is still polynomial.

Example 1: Table II shows some transitions and their paths from the initial location l 0 to a final one l 3 , l 7 or l 9 of the RTA of the TPA of Fig. 1. The bold part of paths are the difference w.r.t the previous one. The guards g 0 , g 1 and g 2 are as follows:

g 0 def = x 2 ∧ ← ---------- x 1 ∧ ← --- x 2 x ∅ , g 1 def = x 2 ∧ ← ---------- x 1 ∧ ← --- x 3 x x , g 1 def = x 2 ∧ ← ------------------------------------- x 1 ∧ ← ------------------------------ x 3 ∧ ← ----------------------- x 2 ∧ ← --------------- x 1 ∧ ← -------- x 2 ∧ ← - g 1 ∅ x ∅ x x ∅ , g 2 def = x 2∧ ← ------------------------------------------- x 1 ∧ ← ------------------------------------ x 2 ∧ ← ----------------------------- x 2 ∧ ←--------------------- x 1 ∧ ← -------------- x 3 ∧ ← ------- x 2 ∧ g 1 ∅ x x ∅ x ∅ , and g 2 def = x 2∧ ←------------------------------------- x 1 ∧ ← ------------------------------ x 3 ∧ ← ----------------------- x 2 ∧ ←--------------- x 1 ∧ ← -------- x 3 ∧ ← - g 2 x x ∅ x x ∅ .
V. TEST GENERATION FROM TPAIO We present in this section our method for test generation from a given TPAIO. We first present the test generation process and then the two new steps of our method. The other step is the computation of a RTA that is presented in the previous section.

A. Process

The data flow diagram in Fig. 4 shows the three steps of the test generation process that we propose in this paper: Tester with Inputs and Outputs (TPTIO). The tester obtained is a TPAIO provided with a location f ail. 2) Computation of a partial RTA and its path table from the TPAIO presented in Sec. IV-B: popping actions depend on the content of the stack as it is impossible to pop a symbol if it is not on the top of the stack. This step computes one or many paths between two locations of TPAIO by respecting the stack constraints. The RTA is a finite timed automaton. The path table associates each transition of the RTA with one or many paths of the TPAIO. This step is presented in the previous section. 3) Generation of tree of test cases that are correct behaviours of the TPAIO, computed by using the TPTIO, the RTA and its path table. It is divided into two steps:(a) Generation of a tree of Test Cases (T Cs) that are a tree of paths of -transitions that go from an initial to a final location of RTA. (b) Generation of tree of test cases of the TPTIO. The second step adds the location f ail and the transitions that leads to it.

B. Construction of a TPTIO from a TPAIO Similarly to [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF] and in order to be able to pronounce nonconformances between an IUT and the TPAIO, we compute a tester from a TPAIO. The tester is a TPAIO. Its output actions are the output actions of Σ out , the stack actions of Γ +-and the response delays. The tester is obtained from the TPAIO by enriching it with a special fail location and transitions that lead to it from each location l. Let ∆ l be the set of transitions leaving l in the TPAIO.

Definition 7 (Deterministic Timed Pushdown Tester): The TPTIO T T = (L ∪ {f ail}, l 0 , Σ, Γ, {y}, ∆ ∪ ∆ f ail , F ) of a TPAIO T = L, l 0 , Σ, Γ, X, ∆, F . The transitions of ∆ f ail are computed as follows:

• (i) Let ∆ l be the set of the complement in Γ +-of the stack actions of ∆ l and the complement in Σ out of the output actions of ∆ l . For all a ∈ ∆ l , the transition (l, a, true, ∅, f ail) is in ∆ f ail .

• (ii) Observations, earlier or later than specified, of the stack and output actions of ∆ l : for every transition (l, a, g, X , l ) in ∆ l , the transition (l, a, ¬g, ∅, f ail) is in ∆ f ail .

• (iii) The transition (l, -, g, ∅, f ail) is in ∆ f ail where g is the conjunction of the exceeding of the deadlines of the stack and output actions of ∆ l .

C. Generating Correct Behaviour Test Cases

Definition 8 (Tree of Test Cases): Let T = L, l 0 , Σ, Γ, X, ∆, F be a TPAIO that is a specification. A tree of test cases is a deterministic acyclic TPAIO whose locations are either location of T or pass or f ail.

We define firstly what a tree of test cases is in Def. 8. The usual approach described in [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF] to derive tests from a tester consists of enumerating its executions and emitting the verdict pass when the executions don't end in the fail location. This often can only be done partially in practice due to the very large, if not infinite, number of possible executions. So practically a targeted set of executions are extracted out of the tester. We propose to select the executions that reach a final location with an empty stack, for producing a set of nominal test cases. For this, we select the -transitions going from an initial location to a final one. The guard of an -transition with backward closure is expressed as a system of linear inequalities over real numbers. For example, in Table II, the guard of the transition l 0 ,g0 --→ l 3 is expressed by the formula

∃(δ 1 , δ 2 , δ 3 ) ∈ R 3 . δ 1 2 ∧ δ 1 + δ 2 1 ∧ δ 3 2.
The satisfiability of a guard can be efficiently evaluated by means of SMT solvers integrating simplex based methods (see [START_REF] Dutertre | A fast linear-arithmetic solver for DPLL(T)[END_REF] for example), such as Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF]. The result is a tree of test cases, in which the actions are either observable (the stack actions of Γ +-and the output actions of Σ out ) or controllable (the input action of Σ in ). The leaves of the tree other than fail are replaced by the verdict pass. Figure 5.(b) shows a tree of test cases that present seven paths

--------→ l 2 D,x 2 -----→ l 3 pow -,x 2,{x} -----------→ l 5 E,x 1,{x} --------→l 6 F,x 3,{x} --------→l 7 pow -,x 2,{x} -----------→ l 5 G,x 1,{x} --------→ l 8 H,x 3 -----→ l 9 TABLE II.
Example of transitions of the RTA of the TPA of Fig. 1, with their paths corresponding to the following -transitions: (l 0 , g 0 , ∅, l 3 ), (l 0 , g 1 , ∅, l 7 ), (l 0 , g 1 , ∅, l 9 ), (l 0 , g 2 , ∅, l 7 ) and (l 0 , g 2 , ∅, l 9 ) whose the paths can be seen in the Table II.

VI. SOUNDNESS, INCOMPLETENESS AND COVERAGE OF

METHOD This section discusses the soundness, incompleteness and coverage of our method for test generation from a TPAIO.

A. Soundness

Definition 9 (reachability in an RTA): A location l i is reachable in an RTA iff there exists a run that leads to it from the initial location l 0 . To prove the reachability of a location l i in an RTA, we compute a sequence of -transitions that lead from l 0 to l i where all the clock constraints are satisfied. When the sequence is a single -transition, it is sufficient to evaluate the satisfiability of its guard. In a longer sequence, the clock constraints are composed by means of backward closures but not verified, whereas the constraints on the stack are already verified by construction with the rules RA 1 to RA 4 . Consequently we can get rid of the stack constraints, and see the corresponding transitions as -ones. By merging all these successive -transitions by the rule RA 4 , we finally get only one -transition that leads from l 0 to l i . Deciding of the reachability of l i thus reduces to evaluate the satisfiability of the guard of this -transition.

Definition 10 (reachability in a TPA): A location l i is reachable in a TPA iff there exists a run that leads to the location l i from the initial location l 0 .

Theorem 1: A location l is reachable in a TPA iff it is reachable in its RTA.

Proof: This is a direct consequence of Lemma 2. ------→ f ail be a path of a tree of test cases of a specification T = L, l 0 , Σ in ∪ Σ out , Γ, X, ∆, F where l i ∈ L, g i ∈ Grd(X) and a

i ∈ Σ in ∪ Σ out ∪ Γ +-∪ {-} for each 0 i n. If a verdict
f ail is observed while executing π on the implementation I, then the implementation I is not conform to the specification T .

Proof:

Let ρ = δ 0 a 0 δ 1 a 1 δ 2 ...δ n-1 a n-1 δ n a n ∈ RT (Σ in ∪ Σ out ∪ Γ +-
) be a trace of a run of the path π. (l n , v n + δ n , p n ) is the current state after the execution of δ 0 a 0 δ 1 a 1 δ 2 ...δ n-1 a n-1 δ n . It exists the three following cases to reach f ail:

• fail is detected after having observed a n in the case of not acceptable stack or output action by the specification according to item (i) in Def. 7 of the tester. If a n is in the complement of the stack actions of ∆ ln w.r.t Γ +-or a n is in the complement of the output actions of ∆ ln w.r.t Σ out , then, this transition (l n , a n , true, ∅, f ail) is a transition of the tester. Therefore, a n / ∈ out(T af ter δ 0 a 0 δ 1 a 1 δ 2 ...δ n-1 a n-1 δ n ) and I does not conform to T .

• fail is detected after having observed a n in the case of the observations of, earlier or later stack action or output actions by the specification according to the item (ii) in Def. 7 of the tester. a n not exist in the complement of the stack actions of ∆ ln w.r.t Γ +-or in the complement of the output actions of ∆ ln w.r.t Σ out . The current clock valuation does not satisfy the guard g n . Thus, a n / ∈ out(T af ter δ 0 a 0 δ 1 a 1 δ 2 ...δ n-1 a n-1 δ n ) and I does not conform to T .

• fail is detected after having observed a delay δ n in the case according to item (iii) in Def. 7 of the tester. g n is the conjunction exceeding of the deadlines of stack and output actions of ∆ ln by the specification. The transition (l n , -, g n , ∅, f ail) is a transition of the tester. If v n + δ n |= g n , then δ n / ∈ out(T af ter δ 0 a 0 δ 1 a 1 δ 2 ...δ n-1 a n-1 ) and I does not conform to T .

For every non-conformance detected by a path of a tree of test cases there is a non conformance between the implemen-

?E, x 1, {x} !F, x 2
?G, x 1, {x} !H, x 3, {x} pow + , x 3, {x} pow -, x 2, {x} pow -, x 2, {x} pow -, x 2, {x} f ail F 1 f ail x > 1 ?B|?C, x > 1 F 2 f ail F 1 f ail x > 2 pow -, x > 2 F 0 f ail F 3 pow + , x > 3 x > 3 f ail F 4 ?E|?G, x > 1 x > 1 f ail F 1 f ail F 0 x > 2 pow -, x > 2 f ail F 1 f ail F 0 x > 2 pow -, x > 2 l0 l1 l2 pass f ail F 1 !A, x 2 f ail F 2 ?B|?C, x > 1 x > 1 ?B, x 1, {x} f ail F 1 !D, x 2 l4 ?C, x 1, {x} f ail F 3 pow + , x > 3 x > 3 l0 pow + , x 3, {x} f ail F 1 l1 !A, x 3
f ail F 2 ?B|?C, x > 1 x > 1 l2 ?B, x 1, {x} l4 ?C, x 1, {x} f ail F 1 l3 f ail F 0 pow -, x > 2 x > 2 !D, x 2
l5 f ail F 4 ?E|?G, x > 1 x > 1 pow -, x 2, {x} l8 f ail F 1 ?G, x 1, {x} pass !H, x 2
l6 f ail F 1 ?E, x 1, {x} pass !F, x 3
l0 pow + , x 3, {x} f ail F 3 pow + , x > 3 x > 3 l1 !A, x 3
f ail ?F 1 l2 ?B, x 1, {x} f ail F 2 ?B|?C, x > 1 x > 1 l3 !D, x 2
f ail F 1 l5 pow -, x 2, {x} f ail F 0 pow -, x > 2 x > 2 l6 l8 ?E, x 1, {x} ?G, x 1, {x} f ail F 4 ?E|?G, x > 1 x > 1 l7 !F, x 3 l5 pow -, x 2, {x} f ail F 1 f ail F 0 pow -, x > 2 x > 2 f ail F 4 ?E|?G, x > 1 x > 1 l6 l8 ?E, x 1, {x} ?G, x 1, {x} f ail F 1 f ail F 1 pass !F, x 3 pass !H, x 3 l9 !H, x 3 l5 pow -, x 2, {x} f ail F 1 f ail F 0 pow -, x > 2 x > 2 f ail F 4 ?E|?G, x > 1 x > 1 l6 l8 ?E, x 1, {x} ?G, x 1, {x} F 1 f ail F 1 pass !F, x 2

B. Incompleteness

The polynomial complexity of the algorithm of Fig. 3 is possible thanks to the incompleteness. In the case of a PA, there is an -transition in the RTA between two locations l and l if and only if l is reachable from l in the PA [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF]. This is w.r.t. the stack constraints. But in the case of a TPA, the reachability also depends on the clock constraints: it is sufficient that the guard of an -transition from l to l is satisfiable for l to be reachable from l in the TPA, but it is not necessary. If the guard is not satisfiable, l might still be reachable from l, but through another path. As we have dropped some of the possible such alternative paths, we cannot conclude anymore that the location is completely unreachable.

Figure 6 illustrates the incompleteness of our algorithm. Figure 6(a) presents a TPA. ----------------------------------x 1∧ ← ----------------------------x 1∧ ← -------------------- ---------------------------------------→ l 1 had been added by applying the rule RA 3 . It has not been added because it covers no a new transition between l 0 and l 1 .

C. Coverage

In section IV-B, we have presented a method for computing an RTA from a TPAIO. The algorithm that computes the RTA takes into account the coverage of the transitions of the TPAIO. It adds a new -transition (l, , g, X, l ) only if its path covers a new transition of the TPAIO between the locations l and l . The paths of all the timed -transitions that go to a final location of the RTA cover all the transitions of the TPAIO. But we can not conclude that the indeed test cases cover all the transitions of TPAIO, because the guard of a given timedtransition may not be satisfiable. But, if the guards of all the -transitions that go from an initial location to final location are satisfiable, then all the reachable locations and transitions of the TPAIO are covered. This is the case in our example.

VII. CONCLUSION AND FURTHER WORK We presented a method to generate test from TPAIO that to our knowledge has not been treated in the literature. First, we presented a method that adapts the algorithm defined in [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (ext. abs[END_REF] for computing an RTA from a TPA. The clock constraints are treated by means of backward closure computations, which gives a system of linear inequalities whose satisfiability evaluation is entrusted to an SMT-solver. To keep the method polynomial the computed RTA is incomplete, but it is sound. We additionally compute a path table which associates each transition of the RTA to its paths that can be unfolded as a sequence of transitions of the TPA. Second, this path table allows the generation of tests that cover the locations and transitions found reachable of the TPA. Third, we have distinguished between the inputs and outputs of the TPA for checking the conformance adapted from TAIO to TPAIO of the IU T w.r.t its specification. A further work is to modify the rules defining the RTA for dealing with the -transition cycles while defining a finite RTA. This will lead to a complete, but exponential, algorithm by saturation, that could experimentally be compared for completeness with the one of this paper.

Figure 1 .

 1 Figure 1. Example of a timed pushdown automaton

Figure 2 .

 2 Figure 2. Possibilities of computing an -transition

Figure 3 .

 3 Figure 3. finite partial RTA computation algorithm

Figure 4 .

 4 Figure 4. Test Generation from TPAIO Process

Figure 5 . 1 def=

 51 Figure 5.(a) illustrates this by showing the tester associated to the TPAIO of Fig 1. The label a 1 |a 2 |...|a n denotes the set of labels {a 1 , a 2 , ..., a n }. The notations F 0 to F 4 are the following abbreviations: F 0 def = ?B|?C|?E|?G|pow + , F 1 def = F 0|pow -, F 2 def = ?E|?G|pow + |pow -, F 3 def = ?B|?C|?E|?G|pow -and F 4 def = ?B|?C|pow + |pow -.

Proposition 1 :

 1 Let π = l 0 a0,g0,X0 -----→ l 1 a1,g1,X1 -----→ l 2 a2,g2,X2 -----→ ...l n-1 an-1,gn-1,Xn-1 -----------→ l n an,gn,Xn

Figure 5 .

 5 Figure 5. (a). The tester associated to the TPAIO of Fig 1 and (b) A tree of test cases

Figure 6 (

 6 b) shows the RTA obtained by our algorithm. The location l 1 is not reachable in this RTA, because the two guards of the transitions l 0 ,... --→ l 1 are not satisfiable. However, l 1 is reachable in the TPA. It could have been detected if the transition l 0 ,x 1∧ ← -

1 aFigure 6 .

 16 Figure 6. Example of an RTA (b) incompletely catching the reachability of a TPA (a)


Jacques M Bahi
email: jacques.bahi@femto-st.fr

Nicolas Friot
email: nicolas.friot@femto-st.fr

Christophe Guyeux
email: christophe.guyeux@femto-st.fr

Lyapunov exponent evaluation of a digital watermarking scheme proven to be secure

Keywords: Lyapunov exponent, Information hiding, Security, Chaotic iterations, Digital Watermarking

In our previous researches, a new digital watermarking scheme based on chaotic iterations has been introduced. This scheme was both stego-secure and topologically secure. The stego-security is to face an attacker in the "watermark only attack" category, whereas the topological security concerns other categories of attacks. Its Lyapunov exponent is evaluated here, to quantify the chaos generated by this scheme.

I. INTRODUCTION

In the field of data hiding, it exists a great number of various watermarking schemes [START_REF] Latif | A watermarking scheme based on the parametric slant-hadamard transform[END_REF], [START_REF] Pan | Tabu search based multi-watermarks embedding algorithm with multiple description coding[END_REF], [START_REF] Huang | Metadata-based image watermarking for copyright protection[END_REF], [START_REF] Chen | Extension of structural watermarks based on balanced incomplete block designs[END_REF]. However it currently exists only three data hiding schemes being both stego-secure and topologically secure. The first one is the "Natural Watermarking" with parameter η = 1 [START_REF] Cayre | Kerckhoffs-based embedding security classes for woa data hiding[END_REF]. The two others are based on chaotic iterations. The first of them is a one bit watermarking scheme [START_REF] Guyeux | Chaotic iterations versus spread-spectrum: chaos and stego security[END_REF], [START_REF] Bahi | Steganography: a class of algorithms having secure properties[END_REF], whereas the last one allows steganographic operations [START_REF] Friot | Chaotic iterations for steganography -stego-security and chaossecurity[END_REF]. In order to enlarge the knowledge about the security of these processes, the Lyapunov exponent of the digital watermarking scheme based on chaotic iterations is evaluated here.

This document is organized as follows. In Section II, some basic reminders are given. The semiconjugacy allowing the exponent evaluation is described in Sect. III. In the next one, the exponent is evaluated. This paper ends by a conclusion section where our contribution is summarized.

II. BASIC REMINDERS

A. Chaotic Iterations and Watermarking Scheme

Let us consider a system with a finite number N ∈ N * of cells, so that each cell has a boolean state. A sequence which elements belong into 1; N is a strategy. Finally, the set of all strategies is denoted by 1, N N . Let S n denotes the n th term of a sequence S, and V i the i th component of a vector V .

∀n ∈ N * , ∀i ∈ 1; N , x n i = x n-1 i if S n = i f (x n-1 ) S n if S n = i.
In other words, at the n th iteration, only the S n -th cell is "iterated". Let us now recall how to define a suitable metric space where chaotic iterations are continuous [START_REF] Bahi | Topological chaos and chaotic iterations, application to hash functions[END_REF].

Let δ be the discrete boolean metric, δ(x, y) = 0 ⇔ x = y. Given a function f , define the function:

F f : 1; N × B N -→ B N (k, E) -→ E j .δ(k, j) + f (E) k .δ(k, j) j∈ 1;N
Consider the phase space X = 1; N N × B N , and the map defined on X by:

G f (S, E) = σ(S), F f (i(S), E) , (1)
where σ :

(S n ) n∈N ∈ 1, N N -→ (S n+1 ) n∈N ∈ 1, N N and i : (S n ) n∈N ∈ 1, N N -→ S 0 ∈ 1,
N are respectively the shift and the initial functions. Then chaotic iterations can be described by the following discreet dynamical system:

X 0 ∈ X X k+1 = G f (X k ). (2)
To study whether this dynamical system is chaotic [START_REF] Devaney | An Introduction to Chaotic Dynamical Systems[END_REF], a distance between X = (S, E) and Y = ( Š, Ě) ∈ X has been introduced in [START_REF] Bahi | Topological chaos and chaotic iterations, application to hash functions[END_REF] as follows: d(X, Y ) = d e (E, Ě) + d s (S, Š), where:

d e (E, Ě) = N k=1 δ(E k , Ěk ) and d s (S, Š) = 9 N ∞ k=1 |S k -Šk | 10 k .
This distance has been introduced to satisfy the following requirements. If the floor value ⌊d(X, Y )⌋ is equal to n, then the states E and Ě differ in n cells. In addition, its floating part is less than 10 -k if and only if the first k terms of the two strategies are equal. Moreover, if the k th digit is nonzero, then the k th terms of the two strategies are different. With this metric, and the boolean vectorial negation f 0 , it has been proven in [START_REF] Bahi | Topological chaos and chaotic iterations, application to hash functions[END_REF] that, Theorem 1 G f0 is continuous and chaotic in (X , d).

The digital watermarking scheme proposed in [START_REF] Guyeux | Chaotic iterations versus spread-spectrum: chaos and stego security[END_REF], [START_REF] Bahi | Steganography: a class of algorithms having secure properties[END_REF] is simply the iterations of this dynamical system on the least significant coefficients of the considered media. Each property exhibited by the dynamical system will then be possessed too by the watermarking scheme. For further explanations, see [START_REF] Guyeux | Chaotic iterations versus spread-spectrum: chaos and stego security[END_REF], [START_REF] Bahi | Steganography: a class of algorithms having secure properties[END_REF].

B. The Lyapunov Exponent

Some dynamical systems are very sensitive to small changes in their initial condition, which is illustrated by both the constants of sensitivity to initial conditions and of expansivity [START_REF] Bahi | Topological chaos and chaotic iterations, application to hash functions[END_REF]. However, these variations can quickly take enormous proportions, grow exponentially, and none of these constants can illustrate that. Alexander Lyapunov has examined this phenomenon and introduced an exponent that measures the rate at which these small variations can grow: Definition 2 Given f : R -→ R, the Lyapunov exponent of the system composed by x 0 ∈ R and

x n+1 = f (x n ) is defined by λ(x 0 ) = lim n→+∞ 1 n n i=1 ln f ′ x i-1 .
Consider a dynamic system with an infinitesimal error on the initial condition x 0 . When the Lyapunov exponent is positive, this error will increase (situation of chaos), whereas it will decrease if λ(x 0 ) 0.

Example 1

The Lyapunov exponent of the logistic map [START_REF] Arroyo | On the inadequacy of the logistic map for cryptographic applications[END_REF] becomes positive for µ > 3, 54, but it is always smaller than 1. The tent map [START_REF] Wang | A block cipher with dynamic s-boxes based on tent map[END_REF] and the doubling map of the circle [START_REF] Richeson | Chain recurrence rates and topological entropy[END_REF] have a Lyapunov exponent equal to ln(2).

To evaluate the Lyapunov exponent of our digital watermarking scheme, chaotic iterations must be described by a differentiable function on R. To do so, a topological semiconjugacy between the phase space X and R must be written.

III. A TOPOLOGICAL SEMICONJUGACY A. The Phase Space is an Interval of the Real Line 1) Toward a Topological Semiconjugacy:

We show, by using a topological semiconjugacy, that chaotic iterations on X can be described as iterations on a real interval. To do so, some notations and terminologies must be introduced.

Let S N = 1; N N be the set of sequences belonging into 1; N and X N = S N × B N . In what follows and for easy understanding, we will assume that N = 10. However, an equivalent formulation of the following can be easily obtained by replacing the base 10 by any base N.

Definition 3

The function ϕ : S 10 × B 10 → 0, 2 10 is defined by: ϕ :

X 10 = S 10 × B 10 -→ 0, 2 10 (S 0 , S 1 , . . .); (E 0 , . . . , E 9 ) -→ ϕ (S, E)
where (S, E) = (S 0 , S 1 , . . .); (E 0 , . . . , E 9 ) , and ϕ (S, E) is the real number:

• whose integral part e is 9 k=0 2 9-k E k , that is, the binary digits of e are E 0 E 1 . . . E 9 .

• whose decimal part s is equal to s = 0, S 0 S 1 S 2 . . . = +∞ k=1 10 -k S k-1 . ϕ realizes the association between a point of X 10 and a real number into 0, 2 10 . We must now translate the digital watermarking process G f0 based on chaotic iterations on this real interval. To do so, two intermediate functions over 0, 2 10 denoted by e and s must be introduced: 10 and:

Definition 4 Let x ∈ 0, 2
• e 0 , . . . , e 9 the binary digits of the integral part of x:

⌊x⌋ = 9 k=0 2 9-k e k .
• (s k ) k∈N the digits of x, where the chosen decimal decomposition of x is the one that does not have an infinite number of 9:

x = ⌊x⌋ + +∞ k=0 s k 10 -k-1 .
e and s are thus defined as follows:

e : 0, 2 10 -→ B 10 x -→ (e 0 , . . . , e 9 ) and s : 0, 2 10 -→ 0, 9 N x -→ (s k ) k∈N

We are now able to define the function g, whose goal is to translate the chaotic iterations G f0 on an interval of R. Definition 5 g : 0, 2 10 -→ 0, 2 10 is by definition such that g(x) is the real number of 0, 2 10 defined bellow:

• its integral part has a binary decomposition equal to e ′ 0 , . . . , e ′ 9 , with:

e ′ i = e(x) i if i = s 0 e(x) i + 1 (mod 2) if i = s 0 • whose decimal part is s(x) 1 , s(x) 2 , . . . In other words, if x = 9 k=0 2 9-k e k + +∞ k=0 s k 10 -k-1 , then: g(x) = 9 k=0 2 9-k (e k + δ(k, s 0 ) (mod 2)) + +∞ k=0 s k+1 10 -k-1 .
2) Defining a Metric on 0, 2 10 : Numerous metrics can be defined on the set 0, 2 10 , the most usual one being the Euclidian distance ∆(x, y) = |y -x| 2 . This Euclidian distance does not reproduce exactly the notion of proximity induced by our first distance d on X . Indeed d is richer than ∆. This is the reason why we have to introduce the following metric: Proposition 1 D is a distance on 0, 2 10 .

Proof: The three axioms defining a distance must be checked.

• D 0, because everything is positive in its definition.

If D(x, y) = 0, then D e (x, y) = 0, so the integral parts of x and y are equal (they have the same binary decomposition). Additionally, D s (x, y) = 0, then ∀k ∈ N * , s(x) k = s(y) k . In other words, x and y have the same k-th decimal digit, ∀k ∈ N * . And so x = y. • D(x, y) = D(y, x).

• Finally, the triangular inequality is obtained due to the fact that both δ and |x -y| satisfy it.

The convergence of sequences according to D is not the same than the usual convergence related to the Euclidian metric. For instance, if x n → x according to D, then necessarily the integral part of each x n is equal to the integral part of x (at least after a given threshold), and the decimal part of x n corresponds to the one of x "as far as required". To illustrate this fact, a comparison between D and the Euclidian distance is given Figure 1. These illustrations show that D is richer and more refined than the Euclidian distance, and thus is more precise.

3) The Semiconjugacy: It is now possible to define a topological semiconjugacy between X and an interval of R: Theorem 2 Chaotic iterations on the phase space X are simple iterations on R, which is illustrated by the semicon-jugacy given bellow:

S 10 × B 10 , d G f 0 ----→ S 10 × B 10 , d ϕ     ϕ 0, 2 10 , D ----→ g 0, 2 10 , D
Proof: ϕ has been constructed in order to be continuous and onto.

In other words, X is approximately equal to 0, 2 N .

B. Chaotic Iterations Described as a Real Function

It can be remarked that the function g is a piecewise linear function: it is linear on each interval having the form n 10 , n + 1 10 , n ∈ 0; 2 10 × 10 and its slope is equal to 10.

Let us justify these claims:

Proposition 2 Chaotic iterations g defined on R have derivatives of all orders on 0, 2 All the points of I n have the same integral part e and the same decimal part s 0 : on the set I n , functions e(x) and x → s(x) 0 of Definition 4 only depend on n. So all the images g(x) of these points x:

• Have the same integral part, which is e, except probably the bit number s 0 . In other words, this integer has approximately the same binary decomposition than e, the sole exception being the digit s 0 (this number is then either e + 2 10-s 0 or e -2 10-s 0 , depending on the parity of s 0 , i.e., it is equal to e + (-1) s 0 × 2 10-s 0 ). • A shift to the left has been applied to the decimal part y, losing by doing so the common first digit s 0 . In other words, y has been mapped into 10 × y -s 0 . To sum up, the action of g on the points of I is as follows: first, make a multiplication by 10, and second, add the same constant to each term, which is 1 10

e + (-1) s 0 × 2 10-s 0 -s 0 .

Remark 1 Finally, chaotic iterations used in our watermarking scheme are elements of the large family of functions that are both chaotic and piecewise linear (like the tent map [START_REF] Wang | A block cipher with dynamic s-boxes based on tent map[END_REF]).

We are now able to evaluate the Lyapunov exponent of our digital watermarking scheme based on chaotic iterations, which is now described by the iterations on R of the g function introduced in Definition 5.

IV. EVALUATION OF THE LYAPUNOV EXPONENT

Let L = x 0 ∈ 0, 2 10 ∀n ∈ N, x n / ∈ I , where I is the set of points in the real interval where g is not differentiable (as it is explained in Proposition 2). Then, Theorem 3 ∀x 0 ∈ L, the Lyapunov exponent of chaotic iterations having x 0 for initial condition is equal to λ(x 0 ) = ln [START_REF] Latif | A watermarking scheme based on the parametric slant-hadamard transform[END_REF].

Proof: It is reminded that g is piecewise linear, with a slop of 10 (g ′ (x) = 10 where the function g is differentiable). Then ∀x ∈ L,

λ(x) = lim n→+∞ 1 n n i=1 ln g ′ x i-1 = lim n→+∞ 1 n n i=1 ln |10| = lim n→+∞ 1 n n ln |10| = ln 10.

Remark 2

The set of initial conditions for which this exponent is not calculable is countable. This is indeed the initial conditions such that an iteration value will be a number having the form n 10 , with n ∈ N. We can reach such a real number only by starting iterations on a decimal number, as this latter must have a finite fractional part.

Remark 3 For a system having N cells, we will find, mutatis mutandis, an infinite uncountable set of initial conditions x 0 ∈ 0; 2 N such that λ(x 0 ) = ln(N).

So, it is possible to make the Lyapunov exponent of our digital watermarking scheme as large as possible, depending on the number of least significant coefficients of the cover media we decide to consider. Obviously, a large Lyapunov exponent make it impossible to achieve the well-known Original Estimated Attacks [START_REF] Cayre | Kerckhoffs-based embedding security classes for woa data hiding[END_REF].

V. CONCLUSION AND FUTURE WORKS

As a conclusion, we have available to us now a new quantitative property concerning our digital watermarking scheme based on chaotic iteration: its Lyapunov exponent is equal to ln(N), where N is the number of least significant coefficients of the cover media. This exponent allows to quantify the amplification of the ignorance on the exact initial condition (the media without watermark) after several iterations of the watermaking process. It illustrates the disorder generated by iterations of our watermarking process, reinforcing its chaotic nature.

Using the semiconjugacy described here, it will be possible in a future work to compare the topological behavior of chaotic iterations on X and R, and to explore the topological security of the watermarking scheme using this new topology. Finally, an analogue study of the two other topologically secure schemes will be also conducted in order to compare these processes, being thus able to choose the best one according to the type of applications under consideration.

Definition 1

 1 The set B denoting {0, 1}, let f : B N -→ B N be a function and S ∈ 1, N N . The chaotic iterations are defined by x 0 ∈ B N and

  (a) Function x → dist(x; 1, 234) on the interval (0; 5). (b) Function x → dist(x; 3) on the interval (0; 5).

Figure 1 .Definition 6

 16 Figure 1. Comparison between D (in blue) and the Euclidian distance (in green).