Sébastien Chédor
email: sebastien.chedor@inria.fr

Thierry Jéron
email: thierry.jeron@inria.fr

Christophe Morvan
email: christophe.morvan@univ-paris-est.fr

Test Generation from Recursive Tile Systems

This paper explores the generation of conformance test cases for Recursive Tile Systems (RTSs) in the framework of the classical ioco testing theory. The RTS model allows the description of reactive systems with recursion, and is very similar to other models like Pushdown Automata, Hyperedge Replacement Grammars or Recursive State Machines. Test generation for this kind of infinite state labelled transition systems is seldom explored in the literature. The first part presents an off-line test generation algorithm for Weighted RTSs, a determinizable sub-class of RTSs, and the second one, an on-line test generation algorithm for the full RTS model. Both algorithms use test purposes to guide test selection through targeted behaviours. Additionally, essential properties relating verdicts produced by generated test cases with both the soundness with respect to the specification, and the precision with respect to a test purpose, are proved.

Introduction and motivation

Conformance testing is the problem of checking by test experiments that a black-box implementation behaves correctly with respect to its specification. It is well known that testing is the most used validation technique to assess the quality of software systems, and represents the largest part in the cost of software development. Automation is thus required in order to improve the cost and quality of the testing process. In particular, it is undoubtedly interesting to automate the test generation phase from specifications of the system. Formal model-based testing aims at resolving this problem by the formal description of testing artefacts (specifications, possible implementations, test cases) using mathematical models, formal definitions of conformance and the execution of tests and their verdicts, and the proof of some essential properties of test cases relating verdicts produced by test executions on implementations and conformance of these implementations with respect to their specifications. The ioco conformance theory introduced in 1996 by Tretmans [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF] is now a well established framework for the formal modelling of conformance testing for Input/Output Labelled Transition Systems (IOLTSs). Test generation algorithms and tools have been designed for this model [START_REF] Jard | TGV: theory, principles and algorithms[END_REF][START_REF] Tretmans | Torx: Automated model-based testing[END_REF] and for more general models whose semantics can be expressed in the form of infinite state IOLTSs [START_REF] Jeannet | Model-based test selection for infinite-state reactive systems. 5th International Symposium on Formal Methods for Components and Objects (FMCO'06)[END_REF][START_REF] Frantzen | A symbolic framework for model-based testing[END_REF]. Test generation techniques have also been devised for timed automata models whose semantics are infinite state systems [START_REF] Larsen | Online testing of real-time systems using Uppaal. Formal Approaches to Software Testing (FATES'04)[END_REF][START_REF] Krichen | Conformance testing for real-time systems[END_REF][START_REF] Bertrand | Off-line test selection with test purposes for non-deterministic timed automata[END_REF].

One can distinguish two different approaches in test generation: off-line test generation aims at generating test cases, storing them, and later executing them on the implementation, while in on-line test generation, test cases are generated while executing them on the implementation, taking into account its reactions to stimuli of the test cases. In both cases, formal properties of test suites need be considered, for example, soundness reflects that no conformant implementation may be rejected, while exhaustiveness expresses that every non-conformant implementation is detected by at least one test in the suite.

When considering infinite state systems, undecidability is often an issue. Very simple models like two counters machines lead to the undecidability of the most basic properties (e.g., reachability of a given configuration, occurrence of a given output). Furthermore, provided the description of a reactive system in a given model, the observable behaviour of such a system may not be expressible in this model. In order to establish properties like soundness and exhaustiveness of a generated test-suite, it is convenient to have both a formal description of the system and to be able to prove properties relative to the generated tests. There are several models between finite state and Turing powerful systems; this paper considers a variant of Pushdown automata (PDAs), which provide a nice middle-ground between expressivity and decidability. They form a model for reactive recursive programs, like the running example which represents an abstraction of the one in Figure 1. This example is presented in some Java-like syntax and involves exceptions (a shortcut that is used whenever the keyword throw is used). More precisely the program asks for some integer, then calls the recursive function comp, which asks for a boolean, and, depending on its value, proceeds by making a recursive call or stopping. Whenever exceptions are raised the program branches directly to the catch block of the main function. Along the paper we will only focus on the control flow of this program and abstract data values away. There exist several ways to define recursive behaviours: PDAs, recursive state machines by Alur et al. [START_REF] Alur | Analysis of recursive state machines[END_REF] or regulars graphs, defined by functional (or deterministic) hyperedge replacement grammars (HR-grammars) [START_REF] Courcelle | Handbook of Theoretical Computer Science, chap. Graph rewriting: an algebraic and logic approach[END_REF][START_REF] Caucal | Deterministic graph grammars. Logic and Automata[END_REF]. Each of these models has its merits and flaws: PDAs are classical, and well understood; recursive state machines are equally expressive and more visual as a model; HR-grammars are a visual model which characterizes the same languages and also enables to model systems having states of infinite degree. Furthermore, recent results by Caucal and Hassen define classes of such systems which may be determinized [START_REF] Caucal | Synchronization of grammars[END_REF], which is of interest for test generation. The HR-grammars, on the other hand, are very technical to define. The present paper tries to get the best of both worlds: HR-grammars are presented as tiling systems, called Recursive Tile Systems (RTSs for short). These systems have already been used in the context of diagnosis by Chédor et al. [START_REF] Chédor | Analysis of partially observed recursive tile systems[END_REF]; they are mostly finite sets of finite LTSs with frontiers, crossing the frontier corresponds to entering a new copy of one of the finite LTSs. Additionally, the alphabet of actions is partitioned into inputs, outputs and internal actions. The semantics of an RTS is then defined as an infinite state IOLTS. Hopefully for such models (co)-reachability, which is essential for test generation using test purposes, is decidable. Also determinization is possible for the class of Weighted RTSs, which permits to design off-line test generation algorithms for this sub-class. For the whole class of RTSs however, determinization is impossible, but on-line test generation is still possible as subset construction is performed along finite executions.

static
To the best knowledge of the authors, test generation for recursive programs has been seldom considered in the literature. The work of Constant et al. [START_REF] Constant | Automatic test generation from interprocedural specifications[END_REF], which considers a model of deterministic PDA with inputs/outputs (IOPDS) and generates test cases in the same model is apparently the only previous work with PDAs. The present work can be seen as an extension of this, where non-determinism is taken into account.

Contribution and outline:

The contribution of the paper is as follows. Section 2 recalls the main ingredients of the ioco testing theory for IOLTSs. Section 3 defines the model of RTS for the description of recursive reactive programs, gives its semantics in terms of an infinite state IOLTS obtained by recursive expansion of tiles. Section 4, in the ioco framework, proposes an off-line test selection algorithm guided by test purposes for Weighted RTSs, a determinizable sub-class of RTSs, and proves essential properties of generated test cases. Furthermore, Section 5 provides an on-line test generation algorithm for the full RTS model, also using test purposes for test selection. Eventually, properties of generated test cases are proved.

Conformance testing theory for IOLTSs

This section recalls the ioco testing theory introduced by Tretmans [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF] for the model of Input/Output Labelled Transition Systems (IOLTSs) that will serve as a basis for test generation from RTSs. First a non-standard definition of IOLTSs is given, where marking of states is defined by colours, then notations and basic operations on IOLTSs are introduced. Afterwards several notions are reviewed: the ioco testing theory, with the modelling of test artefacts and their interactions, the central notion of conformance relation, and essential properties requested on test cases.

The IOLTS model and operations

There is a lot of literature relative to IOLTSs. This notion classically boils down to Kripke structures with an alphabet partitioned into inputs, outputs and internal actions. The following definition is not the classical one in the sense that it uses colours to identify sets of states. Furthermore, a colour is also used to single out initial states. Obviously this modification does not affect the properties of IOLTSs, however it will be useful later on in this paper when considering such systems defined by recursive tile systems.

Definition 1 (IOLTS). An IOLTS (Input Output Labelled Transition System) is a tuple

M = (Q, Σ, Λ, → M , C, init)
where Q is a set of states; Σ is the alphabet of actions partitioned into a set of inputs Σ ? , a set of outputs Σ ! and a set of internal actions Σ τ and Σ o Σ ? ∪ Σ ! denotes the set of visible actions1 ; Λ is a set of colours with init ∈ Λ a colour for initial states;

→ M ⊆ Q × Σ × Q is the transition relation; C ⊆ Q × Λ is a

relation between colours and states.

In this non-standard definition of IOLTSs, colours are used to mark states by the relation C. For a colour λ ∈ Λ, C(λ) {q ∈ Q | (q, λ) ∈ C} and C(λ) Q \ C(λ) denote respectively the sets of states coloured and not coloured by λ. In particular, C(init) defines the set of initial states.

Formula q µ -→ M q ′ denotes (q, µ, q ′ ) ∈→ M and q

µ -→ M denotes ∃q ′ : q µ -→ M q ′ .
The first notation is generalized to sequences of actions, and thus q w -→ M q ′ denotes ∃q 0 , . . . , q n : q

= q 0 µ1 -→ M q 1 µ2 -→ M • • • µn --→ M q n = q ′ , with w = µ 1 • • • µ n ∈ (Σ) * .
Such an alternate sequence of states and labelled transitions is called a path. For each of these notations, the subscript M is omitted whenever there is no ambiguity with respect to the IOLTS.

The language of M accepted in a set of states P ⊆ Q noted L P (M) {w ∈ (Σ) * | ∃q 0 ∈ C(init), q ∈ P : q 0 w -→ M q}, is the set of sequences from an initial state to a state in P . In particular L(M) L Q (M) represents the whole set of sequences of M. A sequence is accepted in a colour λ if it is accepted in C(λ) and L λ (M) stands for L C(λ) (M).

For X ⊆ Q a subset of states and

Σ ′ ⊆ Σ a sub-alphabet, post M (Σ ′ , X) = {q ′ ∈ Q | ∃q ∈ X, ∃µ ∈ Σ ′ : q µ -→ M q ′ } denotes the set of successors of a state in X by a single action in Σ ′ , conversely pre M (Σ ′ , X) = {q ∈ Q | ∃q ′ ∈ X, ∃µ ∈ Σ ′ : q µ -→ M q ′ }
denotes the set of predecessors of X by a single action in Σ ′ . The set of states reachable from a set of states P ⊆ Q by actions in Σ ′ is r each M (Σ ′ , P ) lfp(λX.P ∪ post M (Σ ′ , X)) where lfp is the least fixed point operator. Similarly, the set of states coreachable from P ⊆ Q (i.e. the set of states from which P is reachable)

is coreach M (Σ ′ , P ) lfp(λX.P ∪ pre M (Σ ′ , X)). For a colour λ ∈ Λ, r each M (Σ ′ , λ) denotes r each M (Σ ′ , C(λ)) and coreach M (Σ ′ , λ) denotes coreach M (Σ ′ , C(λ)).
For a state q, Γ M (q

) {µ ∈ Σ | q µ -→ M
} denotes the subset of actions enabled in q and respectively, Out M (q) Γ M (q)∩Σ ! and In M (q) Γ M (q)∩Σ ? denote the set of outputs (resp. inputs) enabled in q. The notation is generalized to sets of states: for P ⊆ Q, Out M (P ) q∈P Out M (q) and In M (P ) q∈P In M (q). Visible behaviours of M, which are essential to consider for testing, are defined as usual by the relation

= ⇒ M ∈ Q × ({ǫ} ∪ Σ o ) × Q as follows: q ε = ⇒ M q ′ q = q ′ or q τ1.τ2•••τn ------→ M * q ′ , for τ i ∈ Σ τ and for a ∈ Σ o , q a = ⇒ M q ′ ∃q 1 , q 2 : q ε = ⇒ M q 1 a -→ M q 2 ε = ⇒ M q ′ . The notation is extended to sequences as follows: for σ = a 1 • • • a n ∈ (Σ o ) * a sequence of visible actions, q σ = ⇒ M q ′ stands for ∃q 0 , . . . , q n : q = q 0 a1 = ⇒ M q 1 • • • an = ⇒ M q n = q ′ and q σ = ⇒ M for ∃ q ′ : q σ = ⇒ M q ′ . The formula q after σ {q ′ ∈ Q | q σ = ⇒ M q ′ }
denotes the set of states in which M can be after observing the visible sequence σ starting from the state q. The notation is extended to sets of states: for P ⊆ Q, P after σ q∈P q after σ.

For a state q, Traces(q

) {σ ∈ (Σ o ) * | q σ = ⇒ M
} denotes the set of sequences of visible actions (called traces) that may be observed from q and Traces(M) q0∈C(init) Traces(q 0 ) are those traces from the set of initial states. For a set of states P , Traces P (M) = {σ ∈ (Σ o ) * | (C(init) after σ) ∩ P = ∅} denotes the set of traces of sequences accepted in P .

M is input-complete if in each state all inputs are enabled, possibly after internal actions, i.e. ∀q ∈ Q, ∀µ ∈

Σ ? , q µ = ⇒ M . M is complete in a state q if any action is enabled in q: ∀q ∈ Q, Γ(q) = Σ. M is complete if it is complete in all states.
An IOLTS M is deterministic if |C(init)| = 1 (i.e. there is a unique initial state) and ∀q ∈ Q, ∀a ∈ Σ, |q after a| ≤ 1, where |.| is the cardinal of a set.

From an IOLTS M, one can define a deterministic IOLTS D(M) with the same set of traces as M as follows:

D(M) = (2 Q , Σ o , Λ D , → D , C D , init D ) where for P, P ′ ∈ 2 Q , a ∈ Σ o , P
: C D (F ) = {s ∈ 2 Q | s ∩ C(f ) = ∅}.
Observe that the definition of D(M) is not always effective (meaning that the process may not always be carried out in finitely many steps by some algorithm). However, it is the case whenever M is a finite state IOLTS. Even when it is effective, such a transformation may lead to an exponential blow-up. Often, for efficiency reasons, the full construction of D(M) is avoided, and on-the-fly paths are computed (visiting only a limited part of the powerset).

Synchronous product of IOLTSs: As usual, one may define a product of two IOLTSs such that sequences of actions in the product IOLTS are the sequences of actions of both IOLTSs. The product of IOLTSs thus implements the intersection of (accepted) languages:

Definition 2 (Synchronous product). Let M i = (Q i , Σ, Λ i , → i , C i , init i ), i = 1,
2 be two IOLTSs with same alphabet Σ. Their synchronous product M 1 × M 2 is the IOLTS P = (Q P , Σ, Λ P , → P , C P , init P ) such that

Q P Q 1 × Q 2 , and ∀(q 1 , q 2 ), (q ′ 1 , q ′ 2 ) ∈ Q P , ∀µ ∈ Σ, (q 1 , q 2 ) µ -→ P (q ′ 1 , q ′ 2 ) q 1 µ --→ M1 q ′ 1 ∧ q 2 µ --→ M2 q ′ 2 . We define Λ P Λ 1 × Λ 2 , in particular init P (init 1 , init 2 )
, and for any (λ 1 , λ 2 ) ∈ Λ P the colouring relation is defined by

C P ((λ 1 , λ 2 )) C 1 (λ 1 ) × C 2 (λ 2 ).
As usual, for P i ⊆ Q i , i = 1, 2 the following holds:

L P1×P2 (M 1 × M 2 ) = L P1 (M 1 ) ∩ L P2 (M 2 ) and in particular L(M 1 × M 2 ) = L(M 1 ) ∩ L(M 2 ) for the case where P i = Q i , i = 1, 2.
Parallel composition of IOLTSs: The parallel composition of IOLTSs is a binary operation used to formalize the synchronous interaction between two IOLTSs. In this interaction, inputs of one IOLTS are synchronized with outputs of the other one, and vice versa. This operation is used to describe the execution of test cases on an implementation.

Definition 3 (Parallel composition). Let M i = (Q i , Σ i , Λ i , → i , C i , init i ), i = 1,
? 1 = Σ ! 2 ). Their parallel composition is the IOLTS M 1 M 2 = (Q M , Σ M , Λ M , → M , C M , init M ) with Q M = Q 1 × Q 2 , Σ M = Σ 1 , Λ Λ 1 × Λ 2 , in particular init (init 1 , init 2 ), for any (λ 1 , λ 2 ) ∈ Λ the colouring relation is defined by C((λ 1 , λ 2 )) C 1 (λ 1 ) × C 2 (λ 2 )
, and the transition relation is defined by the rules:

a ∈ Σ o q 1 a --→ M1 q ′ 1 q 2 a --→ M2 q ′ 2 (q 1 , q 2 ) a -→ M (q ′ 1 , q ′ 2 ) q 1 τ --→ M1 q ′ 1 (q 1 , q 2 ) τ -→ M (q ′ 1 , q 2 ) q 2 τ --→ M2 q ′ 2 (q 1 , q 2 ) τ -→ M (q 1 , q ′ 2 )
Synchronization being defined on visible actions, thus, for

P i ⊆ Q i , i = 1, 2 the following holds Traces P1×P2 (M) = Traces P1 (M 1 ) ∩ Traces P2 (M 2 )
, and in particular Traces(M) = Traces P1 (M 2 ) ∩ Traces P2 (M 2 ). Note that this definition is not completely symmetric: the direction of actions (output, input) is given by the first operand.

The ioco testing theory

Specification and implementation: In the ioco testing framework, it is assumed that the behaviour of the specification is modelled by an IOLTS M = (Q, Σ, Λ, → M , C, init). The implementation under test is a black box system with same observable interface as the specification. In order to formalize conformance, it is usually assumed that the implementation behaviour can be modelled by an (unknown) input-complete IOLTS I = (Q I , Σ I , Λ I , → I , init I ) with Σ I = Σ ? I ∪ Σ ! I ∪ Σ τ I and Σ ? I = Σ ? and Σ ! I = Σ ! . The input-completeness assumption means that the implementation is always ready to receive inputs from its environment, in particular from test cases. In the sequel, the set of implementations, with alphabet compatible with M, is denoted by IMP(M).

Quiescence: It is current practice that tests observe traces of the implementation, and also absence of reaction (quiescence) using timers. Tests should then distinguish between quiescences allowed or not by the specification. Several kinds of quiescence may happen in an IOLTS: a state q is output quiescent if it is only waiting for inputs from the environment, i.e. Γ(q) ⊆ Σ ? , (a deadlock i.e. Γ(q) = ∅ is a special case of output quiescence), and a livelock if an infinite sequence of internal actions is enabled, i.e. ∀n ∈ N, ∃σ ∈ (Σ τ ) n , q σ -→ M2 . Whenever q is an output quiescence or in a livelock is denoted by quiescent(q). From an IOLTS M one can define a new IOLTS ∆(M) where quiescence is made explicit by a new output δ:

Definition 4 (Suspension). Let M = (Q, Σ, Λ, → M , C, init) be an IOLTS, the suspension of M is the IOLTS ∆(M) = (Q, Σ ∆(M) , Λ, → ∆(M) , C, init) where Σ ∆(M) = Σ ∪ {δ} with δ ∈ Σ ! ∆(M)
(δ is considered as an output, observable by the environment), and the transition relation → ∆(M) → M ∪{(q, δ, q) | q ∈ quiescent(M )} is obtained from → M by adding δ loops for each quiescent state q.

Note that ∆(M) might be not computable for infinite state IOLTSs. In the sequel, the sets Σ ! ∪ {δ} and Σ o ∪ {δ} are respectively denoted by Σ !δ and Σ oδ . The traces of ∆(M) denoted by STraces(M) are called the suspension traces of M. They represent the visible behaviours of M, including quiescence, and are the basis for the definition of the ioco conformance relation.

Conformance relation:

In the ioco formal conformance theory [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF], given a specification IOLTS M, an implementation I ∈ IMP(M) is said to conform to its specification M if, after any suspension trace σ of M, the implementation I exhibits only outputs and quiescences that are specified in M. Formally:

Definition 5 (Conformance relation). Let M be an IOLTS and I ∈ IMP(M) be an input-complete IOLTS with same visible alphabet (i.e. Σ ? = Σ ?

I and Σ ! = Σ ! I ),

I ioco M ∀σ ∈ STraces(M), Out(∆(I) after σ) ⊆ Out(∆(M) after σ).
It can be proved [START_REF] Jeannet | Model-based test selection for infinite-state reactive systems. 5th International Symposium on Formal Methods for Components and Objects (FMCO'06)[END_REF] that I ioco M if and only if STraces(I) ∩ MinFTraces(M) = ∅, where MinFTraces(M) STraces(M).Σ ! \ STraces(M) is the set of minimal (with respect to the prefix ordering) non-conformant suspension traces. Notice that the set of all non-conformant traces is then MinFTraces(M).Σ * . This alternative characterisation of ioco will be useful in the sequel, in particular for the description of properties of test cases.

Test cases, test suites, properties: In order to complete the formal background, a definition of test cases and test suites (sets of test cases) is provided together with their expected properties relatively to conformance. In practice a test case describes the interaction that should be played when checking conformance of an implementation and the verdicts associated to this interaction. In the present formal setting, the behaviour of a test case is modelled by an IOLTS equipped with colours representing verdicts assigned to executions.

Definition 6 (Test case, test suite). A test case for M is a deterministic and input-complete IOLTS

T C = (Q T C , Σ T C , Λ T C , → T C , C T C , init T C ) where Pass, Fail, Inc, None ∈ Λ T C are colours characterising verdicts such that C T C (Pass), C T C (Fail), C T C (Inc) and C T C (None) form a partition of Q T C and for λ ∈ {Pass, Fail}, r each T C (Σ, Λ) ⊆ C T C (λ) and r each T C (Σ, Inc) ⊆ C T C (Inc) ∪ C T C (Fail). The alphabet is Σ T C = Σ ? T C ∪ Σ ! T C where Σ ? T C = Σ !δ and Σ ! T C = Σ ? (

outputs of T C are inputs of M and vice versa). A test suite is a set of test cases.

The execution of a test case T C against an implementation I can be modelled by the parallel composition T C ∆(I) where common actions (inputs, outputs and quiescence) are synchronized. The effect is to intersect sets of suspension traces of I with traces of T C (Traces(T C ∆(I)) = STraces(I) ∩ Traces(T C)). Consequently, the possible failure of a test case on an implementation is defined as the fact that the interaction of I and T C may lead to a state coloured by F ail in T C. Using properties of traces of the parallel composition, this is formalized by

I fails T C STraces(I) ∩ Traces C T C (Fail) (T C) = ∅.
Notice that I fails T C only means that I may be rejected by T C, depending on choices made by I in its interaction with T C. Similar definitions can be given for passes and inconc relative to the verdicts Pass and Inc. Now follows formal definitions of properties that should be satisfied by test cases in order to correctly relate conformance to rejection by a test case: Definition 7 (Test suites properties). Let M be a specification, and T S a test suite for M.

• T S is sound if no test case may reject a conformant implementation:

∀I ∈ IMP(M), (I ioco M =⇒ ∀T C ∈ T S, ¬(I fails T C)).
• T S is exhaustive if it rejects all non-conformant implementations:

∀I ∈ IMP(M), (¬(I ioco M) =⇒ ∃T C ∈ T S, I fails T C).
• T S is complete if it is both sound and exhaustive.

• T S is strict if it detects non-conformances as soon as they happen:

∀I ∈ IMP(M), ∀T C ∈ T S, ¬(T C I ioco M) ⇒ I fails T C.
The following characterisations of soundness, exhaustiveness and strictness, derived from [START_REF] Jeannet | Model-based test selection for infinite-state reactive systems. 5th International Symposium on Formal Methods for Components and Objects (FMCO'06)[END_REF], are very convenient to prove that generated test suites satisfy those properties. They are obtained by replacing ioco by its alternative characterization, fails by its definition, replacing universal quantification on T C by a union, and suppressing the universal quantification on I, using an argument on sets to replace implication by inclusion.

Proposition 1 ([4]

). Let T S be a test suite for M,

• T S is sound if T C∈T S Traces C T C (Fail) (T C) ⊆ MinFTraces(M).Σ * , • T S is exhaustive if MinFTraces(M) ⊆ T C∈T S Traces C T C (Fail) (T C), • T S is strict if ∀T C ∈ T S, Traces(T C) ∩ MinFTraces(M) ⊆ Traces C T C (Fail) (T C).
(According to earlier notations, the set Traces C T C (Fail) (T C)) is formed by the traces in T C leading to a state with colour Fail.)

Informally, soundness is characterized by the fact that traces of test cases leading to Fail are non-conformant traces. Exhaustiveness means that all non-conformant traces are recognized in Fail states of some test case. Furthermore, strictness means that traces of test cases which are minimal non-conformant ones lead to a Fail state.

Recursive Tile Systems and their properties

This section provides a definition for the Recursive Tile Systems (RTSs), a model finitely representing infinite state IOLTSs inspired from the regular graphs of Courcelle [START_REF] Courcelle | Handbook of Theoretical Computer Science, chap. Graph rewriting: an algebraic and logic approach[END_REF]. These systems form classical middle-ground between finite state systems and Turing-complete ones. They are expressive enough to model recursive systems, yet many properties remain decidable. RTSs in particular are graphical finite representations, as such they seem simple and intuitively close to finite IOLTSs. The present section introduces some algorithms and properties of RTSs: ε-closure (suppression of internal actions), product and determinization. These properties are useful for test generation which will be discussed in the next section.

Recursive tile systems

Roughly speaking an RTS is a finite collection of finite transition systems (called tiles) together with identifications enabling to connect these tiles. Each RTS generates a single infinite IOLTS composed of finite patterns which correspond to the tiles. Definition 8 (Recursive tile system). A recursive tile system (RTS) is a tuple R = ((Σ, Λ), T , t 0 ) where

• Σ = Σ ? ∪ Σ ! ∪ Σ τ is

a finite alphabet of actions partitioned into inputs, outputs and internal actions,

• Λ is a finite set of colours with a particular one init marking initial states.

• T is a set of tiles t

A = ((Σ, Λ), Q A , → A , C A , S A , F A ) defined on (Σ, Λ) where -Q A ⊆ N is the set of vertices, -→ A ⊆ Q A × Σ × Q A is a finite set of transitions, -C A ⊆ Q A × Λ is a finite set of coloured vertices, -S A ⊆ Q A is the support -F A ⊆ T × 2 N×N ,
the frontier, relates to some tile, t B , a partial function (often denoted f B ) over N, associating to each vertex of the support S B , vertices of Q A .

• t 0 ∈ T is an initial tile (the axiom), with S 0 = ∅.

Each single tile t A defines an IOLTS

[t A ] = (Q A , Σ, Λ, → A , C A , init
) in a straightforward way when ignoring the support and frontier.

The tiling operation (that will be defined later on) inductively constructs an IOLTS from an RTS. The support of a tile indicates vertices which may be attached to other tiles, in the tiling operation. The frontier F A of a tile t A defines which tiles t B are attached to t A along the tiling, it also specifies how vertices of the support of t B are merged with vertices of t A by this operation.

The V -frontier of any tile t A , is the set formed by the vertices which belong to the image of any function in the frontier, formally, V -frontier

= {f B | (t B ,f B )∈F A } Im(f B ).
Example 1. The program depicted on Fig. 1, may be abstracted in the following RTS: R = ((Σ, Λ), T , t main ) with Σ τ = {try, throw, catch, intern}, Σ ? = {int, true, false}, Σ ! = {m1, m2, m3, m4}, Λ = {init, succ}, a set of tiles T = t main , t comp (a graphical presentation of these tiles is depicted on Fig. 2), and t main the initial tile. The output actions correspond to messages: m1 is Done, m2 is An error has occurred, m3 is Some text and m4 is You stopped. The symbol int stands for the integer input, and observe that the actual value of this input is not reflected by the structure of the RTS, inputs true, false reflect the boolean input in block 4. The symbol intern reflects the unlabelled internal action in block 5 (the computation).

• t main = ((Σ, Λ), Q main , → main , C main , S main , F main ) with Q main = {0, 1, 2, 3, 4, 5, 6}, C main = {(0, init)} (init depicted by ✸) S main = ∅, F main = (t comp , {0 → 2, 2 → 3, 5 → 4})
, and → main depicted below, means that (t comp , {0 → 2}) belongs to F main , i.e. the vertex 0 of t comp is associated to the vertex 2 of t main .

• t comp = ((Σ, Λ), Q comp , → comp , C comp , S comp , F comp ) with Q comp = {0, 1, 2, 3, 4, 5}, → comp C comp = {(2,
The semantics of an RTS is formally defined by an IOLTS by a tiling operation that appends tiles to another tile (initially, the axiom), inductively defining an IOLTS. Formally, given a set of tiles T and a tile

t E = ((Σ, Λ), Q E , → E , C E , S E , F E ) with F E defined on T , the tiling of t E by T , denoted by T (t E ), is the tile t ′ E = ((Σ, Λ), Q ′ E , → ′ E , C ′ E , S ′ E , F ′ E )
iteratively defined according to the elements of the frontier F E , as follows:

1. Initially, Q ′ E = Q E , → ′ E =→ E , C ′ E = C E , S ′ E = S E , F ′ E = ∅; 2. For each pair (t B , f B ) ∈ F E , with t B = ((Σ, Λ), Q B , → B , C B , S B , F B ) ∈ T B , let ϕ B : Q B → N be the injection mapping vertices of Q B to new vertices of Q ′ E with ϕ B (n) := f B (n) whenever n ∈ dom(f B ), n + max(Q ′ E ) + 1 otherwise, where max(Q ′ E )
is the vertex with greatest value in Q ′ E . The tile t ′ E is then defined by:

• Q ′ E = Q ′ E ∪ Im(ϕ B ), • S ′ E = S ′ E , • → ′ E =→ ′ E ∪ {(ϕ B (n), a, ϕ B (n ′ )) | (n, a, n ′ ) ∈→ B }, • C ′ E = C ′ E ∪ {(ϕ B (n), λ) | (n, λ) ∈ C B }, • F ′ E = F ′ E ∪ {(t C , {(ϕ B (j), f C (j)) | j ∈ dom(f C )}) | (t C , f C ) ∈ F B }.
The update of F ′ expresses that the frontier of the new tile t ′

A is composed from those of the tiles that have been added. Remark 1. In a tiling, the order chosen to append a copy of the tiles that belong to the frontier is not important. Two different orders would produce isomorphic tiles (the same tiles up to renaming of the vertices). More precisely, one could define an order on the way to append tiles from the frontier and thus produce a single possible tile after the tiling. This process would be long and intricate. The benefit would be limited since every possible order produces an isomorphic tile (up to a renaming of vertices). Hence, the choice, here, is not to fix this order, enabling the production of several isomorphic semantics for a given RTS.

Example 2. The principle of tiling is illustrated now, using the RTS defined in Example 1. Consider that t main is the initial tile (it has empty support). Its tiling T (t main ), is performed as follows: there is a single element in its frontier; a copy of t comp (with new vertices) is added, identifying vertices 2, 3 and 4 of t main to vertices 0, 2 and 5 (the support) of t comp .

The resulting tile is depicted in Fig. 3 (top). This new tile may be in turn extended by adding a copy of t comp , identifying 4, 10 and 11 respectively to 0, 2 and 5. Again, the resulting tile is illustrated in Fig. 3 (bottom) (observe that the definition of ϕ comp induces that some elements of N are left out). Obviously iterating this process will result in vertex 4 having infinite in-degree.

An IOLTS is finally obtained from an RTS as the union of the IOLTSs of tiles resulting from the iterated tilings from the axiom. Formally, Definition 9 (Semantic of an RTS). Let R = ((Σ, Λ), T , t 0 ) be an RTS.

R defines an IOLTS R = (Q R , Σ, Λ, → R , C R , init) given by k [T k (t 0 )]
The infinite union of Definition 9 is valid because, by construction, for all k ≥ 0: [T k (t 0 )] ⊆ [T k+1 (t 0 )], where ⊆ is understood as the inclusion of IOLTSs, i.e. inclusion of states, transitions and colourings.

For an RTS R with axiom t 0 , and a state q in R , ℓ(q) denotes the level of q, i.e. , the number of tiling operations needed to create q, formally, the least k ∈ N such that q is a state of [T k (t 0 )]. Also, t(q) denotes the tile in T that created q. For a vertex v of a tile of R, v denotes the set of states in R corresponding to v.

Requirement 1. In order to simplify computations, some technical restrictions are imposed on the RTS, R = ((Σ, Λ), T , t 0 ), that can be ensured by a normalization 3 step, without loss of generality:

1. for any state q of finite degree in R , every transition connected to q is either defined in t(q) or one of the tiles of its frontier (this may be checked on T );

2. the set of enabled actions in copies of a vertex v is uniform (for all vertices v in R, for all q, q ′ in v , Γ R (q) = Γ R (q ′ )), thus can be written Γ R ( v ). Furthermore, one may assume that each vertex possesses a colour reflecting this value (see Corollary 1 below). The first restriction will simplify the computation of the Σ τ -closure (this operation will be defined in Section 3.3), and the second will simplify the computation of the suspended specification.

Remark 2. The IOLTSs obtained from RTSs correspond to the equational, or regular graphs of respectively Courcelle and Caucal [START_REF] Courcelle | Handbook of Theoretical Computer Science, chap. Graph rewriting: an algebraic and logic approach[END_REF][START_REF] Caucal | Deterministic graph grammars. Logic and Automata[END_REF]. These IOLTSs are derived from an axiom using deterministic HR-grammars. Each such grammar may be transformed into a tiling system, and conversely. Deterministic HR-grammars are defined by sets of graphrewriting rules. Each left-hand side is formed by a non-terminal hyperedge (corresponding to the notion of support in tiles). Each right-hand side is formed by a finite hypergraph. In this hypergraph, the set of non-terminal hyperedges corresponds to the frontier, terminal hyperedges are ordinary transitions. This definition of RTSs aims at a greater simplicity by focusing the definition on a finite set of graphs rather than a finite set of rules, and removing hyperedges which are only a syntactical element used to connect tiles.

Reachability of RTSs

This subsection presents fundamental results on RTSs with respect to the formal generation of test suites. In particular to detect quiescent states, and to prune the canonical tester.

Reachability.

Computation of (co)reachability sets, that are central for verification and safety problems, as well as for test generation with test purposes, are effective for RTSs: Proposition 2 ( [START_REF] Caucal | Deterministic graph grammars. Logic and Automata[END_REF]). Given an RTS R = ((Σ, Λ), T , t 0 ), a sub-alphabet Σ ′ ⊆ Σ, a colour λ ∈ Λ, and a new colour r λ ∈ Λ, an RTS R ′ can be effectively computed, such that R ′ is isomorphic to R with respect to the transitions and the colouring by Λ, and states reachable from a state coloured λ by actions in Σ ′ are coloured r λ :

C R ′ (r λ ) = r each R (C R (λ), Σ ′ ).
The same result holds for states co-reachable from λ.

Proposition 2 is established, for regular graphs, by Caucal [START_REF] Caucal | Deterministic graph grammars. Logic and Automata[END_REF], the resulting system may be of exponential size in the size of the largest support. However, in the following we will first use a normal form (of quadratic size), such that the size of the support of each tile will have size 2. Hence, with respect to the computations we are performing, reachability computation takes polynomial time. Now, in Caucal [START_REF] Caucal | Deterministic graph grammars. Logic and Automata[END_REF], Proposition 3.13 enables to perform several computations related to the purpose of this paper. The following proposition is a reformulation for RTSs.

Proposition 3 ([11]

). Given an RTS R = ((Σ, Λ), T , t 0 ), for any subset S in N ∪ {∞} and new colour # S ∈ Λ, it is possible to compute an RTS R ′ = ((Σ, Λ ∪ {# S }), T ′ , t ′ 0 ) such that R is isomorphic to R ′ with respect to the transitions and the colouring by Λ, and every state of R ′ of (in-or out-or total-) degree in S is coloured by # S . This computation may be performed in linear time: in a given tile t the neighbourhood of each vertex, not in its support, only depends on t and possibly the tiles in its frontier.

Proposition 3 enables to identify directly on the set of tiles some state properties, like deadlocks, inputlocks. The following corollary is also a direct consequence of this proposition (performing successively, for each action a, a colouring for the degree related to a).

Corollary 1. Given an RTS R and a vertex v of a tile t of R, for any state q in v , the allowed actions Γ R (q) in q can be effectively computed.

Σ τ -closure of RTSs

Abstracting away internal transitions (labelled by actions in Σ τ ) is important to compute the next observable actions after a trace, thus for test generation. While the following proposition shows it is possible to do it for RTSs, the rest of the subsection will be devoted to establish a more precise result (Proposition 5) and will provide an algorithm to perform the Σ τ -closure of RTSs.

Proposition 4. From an RTS R with IOLTS R = (Q R , Σ, Λ, → R , C R , init) and visible actions Σ o ⊆ Σ, one can effectively compute an RTS Clo(R) with same colours Λ, whose IOLTS Clo(R) = (Q ′ R , Σ o , Λ, → ′ R , C ′ R , init
) has no internal action, is of finite out-degree, and for any colour λ ∈ Λ,

Traces C R (λ) ( R ) = Traces C ′ R (λ) ( Clo(R)
). This result is classical for pushdown systems and regular graph; it follows mainly from the work of Caucal [START_REF] Caucal | Deterministic graph grammars. Logic and Automata[END_REF] and can be adapted to RTSs: from a given RTS (labelled by Σ τ ∪ Σ o ), a context-free grammar generating the same set of traces (in Σ o * ) may be constructed, then from such a grammar an RTS of finite degree may be constructed. Now follows a direct construction, in order to provide an accurate evaluation of the complexity of the process, and to assess which properties of the original RTS are preserved. In particular our construction will take colours into account since it is essential for the generation of tests cases. First, a careful examination of which equivalence between IOLTSs may be considered, is performed. Then, a specific computation of the Σ τ -closure of an IOLTS (preserving this equivalence) is proposed. Since this new computation is not effective for infinite state systems, a direct transformation on RTSs (performing this computation for the generated IOLTSs) is given.

Equivalence for IOLTSs.

The computation of a closure for transition systems is usually focused on traces preservation, and performed either by forward or backward computation. Since, in this paper, the states of IOLTSs have colours, such a straightforward computation may result in the loss of important information, indeed, from Proposition 3, deadlocks, outputlocks, hence quiescence are specified by colours. Thus, a notion of coloured traces is introduced in order to obtain a finer equivalence, preserving this information.

Coloured traces, and coloured equivalence. A coloured trace is a finite sequence in (Λ.(Σ o ) + ) + .Λ. A coloured trace λ 1 w 1 λ 2 w 2 ...λ n is recognized by an IOLTS M = (Q, Σ, Λ, →, C, init) if there exists n states q 1 , q 2 , ..., q n such that for all 1 ≤ k ≤ n -1, q k w k = ⇒ q k+1 , and for all 1 ≤ k ≤ n, q k ∈ C(λ k ).

Observe that paths in this definition do not necessarily start from a state coloured by init. Moreover, given a path in some IOLTS, several distinct coloured traces might be defined from this same path since a state can have several colours. Finally, the empty word may not label a coloured trace, this is an arbitrary choice guided by a technical reason: preserving ε-labelled coloured traces would be much more difficult and impose a much more complex definition of colours in states.

Definition 10 (Coloured equivalence). Let M and M ′ be two IOLTSs. M and M ′ are coloured equivalent whenever they recognise the same coloured traces.

The coloured equivalence is more precise than trace equivalence, since two coloured equivalent systems have the same traces (up to the empty word) whereas the converse if not true in general. Conversely coloured equivalence is less precise than bisimulation.

Mixed closure.

The purpose is eventually to compute the closure, with respect to internal events in Σ τ , of IOLTSs defined by RTSs. A naive approach to accomplish such a computation would be to perform it in each tile. Unfortunately both forward and backward closures face difficulties to deal with states generated at the V -frontier of some tile. Hence the introduction of a general process: mixed closure which will be suited to RTSs and furthermore will preserve coloured traces. This subsection presents the principles of mixed closure for IOLTSs and the next one will present its adaptation to systems generated by RTSs.

Roughly speaking this approach simply consists in adding a new state for each pair of states connected by a Σ τlabelled transition (Σ τ -transition for short), connecting this new state to each predecessor of the source of the transition and to each successor of the target. Whenever there exist strongly connected components labelled by actions in Σ τ , this process will proceed forever. Hence this technique will first eliminate these cycles.

In order to present the mixed closure, consider an IOLTS M = (Q, Σ, Λ, → M , C, init) having Σ τ labelled transitions. Let Clo(M) = (Q Clo , Σ, Λ, → Clo , C Clo , init) be the resulting mixed closure of M. This system is obtained after several iterations constructing intermediate IOLTSs denoted by M i with sets of states, transitions and colouring denoted respectively by Q i , → i , C i (observe that the sets of labels and of colours are not modified). We now start by considering strongly connected components of Σ τ -transitions, then we will perform the closure of remaining unobservable transitions.

Strongly connected component of Σ τ -transitions. Let {C 1 , . . . , C N } be the set of maximal strongly connected components (SCCs) of Σ τ -transitions in M. Let M 0 M, then, for all i = 1 . . . N -1, the states, transitions, and colouring of M i+1 are as follows:

• Q i+1 Q i ∪ {q i } with qi a new state; • For all states q of Q i+1 , C i+1 (q) = p∈Ci C i (p) if q = qi , C i+1 (q) = C i (q) otherwise; • → i+1 → i \ {(q, µ, q ′ ) | q, q ′ ∈ C i } ∪ {(q, µ, qi ) | ∃q τ ∈ C i , µ ∈ Σ, (q, µ, q τ ) ∈→ i } ∪ {(q i , µ, q) | ∃q τ ∈ C i , µ ∈ Σ, (q τ , µ, q) ∈→ i } .
For all i = 1 . . . N -1, M i+1 has the same coloured traces as M i (hence same as M) since paths having no transitions in Σ τ are preserved and those having such transitions may only have at most one colour of a sequence in (Σ τ ) + and each such colour is kept.

Closure of remaining Σ τ -transitions. Assume that M has been transformed into M N (where N is the total number of SCCs in M), and thus has no strongly connected component of Σ τ . Now, internal transitions are iteratively suppressed by defining new IOLTS M N +1 , . . . , M N +k as follows, starting from

M i = M N .
If there exists a transition q 1 τ → q 2 ∈→ i for some τ ∈ Σ τ , then the states, transitions, and colouring of M i+1 are as follows:

• Q i+1 Q i ∪ {q 12 } with q12 a new state; • For all states q of Q i+1 , C i+1 (q) = C i (q 1 ) ∪ C i (q 2 ) if q = q12 , C i+1 (q) = C i (q) otherwise; • → i+1 → i \ {(q 1 , τ, q 2 )} ∪ {(q, µ, q12 ) | q ∈ Q i , µ ∈ Σ, (q, µ, q 1 ) ∈→ i } ∪ {(q 12 , µ, q) | q ∈ Q i , µ ∈ Σ, (q 2 , µ, q) ∈→ i } .
For all i ≥ N , M i+1 has the same coloured traces as M i (hence same as M) since the only transformation is to replace a single internal transitions by a single state having both colours of the states connected by this transition (and all in-transitions of the sources, and all out-transitions of the target), and coloured traces have at least one visible action between two consecutive colours. Eventually the closure of M, Clo(M), has the same coloured traces as M.

Whenever the system M has finitely many states, the resulting system Clo(M) is obtained after finitely many steps (reducing the length of a sequence of internal transitions at each step). In general this may not be applied for infinite state IOLTSs.

Effective mixed closure for RTSs.

Even though the construction of the mixed closure is not effective for infinite state systems in general, it is possible to adapt this construction for RTSs by transforming the tiles of an RTS and construct another coloured equivalent RTS. Observe, also, that a non-careful transformation could produce states of infinite degree which is often not desirable. The transformation presented here will avoid producing such states.

The most naive approach to compute mixed closure for a system generated by a RTS would be to proceed for each tile independently. This idea fails whenever some internal transitions are connected to the support or to a vertex of the V -frontier of a tile. It fails even more blatantly when a sequence of such transitions connects a vertex of the support to one of the V -frontier. In order to solve these problems, a normal form (introduced in Hassen's PhD thesis [START_REF] Hassen | Synchronisation de grammaires de graphes[END_REF][START_REF] Caucal | Synchronization of grammars[END_REF]) is presented and followed by a technique that removes paths of internal transitions traversing tiles from the support to the V -frontier (or conversely). The final step consists in iterating a finite closure in each tile.

Path tiles. Path tiles is a normal form of RTS which focuses on paths. This normal form transforms the generated IOLTS by duplicating some paths while preserving coloured traces. It allows a simple application of the mixed closure assuming that there are no paths of Σ τ actions traversing any tile from support to V -frontier.

A path tile is a tile whose support is composed of at most one vertex having null in-degree and at most one with null out-degree.

Given any RTS it is possible to construct a coloured-equivalent RTS having only path tiles. This construction is straightforward and consists simply, for any original tile t A , and any pair of vertices v and v ′ (which may not be distinct) in the support of t, in constructing a new tile t Avv ′ having v and v ′ as support (when they are identical two distinct vertices will be present in t Avv ′ ), and respectively v and v ′ with null in and out-degree. The tile t Avv ′ contains only the out-transitions from v, and in-transitions to v ′ , and vertices of t reachable from v and co-reachable from v ′ . The frontier is defined accordingly splitting each tile in the frontier into each of its components (according to this decomposition). Two other tiles, t Avo and t Avi , are defined for v, having respectively null out-and in-degree, and containing only, respectively, states reachable and co-reachable from v (the frontier is built similarly).

This transformation duplicates several states but enables complete preservation of coloured traces. Furthermore it produces a quadratic number of tiles (in the cardinality of the supports).

Removing Σ τ -paths between support and V -frontier. There are two symmetrical operations. Only the one removing internal transitions from the support to the V -frontier is presented here.

From the previous construction, without loss of generality, one may assume that the RTS M is only formed of path tiles (for the sake of simplicity the same convention as in the previous paragraph is assumed for the name of those tiles).

Let t Avv ′ be a tile of M having Σ τ -paths from v to elements of the V -frontier. The following step is iterated to construct a new tile t ′ Avv ′ which will not have any traversing Σ τ -paths, or traversing paths reaching tiles that have already been traversed:

For each v ′′ in the V -frontier of t Avv ′ , with (t Bww ′ , v B , v ′′ ) ∈ F A , target of a Σ τ -path from v, tile t Avv ′ with t Bww ′ .
Then, for each vertex, v B , of the V -frontier, connected to some tile t Bww ′ which is target of a Σ τ -path, identify the vertex, v ′ B , corresponding to the previous occurrence of t Bww ′ (which is always possible from the halting condition of the previous iteration).

For each transition v µ → v B , with ℓ(v) ≥ ℓ(v B ) (appearing in or after the occurrence of t Bww ′ ), add a transition

v µ → v ′ B .
When all these transitions have been added, remove v from the frontier of the constructed tile. Iterating the previous process for each tile reached by a Σ τ -path, the resulting tile, denoted by t ′ Avv ′ has no traversing Σ τ -path. Iterating this process on each tile produces a coloured equivalent RTS with no Σ τ -path.

The removal of paths from the V -frontier to the support is performed similarly, except that the transitions are considered the opposite way.

In order to perform these operations, an exponential number of tiles may be appended to each original tile. Every path in a tree need to be considered to remove traversing Σ τ -paths. Note, however, that in order to reach such an important size a considerable amount of traversing Σ τ -paths needs to exists in the system.

Removing internal paths. Now in order to perform the mixed closure, first SCCs of internal transitions need to be identified. Since there are no traversing Σ τ -paths, each SCC either fully belongs to a tile or belongs to adjacent tiles. Hence the closure of internal transitions between elements of the support may be performed: given a tile t A having paths of internal transitions between elements of its support, extra vertices are added to the support of t A and tiles having t A in their supports are modified accordingly. Once it has been performed, the converse is done for paths of internal transitions between vertices. Afterwards, for every tile, a mixed closure is applied inside the tile.

First, removal of SCCs may be performed in polynomial time, in the number of vertices. Then, the mixed closure is exponential: for each sequence of silent actions of length n (n is smaller than the number of vertices), (n + 1)n/2 new vertices may be constructed. In the worst case, there is an exponential number of such sequences hence an exponential bound.

Proposition 5. From an RTS R with internal actions Σ τ , one can effectively compute an RTS Clo(R) of exponential size in the number of vertices, such that its semantics Clo(R) has no internal action, is of finite out-degree, and has the same coloured traces as the IOLTS R .

From earlier observations the complete process of performing the closure is performed in exponential time.

Weighted RTSs.

In formal testing, off-line test computations are performed from deterministic models, in order to determine all possible outputs after any trace. However RTSs are not determinizable in general, in fact, Section 5 presents an on-line approach to perform tests on RTSs which one do not wish to determinize. Still there are some RTSs which may be determinized, in particular, weighted RTSs form a decidable class of RTSs which have an effective determinization process.

Definition 11 (Weighted RTS). An RTS R with no internal action and with IOLTS semantics R = (Q, Σ, Λ, → R , C, init) is weighted if C(init) is a singleton {q 0 }, and for any w ∈ Σ * and any pair of states q, q ′ ∈ Q, q 0 w → q and q 0 w → q ′ implies ℓ(q) = ℓ(q ′ ): two states reached by the same sequence have the same level 4 .

Determining whether a given RTS is weighted is decidable (Lemma 4.1 by Caucal and Hassen [START_REF] Caucal | Synchronization of grammars[END_REF]), in polynomial time. The algorithm initially provided in Hassen's thesis [START_REF] Hassen | Synchronisation de grammaires de graphes[END_REF] for HR-grammars can be explained for RTSs as follows. The computation is performed by three successive fixed-points which do not modify the set of tiles (hence the polynomial bound). The first one consists in computing the set of outgoing labels for vertices of the support of tiles (linear computation). The second fixed-point is the computation of sets of pairs of vertices (in a corresponding product of tiles) which are synchronized in the (formal) product RTS. Synchronized means that a given sequence of actions starting from each vertex of the pair reaches vertices of the same depth. This computation is polynomial since there are a quadratic number of pairs, each one is connected to a set of at most a quadratic number of it. The last fixed-point is defining the set of synchronized vertices (in the original RTS), building from the previous step, thus producing a smaller set. Whenever the last set witnesses a vertex which belongs to the support of a tile synchronized with a vertex that does not, the RTS is not weighted. Hence a globally polynomial decision process.

Determinization of RTSs.

An RTS R is said deterministic if its underlying IOLTS R is deterministic. This property is decidable from the set of tiles defining it (for example using Proposition 3). However, since PDAs cannot be determinized in general, there is no hope to determinize an arbitrary RTS. Still, there are some classes of determinizable PDAs, like visibly PDAs [START_REF] Alur | Visibly pushdown languages[END_REF], or, more recently, weighted grammars [START_REF] Caucal | Synchronization of regular automata[END_REF]. These grammars define a class of PDAs that can be determinized and which both subsume the visibly PDAs and the height deterministic PDAs [START_REF] Nowotka | Height-deterministic pushdown automata[END_REF].

Proposition 6 ([12]

). Any weighted RTS R (with no internal transition) can be transformed into a deterministic one D(R) with same set of traces and, for any colour, same traces accepted in this colour. This operation implies first to transform the RTS, so that it only has path-tiles, then these tiles are merged with respect to the vertices with positive out-degree. Both these computations may be performed in polynomial time. Eventually the computation is performed inside tiles resulting in an exponential complexity similar to the case of finite state systems.

Example 3. Assuming internal actions are not visible, the RTS defined in Example 1 is slightly modified: assume that vertex 5 is not in the V -frontier anymore, and suppose that there are 3 transitions labelled int between 0 and respectively 1, 3 and 5. The resulting system is weighted. In such a situation, determinization would simply perform a finite IOLTS determinization in the tile t comp . In the general case some tiles need first to be merged.

Synchronous product.

As seen in Section 2.1, the synchronous product of IOLTSs is the operation used to intersect languages. It is also useful for test selection using a test purpose. In general, the model recognizing the intersection of languages of two RTSs is not recursive. Indeed, the intersection of two context-free languages can be obtained by a product of two RTSs, if such a product was recursive the intersection of two context-free languages would be a context-free language (e.g.,

a n b n c k | n, k ∈ N ∩ a n b k c k | n, k ∈ N is not context-free).
However, the product of an RTS with a finite IOLTS is an RTS. More precisely, given any RTS R with IOLTS R , and a finite state IOLTS A, one can compute an RTS denoted by R × A such that R × A = R × A (the × on the right-hand side of the equality is the product for IOLTSs). This RTS is defined as follows; let A = (Q, Σ, Λ, → A , C, init) be a finite IOLTS, and R = ((Σ, Λ), T , t 0 ) be a RTS. The set of tiles T R×A is the sets of products of the tiles of T in synchronous product with A. Formally, for a given tile t B ∈ T , with t B = ((Σ, Λ), Q B , → B , C B , S B , F B ), the product tile, denoted by t B × A, is the following:

t B × A = ((Σ, Λ × Λ), Q B × Q, → B×A , C B×A , S B×A , F B×A )
, with the transitions and colours defined like for products of IOLTSs in Section 2.1, the support is simply: S B × Q, and, for each

(t C , f C ) ∈ F B (f C : S C → Q B )
, there is a (t C×A , f C×A ) with t C×A another tile of the product, and f C×A a function between S C × Q and Q B × Q that associates to any pair (q C , q) the pair: (f C (q C ), q). Any coloured trace of the product may be projected (with respect to colours) on either one of the systems and is a coloured trace of this system.

Effective run execution in RTSs

In order to perform passive testing (testing which does not involve providing input to the implementation), monitoring, diagnosis or on-line testing, one needs to follow an actual execution on a model of the specification. Whenever such a specification is given by an RTS it is not necessary to actually construct recursively the tilings in order to follow symbolically an execution, or to check whether some observed run is a correct execution of the system.

Runs in Deterministic RTSs.

Given a deterministic RTS R = ((Σ, Λ), T , t 0 ), and a word w = µ 0 • • • µ n-1 ∈ Σ * , let v 0 ∈ t 0 be such that v 0 ∈ init. Let T be a set of arbitrary symbols denoting tiles and let π be the bijection mapping tiles of T into symbols of T . The symbolic path labelled by w is the following sequence:

(v 0 , π(t 0 )) µ0 -→ (v 1 , u 1 ) • • • (v i , u i ) µi -→ (v i+1 , u i+1 ) • • • µn-1 ---→ (v n , u n ),
each word u i is a sequence of symbols in T representing tiles traversed in the past, and each v i is a vertex in some tile (the inverse image by π of the last symbol in u i ). It is assumed here that, either in any tile at most one tile of each kind may be tiled, or the set of symbols, T , enables unambiguous identification of the precise traversed tiles (for example having indices to distinguish several occurrences of a tile in the frontier of another). For each i, transition (v i , u i ) µi -→ (v i+1 , u i+1 ) corresponds to one of the three cases (assume v i ∈ t i for tile t i which is the last in u i : t i = π -1 (u i (|u i | -1))) described hereafter. Observe that these three operations correspond respectively to the internal, pop and push operations of pushdown automata:

• (internal) the transition labelled µ i belongs to tile t i , then v i+1 is simply the target of this transition and u i+1 = u i ;

• (pop) the transition labelled µ i reaches the support of t i , then use the frontier of the tile π -1 (u i (|u i | -2)) to identify the state v i+1 corresponding to it. Then u i+1 is formed by the first |u i | -1 symbols of u i ;

• (push) the vertex v i belongs to the frontier (and there is no transition labelled µ i in t i ), then assuming that t i+1 is the tile containing a transition labelled µ i starting at the inverse image of v i in the frontier. First, let state v i+1 be the image of such transition in tile t i+1 , and second, u i+1 = u i π(t i+1 ).

Whenever the RTS is deterministic, there is at most one symbolic path corresponding to a word. The computation of this symbolic path does not require to compute the whole system the actual path traverses.

Runs in Non-deterministic RTSs and Weighted RTSs.

In the case of a non-deterministic RTS, a word w in Σ * may label several symbolic paths from the states labelled init. In fact there may be exponentially many such paths (with respect to the length of w). Furthermore there is no guaranty on the words of T * representing sequences of tiles: these words may evolve completely independently, reaching any length between 0 and the length of w. On the other hand, Weighted RTSs may also produce exponentially many symbolic paths for a given word w in Σ * (this is unavoidable and may also occur for finite state systems). But each symbolic word in T * , reached by w, will have same length, enabling efficient representation and computation of continuations.

Note on Implementation.

In order to efficiently implement runs in systems modelled by RTSs, the system only needs to have access to a single copy of each tile. For each symbolic path, a pair formed by the current vertex and a word of T * must be kept. This data structure may become large but it is much smaller than the actual tile obtained after k tilings when k is large.

Off-line test generation for weighted RTSs

This section and the following consider the generation of test cases from RTSs. The present section focuses on weighted RTSs, which are determinizable, and proposes an off-line test generation algorithm that operates a selection guided by a test purpose (specified by a finite IOLTS). For a finite IOLTS M, off-line test generation guided by an IOLTS test purpose T P consists in a series of operations as follows (see e.g. the work of Jard and Jéron [START_REF] Jard | TGV: theory, principles and algorithms[END_REF]): first the suspension IOLTS ∆(M) is computed, and determinized into an IOLTS deter(M). Next, this IOLTS is completed by directing unspecified outputs into Fail states, and mirroring actions, giving rise to the so called canonical tester Can(M). Then, the product IOLTS Can(M) × T P is computed, allowing to set Pass verdicts to states of the product whose component in T P is accepting. Finally, the analysis of co-reachability from Pass states allows both to set None verdicts, and Inc ones by complementation, and finally to select a test case T C by removing those transitions labelled by outputs ending in Inc and all transitions from Inc. Here, the aim is essentially to mimic this computation process for the case of RTSs. This means that computations are here performed at the RTS level, with consequences on the underlying IOLTS semantics, enabling the proof of properties on generated test cases.

Construction of the canonical tester

Quiescence

As seen in Section 2 quiescence represents the absence of any visible reaction in the specification. Given a specification defined by an RTS R, detecting vertices where quiescence is permitted enables to construct a suspended specification, ∆(R).

For finite state IOLTSs, livelocks come from loops. For infinite state IOLTSs (e.g. defined by RTSs), livelocks may also come from infinite paths of silent actions involving infinitely many states. Such paths are said divergent. The following lemma characterizes the existence of loops or divergent paths in RTSs by the existence of a path between two copies of the same vertex.

Lemma 1. For an RTS R, there exists a loop or a divergent path in R if and only if there exists a vertex v and two states q 1 , q 2 ∈ v with ℓ(q 1 ) ≤ ℓ(q 2 ) such that q 1 w → q 2 for some w ∈ (Σ τ ) + and for all states q on this path, ℓ(q 1 ) ≤ ℓ(q). Proof. (⇒) Let p = q 0 µ1 → q 1 µ2 → q 2 ... be an infinite path in R , with ∀k ∈ N, µ k ∈ Σ τ . If p contains a loop, there exits one state of minimal level in this loop, let q i1 be this state. Now consider an elementary path (i.e. a path with no loop). As each state in this path is only seen once, we build a sequence of states q i k such that ∀i k ≤ j, ℓ(q i k ) ≤ ℓ(q j ). As there are only a finite number of vertices, there is a least one v such that two states of v appear in this path. Let these two states be q 1 and q 2 .

(⇐) Suppose that there exists a vertex v and two states q 1 , q 2 ∈ v such that q 1 w → q 2 for w ∈ (Σ τ ) + , and for all states q on this path, ℓ(q 1 ) ≤ ℓ(q). There are two cases. If ℓ(q 1 ) = ℓ(q 2 ) then q 1 = q 2 , since any path from two distinct occurrences of the same tile at the same level involves vertices of lower level. Hence this path is a loop. Otherwise, ℓ(q 1 ) < ℓ(q 2 ), let p 0 be a path q 1 w → q 2 for w ∈ (Σ τ ) + , such that for all q in this path, ℓ(q 1 ) ≤ ℓ(q). Thus, from the definition of tiling, a similar path, p 1 , may be constructed from q 2 to a state q 3 ∈ v , with, p 1 = q 2 σ ′ → q 3 for σ ′ ∈ (Σ τ ) + , ℓ(q 2 ) < ℓ(q 3 ), and ℓ(q 2 ) ≤ ℓ(q) for all q involved. Iterating this process enables to produce an infinite path of silent actions in R : a divergent path.

The next proposition states that it is effective to build the suspension of an RTS, i.e. , an RTS whose semantics is the suspension (in terms of IOLTS) of the semantics of the original RTS.

Test case selection with a test purpose

The canonical tester has important properties, but one may want to focus on particular behaviours, using a test purpose.

In the present formal framework, a test purpose will be defined by a deterministic IOLTS, using the fact that the product of an RTS and an IOLTS is still an RTS.

Definition 12 (Test purpose). A test purpose is a complete deterministic finite IOLTS T P over Σ oδ , with a particular colour Accept, such that states coloured by Accept have no successors.

As seen in the previous section, the product P between Can(R) and T P is an RTS. On this product, new colours are specified as follows : In order to avoid vertices coloured by Inc where the test purpose cannot be satisfied anymore, transitions labelled by an output (input of R, controllable by the environment) and leading to a vertex coloured by Inc may be pruned, as well as those leaving Inc. Consequently, runs leading to an Inc coloured vertex necessarily end with an input action.

• C P (Fail) = C Can(R) (Fail) × Q T P • C P (
Finally, the test case T C generated from R and T P is the product P, equipped with new colours Fail, Pass, None, Inc and pruned as above.

Example 5. Using the canonical tester (Fig. 4) resulting from Example 1, Figure 5 depicts the test case obtained with the test purpose, T P, accepting the traces in (Σ oδ ) * .?true.?true(Σ oδ ) * .!m1. The IOLTS T P has four states q 1 , q 2 , q 3 and q 4 (the only state coloured Accept), with self-loops for all actions but one in q 1 and q 3 , and transitions labelled respectively by ?true and !m1, from q 1 to q 2 and from q 3 to q 4 . The product between the canonical tester and T P is performed in each tile leading to the two tiles depicted in Figure 5. For a better readability, the only vertices represented are those reachable from (1, q 1 ) (of tile main) furthermore, in each tile, vertices coloured by Fail (resp., Inc) are merged.

(1, q1) main':

F (3, q3) fcomp(2, q3) (2, q1) fcomp(0, q1) (5, q3) ?int !m1 δ δ δ !m1,!m2,!m3,!m4 !m 1 , !m 2 , !m 3 , !m 4 !m2,!m3,!m4,δ !m 1 , !m 2 , !m 3 , !m 4 (0, q1) comp': (0, q2) (0, q3) (6, q3) (2, q3) (3, q2) fcomp(0, q2) (3, q3) fcomp(0, q3) (4, q3) fcomp(2, q3) F Inc ?true ?true ?true ?false !m4 !m3 !m1,!m3,!m4,δ !m 1 , !m 3 , !m 4 , δ !m 1 , !m 2 , !m 4 , δ !m1,!m2,!m3,δ !m2 !m2

Complexity of the computation of the canonical tester

The computation of the canonical tester is the core of formal test generation. In the case of RTSs it follows several steps described in the previous subsection.

There are two exponential steps in the computation of the canonical tester: the determinization which is unavoidable, and the Σ τ -closure (computation of Clo(CS(R))). The latter results from the possibility to have traversing Σ τ -paths, in fact, complete trees of Σ τ -transitions are needed to reach this bound. The following list summerize the complexity of each individual step.

Exhaustiveness

It is now possible to prove that the test suite T S composed of all test cases that can be generated from arbitrary test purposes T P is exhaustive. First one needs to establish the inequality T C∈T S Traces C(Fail) ( T C ) ⊇ MinFTraces( R ).

Let σ ′ = σ.a ∈ MinFTraces( R ) = Traces C(Fail) ( Can(S) ) be a minimal non-conformant trace for R. Thus σ belongs to STraces( R ) and there exists b ∈ Σ !δ such that σ.b ∈ STraces( R ) (if no output continues σ in STraces( R ), a δ does). Now, it remains to define a test purpose T P such that σ.b ⊆ Traces C(Accept) (T P). Let T C be the test case generated from R and T P. By construction of T C from R and T P: both σ.b belongs to Traces( T C ) and σ ′ belongs to Traces C(Fail) ( T C ). The requested inclusion is thus established.

Precision

As a complement to the above properties, precision relates test cases to test purposes. It says that the verdict Pass is returned as soon as possible, once the test purpose is satisfied. This may be formalized as follows:

On-line test generation from RTS

Like every model characterizing context-free languages, RTSs are not determinizable (as seen in Section 3). This issue does not doom the prospect of formal test suites generation. In similar cases, Tretmans [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF] suggests an on-line test generation process. In fact this process amounts to producing test cases without constructing a deterministic canonical tester. Such a technique performed either off-line or on-line is applicable to RTSs. This section introduces this technique, and establishes properties of the generated test cases.

Test case generation

Since the only transformation not guaranteed to succeed in off-line test generation is determinization, the first steps of the algorithm to generate test cases on-line are identical to those generating test cases off-line, namely suspension, output-completion and Σ τ -closure. The process thus starts from the closure of the output-completed specification Clo(CS(R)) defined in Section 4. This time, the canonical tester cannot be built in general by determinization from Clo(CS(R)). However, using Proposition 4, one can build Clo(CS(R)) from R, ensuring the following properties of equations ( 5), ( 6), ( 7) and ( 8

Product and colouring

The next step consists in the computation of the product of Clo(CS(R)) with a test purpose given as a complete and deterministic finite IOLTS T P. Let P = Clo(CS(R)) × T P be this product, one may define the following new colours on P using a co-reachability analysis:

Computing test cases

The last step consists in computing test cases in the form of IOLTSs, by exploration of the semantics of Clo(CS(R)), in a similar way as Tretmans [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF]. These test cases will be modelled as finite trees formed by alternating sequences of choices of inputs for the system and subtrees of possible answers of the system (computed from P), each node of the tree carries a verdict. Formally such a finite tree will be a prefix-closed set of words in (Σ oδ ) * .({Fail, Pass, None, Inc} ∪ {ε}). Given a tree θ, and some symbol a, the tree formed by a followed by tree θ is denoted by a; θ, it is defined by a; θ {au | u ∈ θ}. Furthermore, given two trees θ, θ ′ , the tree formed by the union of those trees is denoted by θ + θ ′ .

A test case T C is a tree built from P by taking as argument a set of states P S of cloCS(R) . Test cases are defined by applying the following algorithm recursively, starting from the initial state C P (init).

On-line test generation algorithm.

Choose non deterministically between one of the following operations. • θ ′ is obtained by recursively applying the algorithm with P S ′ = (P S after a)

Formally, a tree needs to be transformed into a test case IOLTS T C by an appropriate colouring of states ending in Fail, Pass, Inc or None after a suspension trace. It is skipped for readability.

At every step, the algorithm makes a non-deterministic choice: namely to stop or to proceed. This choice might be influenced by several factors, for example, in order to avoid generating tests cases containing neither Fail nor Pass.

P

  ′ ⇐⇒ P ′ = P after a, and init D ∈ Λ D is the colour for the singleton state C D (init D ) = C(init) after ε ∈ 2 Q . One can define other colours in Λ D and, depending on the objective, the colouring C D may be defined according to Λ and C. For example, if f ∈ Λ defines marked states in M, one may define a colour F ∈ Λ D for D(M) such that Traces C(f ) (M) = Traces C D (F ) (D(M )) simply by colouring by F the states s ∈ 2 Q such that C(f ) intersects s, i.e. at least one state in s is marked by f

Figure 2 :

 2 Figure 2: Tiles composing the system R For the frontier, e.g., in the tile t main , 2 f comp (0)means that (t comp , {0 → 2}) belongs to F main , i.e. the vertex 0 of t comp is associated to the vertex 2 of t main .

Figure 3 :

 3 Figure 3: T (t main ) and T 2 (t main ) tiles

main: 1 F 3 1 , !m 2 , !m 3 , !m 4 compFigure 4 :

 1312344 Figure 4: Example of a canonical tester.

  Pass) = C P (Fail) × C T P (Accept) • C P (None) = Coreach(Σ oδ , C P (Pass)) \ C P (Pass) • C P (Inc) = Q P \ (C P (Fail) ∪ C P (Pass) ∪ C P (None)) Note that, by construction, each vertex has a unique colour in {Fail, Pass, None, Inc}. Vertices coloured by Fail or Pass have no successors, and vertices coloured by Inc have only Fail or Inc successors.

Figure 5 :

 5 Figure 5: Example of a test case

1 )

 1 Computation of ∆(R): polynomial time 2) Computation of CS(R): polynomial time 3) Computation of Clo(CS(R)): exponential space 4) Checking whether Clo(CS(R)) is weighted: polynomial time 5) Determinizing Clo(CS(R)): exponential space 6) Synchronous product Can(R) × T P and selection: polynomial time4.3 Properties of generated test casesThis subsection contains proofs of the requested properties of test cases defined in Section 2, relating test case failure to non-conformance, and a new property, precision, that relates test case success (Pass verdict) to the satisfaction of the test purpose.

  Soundness and strictnessAccording to the construction of P = Can(R)×T P, the definition of C P (Fail), and pruning, selection by T P does not add any colouring by Fail with respect to Can(R), thus Traces C(Fail) ( T C ) = Traces( T C )∩Traces C(Fail) ( Can(R) ). The equation Traces C(Fail) ( T C ) = Traces( T C ) ∩ MinFTraces( R ) ⊆ MinFTraces( R ) follows from equation (9) and proves both strictness (equality) and soundness (inclusion).

Definition 13 (

 13 Precision). A test case T C is precise with respect to an IOLTS specification M and a test purpose T P if Traces C(Pass) ( T C ) = Traces C(Accept) (T P) ∩ STraces(M) ∩ Traces( T C ). It is easy to prove that test cases generated from an RTS R and a test purpose T P are precise. By construction, states coloured by Pass are those coloured by Accept in T P and not by Fail in Can(R). Thus Traces C(Pass) ( T C ) = Traces C(Accept) (T P) ∩ STraces( R ), which (since Traces C(Pass) ( T C ) ⊆ Traces( T C )) implies precision.

R ( 5 )

 5 ):Traces C(UnS) ( Clo(CS(R)) ) ⊆ STraces( R ).Σ !δ Traces C(UnS) ( Clo(CS(R)) ) = STraces( R ) (6) Traces( Clo(CS(R)) ) = STraces( R ).Σ !δ R ∪ STraces( R ) (7)andMinFTraces( R ) = Traces C(UnS) ( Clo(CS(R)) ) \ Traces C(UnS) ( Clo(CS(R)) ) (8)

•

  C P (UnS) = C Clo(CS(R)) (UnS) × Q T P • C P (Pass) = C Clo(CS(R)) (UnS) × C T P (Accept) • C P (None) = Coreach(Σ oδ , C P (Pass)) \ C P (Pass) • C P (Inc) = Q P \ (C P (Fail) ∪ C P (Pass) ∪ C P (None))

• X 1 =

 1 1. ( * Terminate the test case *) θ := {None} 2. (* Give a next input to the implementation *) Choose any a ∈ out(P S) such that (P S after a) ∩ (C P (Pass) ∪ C P (None)) = ∅ θ := a; θ ′ where θ ′ is obtained by recursively applying the algorithm with P S ′ = (P S after a) 3. (* Check the next output of the implementation *) {a | P S after a ⊆ C P (UnS)} • X 2 = {a | (P S after a ⊆ (C P (Inc) ∪ C P (UnS))) ∧ (P S after a ∩ C P (Inc) = ∅)} • X 3 = {a | P S after a ∩ C P (Pass) = ∅} • X 4 = {a | (P S after a ∩ C P (Pass) = ∅) ∧ (P S after a ∩ C P (None) = ∅)}

In the examples, for readability reasons, an input a ∈ Σ ? is written ?a, an output x ∈ Σ ! is written !x. Internal actions have no extra symbol.

While the original ioco theory restricts to non-divergent IOLTSs, in this paper, IOLTSs having both loops of internal actions and divergences, i.e. infinite sequences of internal actions traversing an infinite number of states, are considered.

Such a normalization transforms the tiles of an RTS without changing its semantic.

Are generated after the same number of tilings.

Conclusion

This paper presented an account on recursive tile systems, a general model of IOLTSs allowing for recursion. It provided algorithms to produce sound, strict and exhaustive test suites, either off-line or on-line. These algorithms enable to employ test purposes (even, for the on-line case) which are a classical way to drive tests towards key properties. The precision of these tests with respect to test purposes has been established. Moreover precise assessments of the complexities of involved operations have been provided.

This method has a drawback: the classical off-line approach may not be used whenever the RTS is not weighted. This property may be verified in polynomial time, but it would really be comforting to have a syntactical characterization of a class of RTSs being weighted. Identifying such a class would be a natural continuation of this work.

Another interesting perspective would be to incorporate known results on probabilistic RTSs that have been considered by several authors [19,20]. This would enable to take into account quantitative properties of systems, or to express coverage properties of finite test suites.

Proposition 7. From any RTS R, it is effective to build an RTS denoted ∆(R) such that ∆(R) = ∆( R ). Consequently Traces( ∆(R) ) = STraces( R ).

Proof. Let R be a RTS, self-loops labelled by δ are added as follows.

• For output quiescence (deadlock or absence of output), Requirement 1, item 2 (defined after Definition 9), ensures that Γ R ( v ), for a vertex v in a tile t of R, has a uniform value. The δ-transitions can thus be added to each v in R such that Γ R ( v ) ⊆ Σ ? R . This operation produces a new RTS R ′ . • For livelocks, the two different cases of internal loops and divergent paths are tackled by Lemma 1. Such situations may be detected from self-reaching vertices. This result also ensures that this detection may be performed by considering each tile as an axiom. Then, for each tile t in R ′ , the following is performed:

-Proposition 2 is used to colour by λ ′ v vertices in r each Rt (Σ τ , λ), where R ′ t is the RTS identical to R ′ , with initial tile t. This computation simply enables to detect vertices involved in an infinite path, but the resulting RTS is not kept.

-Each vertex v coloured by both λ v and λ ′ v is involved in a livelock. Quiescence is added to each such vertex in R ′ to produce ∆(R).

It is not hard to see that this construction mimics the suspension of IOLTSs on RTSs, thus ensuring that Traces( ∆(R) ) = STraces( R ).

Output completion

After using Proposition 7 for the computation of ∆(R) from the specification R, the next step is to complete ∆(R) into an RTS denoted CS(R) which recognize STraces(R).Σ !δ in a fresh color.

The complete suspended specification, denoted by CS(R), is computed from ∆(R) as follows: a fresh colour UnS is added to detect paths ending with unspecified outputs. Then, for every tile t A , a new vertex v UnS A is added (having colour UnS), and new transitions leading to v UnS A are added as well for unspecified outputs:

By construction, the following is true:

The inequality (1) simply says that the traces of sequences recognized in UnS are suspension traces of R prolonged with outputs. The equality (2) holds because Traces C(UnS) ( CS(R) ), which are traces of sequences leading outside the colour UnS, are the original suspension traces of ∆(R), thus STraces( R ). The equality (3) is obtained by union of ( 1) and [START_REF] Jard | TGV: theory, principles and algorithms[END_REF]. Notice however that it is not a disjoint union: a trace can be in both Traces C(UnS) ( CS(R) ) and Traces C(UnS) ( CS(R) ), as it can be the projection of both a sequence in ∆(S) and a sequence leading to UnS.

Expanding the definition of MinFTraces( R ), produces

Remark 3. Notice that the introduction of the section describes a test generation process from finite IOLTSs, where a canonical tester is built by output completion to Fail after determinization. A similar process could be described for weighted RTSs. However, here, the process consists first in performing an output completion (with a slightly different meaning to a colour UnS), and then in determinizing (next paragraph) while defining Fail. The reason is that output completion can be computed for any RTS, and will be used for both off-line and on-line test generation, while determinization is not, and will be used only for off-line test generation for weighted RTSs.

Using Proposition 4, from CS(R) one can build an RTS Clo(CS(R)), which semantics Clo(CS(R)) has no internal action and has same coloured traces as CS(R) . It immediately follows that Clo(CS(R)) ensures the same inequalities and equalities as (1), ( 2) and (3):

Moreover, the equality (4) immediately transposes to Clo(CS(R)):

Canonical tester

Whenever Clo(CS(R)) is weighted, Proposition 6 enables to determinize it into D(Clo(CS(R))). From D(Clo(CS(R))) a new RTS Can(R) called the canonical tester of R is built as follows:

• a new colour Fail is considered and vertices of D(Clo(CS(R))) are coloured by Fail if composed of vertices all coloured by UnS in Clo(CS(R)), thus recognizing traces of sequences all leading to UnS.

• inputs and outputs are mirrored in Can(R) wrt. R.

From this construction and equality (8) follows:

and

where the union is now a disjoint union. In fact

and

From equality (9) it immediately follows that the test suite T S reduced to the canonical tester, T S = {Can(R)}, is sound and exhaustive (see Section 2). T S is also strict, which is proved as follows:

using the fact that ( 11) is a disjoint union, and the equality [START_REF] Courcelle | Handbook of Theoretical Computer Science, chap. Graph rewriting: an algebraic and logic approach[END_REF].

Example 4. Figure 4 represents the canonical tester obtained from Example 1. Observe that it has been suspended, and that internal actions, {try, throw, catch, intern}, have been abstracted away. The vertices labelled by F correspond to the ones coloured by Fail. These vertices are those reached by unspecified output actions.

Properties of the test cases generated on-line

One of the main benefits of the formal generation of test cases from a specification is that properties of these test suites may be proved. This is still the case for on-line test suites. Even though these proofs are largely similar to those of the off-line case, we present precise correlations in this section.

Soundness and Strictness

By definition of the set X 1 , the traces of T C falling in a state coloured by Fail are those in Traces( Clo(CS(R))

which proves both soundness and strictness, as in the off-line case.

Exhaustiveness

The proof of exhaustiveness is similar to the one in Section 4, consisting in building a test purpose T P for each non-conformant trace, and proving that a possible resulting test case would produce a Fail after this trace.

Precision

From the construction of T C, in particular, the set X 3 , we have Traces

Application of on-line test cases generation

Previous subsections have shown how to generate on-line test cases without computing a deterministic canonical tester. In fact, using the method proposed in Section 3.4, it is possible to perform such computation without constructing the whole tile modeling the system. From the algorithm presented in subsection 5.1.2, we compute a set of compatible symbolic paths: each of these paths is stored as a pair formed by a vertex and a word of tile symbols (in T * ).

The following example illustrates how to apply the previous construction to the RTS of Example 1 (it is deterministic but is convenient for the purpose of illustration). Example 6. Let T be the set {m, c} where the symbols represent respectively tiles main and comp. Assume 8, true, true, true is the sequence of input already computed. One may check that the following pair is reached: (1, mccc). Hence if the implementation outputs something, the test will fail. Otherwise if, for example, the random choice of the tester selects to output f alse, (6, mcccc) is reached, then the output "You stopped" (message m4) is expected, leading to the configuration (2, mcccc). Then the tester only expects the message "Some text" (message m3), each time removing one c. Eventually, state (5, m) will be reached after receiving "Done" (message m1) from the implementation. This would be the end of this test.