K Meinke

F Niu
email: niu@csc.kth.se

Learning-Based Testing for Reactive Systems using Term Rewriting Technology

We show how the paradigm of learning-based testing (LBT) can be applied to automate specification-based black-box testing of reactive systems using term rewriting technology. A general model for a reactive system can be given by an extended Mealy automata (EMA) over an abstract data type (ADT). A finite state EMA over an ADT can be efficiently learned in polynomial time using the CGE regular inference algorithm, which builds a compact representation as a complete term rewriting system. We show how this rewriting system can be used to model check the learned automaton against a temporal logic specification by means of narrowing. Combining CGE learning with a narrowing model checker we obtain a new and general architecture for learningbased testing of reactive systems. We compare the performance of this LBT architecture against random testing using a case study.

Introduction

Learning-based testing (LBT) is an emerging technology for specification-based black-box testing that encompasses the three essential steps of : (1) test case generation (TCG), [START_REF] Chauhan | Automated abstraction refinement for model checking large state spaces using sat based conflict analysis[END_REF] test execution, and (3) test verdict (the oracle step). It has been successfully applied to testing procedural systems in [START_REF] Meinke | Automated black-box testing of functional correctness using function approximation[END_REF] and [START_REF] Meinke | A learning-based approach to unit testing of numerical software[END_REF], and reactive systems in [START_REF] Meinke | Incremental learning-based testing for reactive systems[END_REF]. The basic idea of LBT is to automatically generate a large number of high-quality test cases by combining a model checking algorithm with an incremental model inference algorithm, and integrating these two with the system under test (SUT) in an iterative loop. The use of incremental learning is critical in making this technology both fast and scalable to large systems under test (SUTs). Our previous research ( [START_REF] Meinke | A learning-based approach to unit testing of numerical software[END_REF] and [START_REF] Meinke | Incremental learning-based testing for reactive systems[END_REF]) has repeatedly shown that LBT has the capability to significantly outperform random testing in the speed with which it finds errors in an SUT.

For testing complex embedded software systems, there is a significant need to generate test cases over infinite data types such as integer and floating point types, and abstract data types (ADTs) such as strings, arrays, lists and various symbolic data types. Specification-based TCG is essentially a constraint solving problem. So this generalisation from finite to infinite and symbolic data types is highly non-trivial since the satisfiability problem for many logics over abstract and infinite data types is undecidable. Thus a search for test cases is not guaranteed to terminate.

Model checking over abstract and infinite data types is therefore a state of the art problem. Recently some success has been achieved with the use of satisfiability modulo theories (SMT) solvers such as Z3 [START_REF] De Moura | An efficient smt solver[END_REF], which are based on heuristic techniques. However, an alternative approach is to use constraint solving based on a narrowing algorithm. Narrowing is a flexible technology, based on term rewriting, which is applicable to any data type for which we can find a complete (confluent and terminating) term rewriting system (see e.g. [START_REF] Baader | Unification theory[END_REF]). It has well understood theoretical properties such as completeness of solutions and conditions for termination. Narrowing has been successfully applied to model checking of infinite state systems in [START_REF] Escobar | Symbolic model checking of infinite-state systems using narrowing[END_REF]. However, the use of narrowing for test case generation has not yet been considered. In fact, our aim in this paper is much wider. We will show that narrowing combines easily with symbolic learning algorithms for automata such as CGE [START_REF] Meinke | Cge: A sequential learning algorithm for mealy automata[END_REF] to yield a new LBT architecture for specification-based testing of reactive systems computing over abstract data types. Initial case studies suggest that despite the significant increase in the problem complexity, this new LBT architecture is also competitive with random testing.

The structure of this paper is as follows. In the remainder of Section 1 we review related work. In Section 2, we recall some essential mathematical preliminaries needed to discuss narrowing. In Section 3, we formalise a general model of a reactive system as an extended Mealy automaton (EMA) over an abstract data type (ADT). We introduce a linear time temporal logic (LTL) for such EMA, and we show how an LTL formula can be translated into constraint sets consisting of equations and negated equations. In Section 4, we present a model checking algorithm based on narrowing applied to a constraint set. In Section 5, we combine this model checking method with a symbolic automata learning algorithm (the CGE learning algorithm of [START_REF] Meinke | Cge: A sequential learning algorithm for mealy automata[END_REF]) to define a new LBT architecture for specification-based testing of reactive systems. In Section 6, we present a case study of this LBT architecture applied to testing the TCP protocol. Finally, in Section 7 we draw some conclusions and discuss open questions to be addressed by future work.

Related Work

In [START_REF] Meinke | Incremental learning-based testing for reactive systems[END_REF], LBT was applied to testing reactive systems modeled as Boolean Kripke structures. Our work here extends this previous work to allow symbolic and infinite data types. Even for finite data types, this approach simplifies the expression of control and data properties of an SUT. For this extension we use a more powerful symbolic learning algorithm, new model checking technology based on term rewriting theory, and a more powerful oracle construction for test verdicts.

Several previous studies, (for example [START_REF] Peled | Black-box checking[END_REF], [START_REF] Groce | Adaptive model checking[END_REF] and [START_REF] Raffelt | Dynamic testing via automata learning[END_REF]) have considered a combination of learning and model checking to achieve testing and/or formal verification of reactive systems. Within the model checking community the verification approach known as counterexample guided abstraction refinement (CE-GAR) also combines learning and model checking, (see e.g. [START_REF] Clarke | Sat-based abstraction refinement using ilp and machine learning[END_REF] and [START_REF] Chauhan | Automated abstraction refinement for model checking large state spaces using sat based conflict analysis[END_REF]). The LBT approach described here can be distinguished from these other approaches by: (i) an emphasis on testing rather than verification, (ii) the focus on incremental learning for efficient scalable testing, (iii) the use of narrowing as a model checking technique, and (iv) the introduction of abstract data types.

There is of course an extensive literature on the use of model checkers (without learning) to generate test cases for reactive systems. A recent survey is [START_REF] Fraser | Testing with model checkers: A survey[END_REF]. Generally this work emphasizes glass-box testing (so no learning is necessary), and the use of structural coverage measures to constrain the search space for test cases. Furthermore, behavioral requirements may or may not be present. By contrast, the LBT approach concerns black-box testing. Furthermore, in LBT behavioral requirements are always present, both to solve the oracle problem and to constrain the search space and guide the search for effective test cases.

In [START_REF] Walkinshaw | Increasing functional coverage by inductive testing: a case study[END_REF], black-box reactive system testing using learning but without model checking is considered. This is also shown to be more effective than random testing. Thus we can conclude that learning and model checking are two mutually independent techniques that can be applied to systems testing separately or together. In the long term we hope to show that the combination of both techniques is ultimately more powerful than using either one alone.

Mathematical Preliminaries and Notation

It is helpful to have some familiarity with the theories of abstract data types and term rewriting. Both use the notation and terminology of many-sorted algebra (see e.g. [START_REF] Meinke | Universal algebra[END_REF]). Let S be a finite set of sorts or types. An S-sorted signature Σ consists of an S * × S-indexed family of sets Σ = Σ w,s | w ∈ S * , s ∈ S . For the empty string ε ∈ S * , c ∈ Σ ε,s is a constant symbol of sort s. For w = s 1 , . . . , s n ∈ S + , f ∈ Σ w,s is a function symbol of arity n, domain type w and codomain type s. An S-sorted Σ-algebra A consists of sets, constants and functions that interpret Σ by a particular semantics. Thus A has an S-indexed family of sets A = A s | s ∈ S , where A s is termed the carrier set of sort s. For each s ∈ S and constant symbol c ∈ Σ ε,s , c A ∈ A s is a constant, and for each w = s 1 , . . . , s n ∈ S + and each f ∈ Σ w,s , f A : A s1 × . . . × A sn → A s is a function. Let X = X s | s ∈ S be an S-indexed family of disjoint sets X s of variables of sort s. We assume X s ∩ Σ ε,s = ∅. The set T (Σ, X) s of all terms of sort s ∈ S is defined inductively by: (i) c ∈ T (Σ, X) s for c ∈ Σ ε,s , (ii) x ∈ T (Σ, X) s for x ∈ X s , and (iii) f (t 1 , . . . , t n ) ∈ T (Σ, X) s for f ∈ Σ w,s w = s 1 , . . . , s n and t i ∈ T (Σ, X) si for 1 ≤ i ≤ n. We use ≡ to denote syntactic equality between terms. An equation e (respectively negated equation) over Σ and X is a formula of the form (t = t ) (respectively ¬(t = t )) for t, t ∈ T (Σ, X) s . We let Vars(t) (respectively Vars(e), Vars(¬(e))) denote the set of all variables from X occurring in t (respectively e, ¬e).

A variable assignment α : X → A is an S-indexed family of mappings α s : X s → A s . A substitution σ is a variable assignment σ : X → T (Σ, X) such that σ s (x) = x for just finitely many s ∈ S and variables x ∈ X s , and this set of variables is the domain of σ s . The result of applying a substitution σ to a term t ∈ T (Σ, X) s is defined inductively in the usual way and denoted by σ(t). If σ and σ are substitutions then their composition σ • σ is defined by σ • σ (x) = σ(σ (x)). A variable renaming is a family of bijective substitutions σ s : X s → X s . A substitution σ is more general than a substitution τ , denoted σ ≤ τ if there exists a substitution δ such that δ

• σ = τ . A disunification problem S = { (t i Q i t i ) | i = 1, . . . , n, n ≥ 0, Q i ∈ { = , = } }
is a finite (possibly empty) set of equations and negated equations over Σ and X. A substitution σ :

X → T (Σ, X) is a syntactic unifier of a set S if for all 1 ≤ i ≤ n, if Q i is = then σ(t i ) ≡ σ(t i ), and if Q i is = then σ(t i ) ≡ σ(t i ).
We let U (S) denote the set of all syntactic unifiers of S. A unifier σ ∈ U (S) is a most general unifier (mgu) if σ ≤ τ for all τ ∈ U (S).

If t ∈ T (Σ, X) s is a term then O(t) denotes the set of all positions in t, i.e. all nodes in the parse tree of t and is inductively defined by

O(c) = O(x) = { ε } and O(f (t 1 , . . . , t n )) = { ε, k.i | 1 ≤ k ≤ n, i ∈ O(t k ) }.
We write t| p for the subterm of t found at position p ∈ O(t), and if t| p , u ∈ T (Σ, X) s then t[u] p denotes the term obtained by replacing the subterm found at p in t by u. We say that p ∈ O(t) is a non-variable position if t| p is not a variable, and let O(t) denote the set of all such non-variable positions.

A term rewriting rule is an expression of the form l → r for l, r ∈ T (Σ, X) s and s ∈ S such that Vars(r) ⊆ Vars(l) and a term rewriting system (TRS) R is a set of rewriting rules. If σ s : X s → X s is a family of variable renamings then σ(l) → σ(r) is a variant of l → r.

Mealy Automata over Abstract Data Types

In this section we formalise a general model of a reactive system as an extended Mealy automaton (EMA) over an abstract data type. We then introduce the syntax and semantics of a linear time temporal logic (LTL) as a language for expressing user requirements on EMA. Finally, we define a syntactic translation of LTL into equations and negated equations, and establish the soundness and completeness of this translation with respect to satisfiability.

We can model a Mealy automaton over an abstract data type as a manysorted algebraic structure by considering inputs, states and outputs as distinguished data sorts (or types). The input and output types will be typically chosen from some well known data types such as int, string, array, list etc. that provide a high level of data abstraction. Definition 1. A signature (S, Σ, input, output) for an extended Mealy automaton is a four-tuple, where S = { state, s 1 , . . . , s n } is a sort set, Σ is an S-sorted signature with distinguished constant and function symbols

q 0 ∈ Σ ε,state , δ ∈ Σ state input,state , λ ∈ Σ state input,output ,
and input, output ∈ { s 1 , . . . , s n } are distinguished input and output types. Definition 2. Let (S, Σ, input, output) be a signature for an EMA. An extended Mealy automaton A (of signature Σ) is an S-sorted Σ algebra A.

As usual q 0

A is the initial state, δ A : A state × A input → A state is the state transition function, and λ A :

A state × A input → A output is the output function.
We define the extended state transition and output functions

δ * A : A state × A * input → A state , λ * A : A state × A + input → A output in the usual way for any q ∈ A state , i ∈ A input and j ∈ A input by δ * A (q, ε) = q and δ * A (q, i . j) = δ A ( δ * A (q, i), j), also λ * A (q, i . j) = λ A ( δ * A (q, i), j). If A state is finite then A is termed a finite state EMA , otherwise A is termed an infinite state EMA.
Next we introduce a linear time temporal logic (LTL) that can be used to express user requirements on EMA. For this it is necessary to integrate the underlying data type signature Σ in an appropriate way. In the sequel we assume that (S, Σ, input, output) is a given EMA signature. Let X = X s | s ∈ S -{ state } be any indexed family of sets X s of variable symbols of sort s. We assume that in ∈ X input and out ∈ X output are two distinguished variable symbols. Definition 3. The set LTL(Σ, X) of all linear temporal logic formulas over Σ and X is defined to be the smallest set of formulas containing the atomic proposition true and all equations (t = t ) for each sort s ∈ S -{ state } and all terms t, t ∈ T (Σ, X) s , which is closed under negation ¬, conjunction ∧ , disjunction ∨ , and the next X, always future G, sometime future F, always past G -1 , and sometime past F -1 temporal operators As usual, X(φ) denotes that φ is true in the next time instant, while G(φ) (respectively F(φ)) denotes that φ is always (respectively at some time) true in the future of a run. On the other hand G -1 (φ) (respectively F -1 (φ)) denotes that φ was always (respectively at some time) true in the past of a run. While not strictly necessary, including these past operators makes this LTL exponentially more succinct, as shown in [START_REF] Markey | Temporal logic with past is exponentially more succinct[END_REF]. This increases the efficiency of our narrowing model checker. We let ( φ =⇒ ψ ) denote the formula ( ¬φ ∨ ψ ), and t = t denotes ¬(t = t ). Then for example, the formula

G( (in = x) ∧ X( (in = y) =⇒ X(out = x + y) ) )
is an LTL formula that expresses that at all times, if the current input is x and next input is y then in two time steps from now the output will be the sum x + y. So in this LTL we can express both control and data properties of reactive systems. Definition 4. Let A be an EMA, let n ∈ N, let i = i 0 , i 1 , . . . ∈ A ω input be an infinite sequence of inputs for A, and let Val A,α : T (Σ, X) s → A s be the valuation mapping on terms given a variable assignment α : X → A. We define the satisfaction relation A, n, i, α |= φ for each formula φ ∈ LTL(Σ, X) by induction. A formula φ ∈ LTL(Σ, X) is satisfiable with respect to A if there exists an infinite sequence i ∈ A ω input and an assignment α : X → A such that A, 0, i, α |= φ.

(i) A, n, i, α |= true. (ii) A, n, i, α |= t = t if, and only if, Val A,β (t) = Val A,β (t ), where β = α[ in → i n , out → λ A (δ * A (q 0 A , i 0 , . . . , i n-1 ), i n )) ]. (iii) A, n, i, α |= ¬φ ⇔ A, n, i, α |= φ. (iv) A, n, i, α |= φ ∧ ψ if,
As is well known, for every formula φ ∈ LTL(Σ, X) there exists a logically equivalent formula φ ∈ LTL(Σ, X) in negation normal form (NNF) where negations only occur in front of atomic subformulas. To solve LTL formulas by narrowing we translate an NNF formula φ into a finite set S = { S 1 , . . . , S n } of constraint sets, where a constraint set S i consists of equations and negated equations. This translation requires an additional set X = { x i | x i ∈ X input } of fresh variable symbols ranging over input sequence elements. Definition 5. Let A be an EMA, and let loopbound be the length of the longest loop-free path in A. For each NNF formula φ ∈ LTL(Σ, X) we define the satisfiability set SatSet n (φ) as a finite collection of constraint sets by structural induction on φ.

SatSet n (t Q t ) = { { (θ n (t) Q θ n (t )) } }
where Q ∈ { =, = } and θ n is the substitution defined by

θ n = { in → x n , out → λ(δ * (q 0 , x 0 , . . . , x n-1 ), x n ) } SatSet n ( φ ∧ ψ ) = { S φ ∪ S ψ | S φ ∈ SatSet n (φ), S ψ ∈ SatSet n (φ) } SatSet n ( φ ∨ ψ ) = SatSet n (φ) ∪ SatSet n (¬φ ∧ ψ) SatSet n ( X(φ) ) = SatSet n+1 (φ) SatSet n ( F(φ) ) = loopbound k=0 SatSet n+k (φ) SatSet n ( F -1 (φ) ) = loopbound k=0 SatSet n-k (φ) SatSet n ( G(φ) ) = loopbound h=0 loopbound l=1 { { x n+h+k.l+i = x n+h+i | 1 ≤ k, 0 ≤ i ≤ l -1 } ∪{ δ * (q 0 , x 0 , . . . , x n+h+l-1 ) = δ * (q 0 , x 0 , . . . , x n+h-1 ) } ∪ h+l-1 i=0 S i | S i ∈ SatSet n+i (φ), 0 ≤ i ≤ h + l -1 } SatSet n ( G -1 (φ) ) = { n i=0 S i | S i ∈ SatSet i (φ) for 0 ≤ i ≤ n }
The translation SatSet n (φ) preserves solutions of φ as follows.

Theorem 1. Let A be an EMA, and loopbound be the length of the longest loop-free path in A. Let φ ∈ LTL(Σ, X) be in NNF, and let n ∈ N.

(i) (Soundness of Translation) For any assignment α : X → A and input se-

quence i = i 0 , i 1 , . . . ∈ A ω input there exists S ∈ SatSet n (φ) such that A, n, i, α |= φ =⇒ A, β(i), α |= S,
where the assignment β(i) :

X → A input is given by β(i)(x n ) = i n .
(ii) (Completeness of Translation) For any assignments α : X → A and β :

X → A input if there exists S ∈ SatSet n (φ) such that A, β, α |= S then there exists an input sequence β ∈ A ω input such that A, n, β, α |= φ.
Thus by Theorem 1, to solve an NNF formula φ it is necessary and sufficient to solve one of the constraint sets S 1 , . . . , S n ∈ SatSet 0 (φ). We will consider a method to solve constraint sets by narrowing in the next section.

The problem of finding solutions to a set { t 1 = t 1 , . . . , t n = t n } of equations is the well known unification problem about which much has been written (see e.g. [START_REF] Baader | Unification theory[END_REF]). More generally, in the case that a set { t 1 = t 1 , . . . , t n = t n , u 1 = u 1 , . . . , u n = u n } of equations and negated equations must be solved, this problem is known as the disunification problem (see e.g. [START_REF] Comon | Disunification: a survey[END_REF]).

Let Σ be a many-sorted data type signature and E be an equational data type specification having a complete rewrite system R. Then the disunification problem is complicated by the fact that we seek solutions modulo R (and hence E) in the following sense. Definition 6. Let R be a term rewriting system. The relation of R-conversion denote by = R is the reflexive symmetric and transitive closure of

R -→ . Let S = { (t i Q i t i ) | i = 1, . . . , n, n ≥ 0, Q i ∈ { =, = } } be a disunification problem. A substitution σ : X → T (Σ, X) is an R-unifier of S if for all 1 ≤ i ≤ n, if Q i is = then σ(t i ) = R σ(t i ), and if Q i is = then σ(t i ) = R σ(t i ). We let U R (S) denote the set of all R-unifiers of S.
In the special case where E = R = ∅, these problems are known as syntactic unification and syntactic disunification, and both problems are decidable. However in many important cases, both the unification and disunification problems are undecidable. Nevertheless, these problems are semidecidable and one can consider complete search algorithms which always terminate when a solution is to be found. The method of narrowing gives such a complete search algorithm, and can be used whenever the data type specification E can be represented by a complete term rewriting system R.

The basic idea of narrowing is a systematic search of the space of possible solutions using the rules of R. If some equation t i = t i cannot be syntactically unified then we can apply a substitution σ : X → T (Σ, X) to t i (or t i ) such that the resulting term σ(t i ) is not in R normal form and then reduce this in one step. This requires unifying t i (or t i ) with the left hand side l of a rule l → r in R, and replacing with a suitable instance of r so that a new equation is obtained. A similar process can be applied to negated equations, and can be iterated for all formulas until syntactic unification of the entire set becomes possible, though the narrowing process may not terminate. If it terminates, the resulting sequence of substitutions σ k : X → T (Σ, X) can be composed together with the final syntactic unifier θ to yield an R-unifier. Definition 7. We say that a term t is R-narrowable into a term t if there exists a non-variable position p ∈ O(t), a variant l → r of a rewrite rule in R and a substitution σ such that:

(i) σ is a most general syntactic unifier of t| p and l, and (ii) t ≡ σ(t[r] p ). We write t [p,l→r,σ] t or simply t σ t . The relation is called R-narrowing.

The R-narrowing relation on terms can be extended to equations and negated equations in an obvious way. A formula

(t Q t ) (where Q is = or =) is R- narrowable into a formula (u Q u )
if there exists a variant l → r of a rewrite rule in R and a substitution σ such that either t [p,l→r,σ] u for some non-variable occurrence p ∈ O(t) or t [q,l→r,σ] u for some non-variable occurrence q ∈ O(t ).

We write

(t Q t ) [p,l→r,σ] (u Q u ) or simply (t Q t ) σ (u Q u ).
Generalising the R-narrowing relation still further to sets of equations and negated equations we will write S [p,l→r,σ] S or S σ S . We can relativise the concept of a substitution σ being more general than a substitution τ (c.f. Section 2) to R as follows. Let V be any S-indexed family of sets V s of variables. We define σ ≤ R τ [V ] if for some substitution δ, δ • σ(x) = R τ (x) for all s ∈ S and x ∈ V s . Now we can discuss the soundness and completeness of narrowing.

Theorem 2. Let S = { (t i Q i t i ) | i = 1, . . . , n, n ≥ 0, Q i ∈ { =, = } } be a disunification problem.
(i) (Soundness of Narrowing) Let S σ1 S 1 σ2 , . . . , σn S n be a terminated R-narrowing derivation such that S n is syntactically unifiable by a substitution θ.

Then θ • σ n • . . . • σ 1 is an R-unifier of S.
(ii) (Completeness of Narrowing) If S is R-unifiable then let ρ be any Runifier and V be a finite set of variables containing Vars(S). There exists a terminated R-narrowing derivation S σ1 S 1 σ2 , . . . , σn S n such that S n is syntactically unifiable. Let µ be a most general syntactic unifier of S n then µ

• σ n • . . . • σ 1 ≤ ρ[V ].
The search space of narrowing is large and narrowing procedures frequently fail to terminate. Many proposals have been made to increase the efficiency of narrowing. One important restriction on the set of occurrences available for narrowing, termed basic narrowing, was introduced in [START_REF] Hullot | Canonical forms and unification[END_REF], and has since been widely studied, e.g. [START_REF] Middeldorp | Completeness results for basic narrowing[END_REF].

A basic narrowing derivation is very similar to a narrowing derivation as given in Definition 7 above. However, in a basic narrowing derivation, narrowing is never applied to a subterm introduced by a previous narrowing substitution. This condition is quite complex to define precisely, and the reader is referred to [START_REF] Hullot | Canonical forms and unification[END_REF].

Theorem 4 of [START_REF] Hullot | Canonical forms and unification[END_REF] can be used to show that basic narrowing for equations and negated equations is also sound and complete in the sense of Theorem 2. However, for basic narrowing [START_REF] Hullot | Canonical forms and unification[END_REF] also establishes sufficient conditions to guarantee termination. This property is important in test case generation, where we need to know if a test case exists at all. Theorem 3. ( [START_REF] Hullot | Canonical forms and unification[END_REF]) Let R = { l i → r i | i = 1, . . . , n } be a complete rewrite system such that any basic R-narrowing derivation from any of the r i 's terminates. Then every R-narrowing derivation terminates.

Many examples of TRS satisfying Theorem 3 are known, including TRS for all finite ADTs. This general termination result can be applied to establish that basic R-narrowing yields a decision procedure for LTL model checking (i.e. basic R-narrowing is sound, complete and terminating) because of the following new result about the CGE symbolic learning algorithm. Proof. Proposition 4.5 of [START_REF] Meinke | Cge: A sequential learning algorithm for mealy automata[END_REF] establishes that R n is complete. To establish termination, consider that every rule l → r ∈ R n is ground by Definitions 3.12 and 4.4 of [START_REF] Meinke | Cge: A sequential learning algorithm for mealy automata[END_REF]. Hence the result is a special instance of Theorem 3 above and Example 3 in [START_REF] Hullot | Canonical forms and unification[END_REF].

We have constructed an implementation of model checking by basic narrowing. We explain how this is integrated into learning-based testing in Section 5.

An LBT Architecture for Testing Reactive Systems

Learning-based testing (LBT) is a general paradigm for black-box specificationbased testing that requires three basic components:

(1) a (black-box) system under test (SUT) S,

(2) a formal requirements specification Req for S, and

(3) a learned model M of S.

Given such components, the paradigm provides a heuristic iterative method to search for and automatically generate a sequence of test cases. The basic idea is to incrementally learn an approximating sequence of models M i for i = 1, 2, . . . of the unknown SUT S by using test cases as queries. During this learning process, we model check each approximation M i on-the-fly searching for counterexamples to the validity of Req. Any such counterexample can be confirmed as a true negative by taking it as the next test case. At step i, if model checking does not produce any counterexamples then to proceed with the iteration, the next test case is constructed by another method, e.g. randomly.

In [START_REF] Meinke | Incremental learning-based testing for reactive systems[END_REF], LBT was applied to testing reactive systems modeled as Boolean Kripke structures. In this paper we consider the case where the SUT S is a reactive system that can be modeled by an EMA over the appropriate abstract data types, and Req is an LTL formula over the same data types. Thus we extend the scope of our previous work to deal with both control and data by applying new learning algorithms and model checking technology.

For LBT to be effective at finding errors quickly, it is important to use an incremental learning algorithm. In [START_REF] Meinke | Incremental learning-based testing for reactive systems[END_REF] this was empirically demonstrated by using the IKL incremental learning algorithm for Boolean Kripke structures. However, learning algorithms for finite data types such as IKL do not extend to infinite data types. The CGE learning algorithm of [START_REF] Meinke | Cge: A sequential learning algorithm for mealy automata[END_REF] was designed to implement learning EMA over abstract data types. Furthermore, this algorithm is incremental since its output is a sequence of representations R 1 , R 2 , . . . of the hypothesis EMA M 1 , M 2 , . . . which are the approximations to S. Each representation R i is a complete TRS that encodes M i as the corresponding quotient of the prefix tree automaton. Details of this representation can be found in [START_REF] Meinke | Cge: A sequential learning algorithm for mealy automata[END_REF]. Furthermore, CGE has many technical advantages over IKL. For example, the number of queries (test cases) between construction of successive approximations R k and R k+1 can be arbitrarily small and even just one query. By contrast, IKL and other table based learning algorithms usually have intervals of tens or hundreds of thousands of queries between successive approximations of large SUTs. As a consequence, model checking can only be infrequently applied.

The input to CGE is a series of pairs (i 1 , o 1 ), (i 2 , o 2 ), . . . consisting of a query string i k for S and the corresponding output string o k from S. In an LBT setting, the query strings i k come from model checker counterexamples and random queries. Finite convergence of the sequence R 1 , R 2 , . . . to some TRS R n can be guaranteed if S is a finite state EMA (see [START_REF] Meinke | Cge: A sequential learning algorithm for mealy automata[END_REF]) and the final hypothesis automaton M n is behaviorally equivalent with S. So with an increasing number of queries, it becomes more likely that model checking will produce a true negative if one exists, as the unknown part of S decreases to nothing. By combining CGE with the narrowing model checker of Section 4, we arrive at a new LBT architecture for reactive systems shown in Figure 1.

Figure 1 illustrates the basic iterative loop of the LBT architecture between: (i) learning, (ii) model checking, (iii) test execution, and (iv) test verdict by an oracle. This iterative loop is terminated by an equivalence checker. This component can be used to detect that testing is complete when the SUT is sufficiently small to be completely learned. Obviously testing must be complete by the time we have learned the entire SUT, since model checking by narrowing is solution complete. The equivalence checker compares the current model representation R k with S for behavioural (rather than structural) equivalence. A positive result from this equivalence test stops all further learning, after one final model check of R k searches for any residual errors. In practical applications of LBT technology, real world SUTs are usually too large to be completely learned. It is this pragmatic constraint that makes incremental learning algorithms necessary for scalable LBT. In such cases the iterative loop must ultimately be terminated by some other method such as a time constraint or a coverage measure.

Figure 1 shows that the current model R k is also passed from the CGE algorithm to the basic narrowing model checker, together with a user requirement represented as an LTL formula φ. This formula is fixed for a particular testing session. The model checker uses R k to identify at least one counterexample to φ as an input sequence i k+1 over the underlying input data type. If φ is a safety formula then this input sequence will usually be finite

i k+1 = ( i 1 , . . . , i j ) ∈ T (Σ) * input .
If φ is a liveness formula then the input sequence i k+1 may be finite or infinite. Since infinite counterexamples to liveness formulas can be represented as infinite strings of the form x y ω , in this case i k+1 is truncated to a finite initial segment that would normally include at least one execution of the infinite loop y ω , such as i k+1 = x y. Observing the failure of infinite test cases is of course impossible, and the LBT architecture implements a compromise solution that executes the truncated input sequence only, and issues a warning rather than a definite test failure. If the next test case i k+1 cannot be constructed by model checking then in order to proceed with iterative testing a random input string generator (see Figure 1) is used to generate i k+1 . During this random generation process, any random string that has been used as a previous test case is discarded to avoid redundant replicate tests.

BN Model Checker

Oracle

Thus from one of two possible sources (model checking or random generation) a new test case i k+1 is constructed. Figure 1 shows that this new test case i k+1 is then executed on the SUT S to yield an actual output sequence o k+1 = o 1 , . . . , o j . The pair ( i k+1 , o k+1 ) is then passed to an oracle to compute the k + 1-th test verdict.

The oracle we have developed for this LBT architecture is more powerful than the one described in [START_REF] Meinke | Incremental learning-based testing for reactive systems[END_REF], and is based on the following two step process.

Step 1. A test verdict can often be derived quickly and simply by computing a predicted output p k+1 = p 1 , . . . , p j obtained by simulating the behavior of M k on i k+1 . This is easily derived by applying the TRS R k to rewrite the input string i k+1 into its normal form, i.e. i k+1 R k -→ * p k+1 . Recall that R k is a complete TRS, so this normal form is always well defined. We then implement a simple Boolean test o k+1 = p k+1 . If this equality test returns true and the test case i k+1 was originally a finite test case then we can conclude that the test case i k+1 is definately failed, since the behaviour p k+1 is by construction a counterexample to the correctness of φ. In this case we can decide to stop testing. If the equality test returns true and the test case i k+1 was finitely truncated from an infinite test case (a counterexample to a liveness requirement) then the verdict is weakened to a warning (but testing is not stopped). This is because the most we can conclude is that we have not yet seen any difference between the observed behaviour o k+1 and the incorrect behaviour p k+1 .

Step 2. If the Boolean test o k+1 = p k+1 in Step 1 returns false then more work is needed to determine a verdict. We must decide whether the observed output o k+1 is some other counterexample to the correctness of φ than p k+1 . This situation easily occurs when the requirement φ is a loose specification of the SUT behavior, such as a constraint or value interval. In this case we can evaluate the requirement formula φ instantiated by the input and actual output sequences i k+1 and o k+1 to determine whether φ is true or false. For this we perform a translation similar to SatSet 0 (φ) but with the variables x n and out instantiated by the appropriate components of i k+1 and o k+1 respectively. We then evaluate all resulting sets of variable free equations and negated equations by rewriting. By Theorem 1, this approach will produce a correct verdict if o k+1 is a counterexample to φ.

Note that while Step 1 was already described in [START_REF] Meinke | Incremental learning-based testing for reactive systems[END_REF],

Step 2 is an additional and more powerful step made possible by the translation of LTL into equational logic, and the use of term rewriting to implement the latter.

When the conditions of Theorem 3 are satisfied by the underlying data type then the LBT architecture of Figure 1 can be proven to terminate since the CGE algorithm correctly learns in the limit and basic narrowing is terminating and solution complete. A detailed analysis of this property will be published in an extended version of this paper. The argument is similar to that presented in [START_REF] Meinke | Incremental learning-based testing for reactive systems[END_REF].

A Case Study of LBT for Reactive Systems

Since the overhead of model checking an EMA by narrowing is high, it is important to study the performance of our LBT architecture in practice using case studies. Now many communication protocols can be modeled as EMA computing over (freely generated) symbolic data types. Thus the LTL decidability results of Section 4 apply to this class of examples.

The Transmission Control Protocol (TCP) is a widely used transport protocol over the Internet. We present here a performance evaluation of our LBT architecture applied to testing a simplified model of the TCP/IP protocol as the 11 state EMA shown in Figure 2. In this performance evaluation, we considered the fault detection capability of LBT compared with random testing. A coverage comparison of learning-based with random testing is for example [START_REF] Walkinshaw | Increasing functional coverage by inductive testing: a case study[END_REF], which even considers the same TCP case study. The methodology for comparison was to start from the concrete model of TCP in Figure 2 and consider a variety of correctness requirements as LTL formulas (including use cases). We then injected transition mutations into the SUT which falsified each individual requirement separately. In this way, several different kinds of bugs were introduced into the protocol model, such as mutating the input/output on transitions, adding extraneous transitions or states and so on. Some of these artificial mutations reflect realistic defects that have been discovered in several TCP/IP implementations [START_REF] Guha | Network security via reverse engineering of tcp code: vulnerability analysis and proposed solutions[END_REF].

Below we informally define five requirements on the TCP/IP protocol and give an LTL formalization of each.

1. Use case. Whenever the entity receives an active_open and sends out a SYN, the entity will send out a SYNACK if it receives a SYN, or send out an ACK if it receives a SYNACK, and send nothing when receiving other inputs.

G( (in = active_open

∧ out = syn) → X((in = syn → out = synack) ∧ (in = synack → out = ack)) )
2. Use case. Whenever the entity receives an active_open and sends out a SYN and then receives a SYNACK, the entity will send out an ACK and then will send out an ACK if it receives a FIN.

G( (in = active_open

∧ out = syn ∧ X in = synack) → (X out = ack ∧ X 2 (in = fin → out = ack)) )
3. Use case. Whenever the entity performs the IO (active_open, SYN ) and receives SYNACK followed by FIN it will send out ACK followed by ACK and then send out FIN if it receives CLOSE.

G( (in = active_open

∧ out = syn ∧ X in = synack ∧ X 2 in = fin) → (X out = ack ∧ X 2 out = ack ∧ X 3 (in = close → out = fin)) )
4. Whenever the entity receives a close and sends out a FIN, or receives a FIN and sends out an ACK, the entity has either sent a passive_open or received an active_open before, and either sent or received a SYN before.

G( ((in = close

∧ out = fin) ∨ (in = fin ∧ out = ack)) → (F -1 (in = pass_open ∨ in = active_open)∧F -1 (in = syn ∨ out = syn)) )
5. Whenever the entity performs the IO (FINACK, ACK ) it must have received or sent SYN in the past and performed the IO (close, FIN ) in the past.

G( (in = finack

∧ out = ack) → (F -1 (in = syn ∨ out = syn) ∧ F -1 (in = close ∧ out = fin)) )

Results and Analysis

To compare LBT with random testing on the TCP/IP stack model, we measured two related parameters, namely: (i) the time t f irst (in seconds), and (ii) the total number of queries (i.e. test cases) Q f irst needed to first discover an injected error in the SUT. To conduct random testing, we simply switched off the CGE and model checker algorithms. The performance of LBT is non-deterministic due to the presence of random queries. Therefore each value of t f irst and Q f irst is an average obtained from over 1000 LBT runs using the same injected error. The results of testing the requirements Req1 to Req 5 are listed in Table 1. Note that Q f irst is the combined sum of the number of model checking queries M CQ and random queries RQ. These are also listed in columns 6 and 7 to provide deeper insight into the strengths and weaknesses of our method. In the final column, Hyp_size is the state space size of the learned hypothesis automaton at time t f irst . Since Hyp_size is always considerably less than 11 (the state space size of our SUT), this confirms the advantages of using an incremental learning algorithm such as CGE.

Requirement Random Testing LBT Q f irst t f irst (sec) Q f irst t f irst (sec) M CQ RQ
We wish to draw two main conclusions from Table 1.

(i) At the level of logical performance, (comparing Q f irst for LBT against Q f irst for random testing) we see that LBT always finds errors with significantly fewer test cases ranging between 0.25% and 18% of the number required by random testing. Therefore, if the overheads of model checking and learning can be reduced then LBT also has the potential to outperform random testing in real-time performance.

(ii) At the level of real-time performance (comparing t f irst for LBT against t f irst for random testing) we see that LBT is often but not always significantly faster than random testing, ranging between 0.9% and 160% of the time required by random testing. This reflects the actual real-time overhead of performing both model checking and learning for the SUT and each requirement.

Looking more closely at the results for Reqs 4 and 5, where LBT is somewhat slower than random testing, we can gain deeper insight into these real-time performance issues. For Reqs 4 and 5 both the values M CQ and the ratios RQ/M CQ are significantly higher than for Reqs 1, 2 and 3. In these cases, basic narrowing is performing a large number of constraint solving tasks on unsatisfiable sets of constraints. However, basic narrowing fails very slowly when no solutions can be found. After this, random test cases are applied to proceed with the task of learning the SUT, but these do not necessarily test the actual requirements.

These preliminary results are nevertheless promising, and based on them we make some suggestions for how to further improve narrowing in Section 7. Thus we can improve the overall real-time performance of our current LBT architecture to achieve a real-time performance closer to the logical performance. It should also be pointed out that as real-time measurement involves factors such as efficiency of implementation, there exists further scope for improvement on the implementation level.

Conclusions

In this paper we have shown how a model checker based on narrowing can be combined with a symbolic automaton learning algorithm such as CGE to give a new architecture for black-box specification-based testing using the learningbased testing (LBT) paradigm. We have benchmarked this LBT architecture against random testing, and shown that it compares favorably, with the potential for future improvement.

The results of Section 6.1 suggest that a pure narrowing procedure could be significantly improved by interleaving it with theorem proving techniques to detect unsatisfiability. This is because counterexamples to correctness may be sparse, in which case narrowing fails very slowly. Term rewriting could be applied to this problem too. Furthermore, it is known that basic narrowing modulo theories is incomplete and suggestions such as the variant narrowing of [START_REF] Escobar | Variant narrowing and equational unification[END_REF] could be considered. Finally, we observe that the CGE algorithm does not currently learn infinite state Mealy automata, and this is another extension of our work that must be considered for EMA.

Theorem 4 .

 4 Let (R state n , R output n ) be the output of the CGE learning algorithm after a sequence of n observations of the I/O behavior of an EMA A. Then R n = R state n ∪ R output n is a complete rewrite system and every R n -narrowing derivation terminates.

Fig. 1 .

 1 Fig. 1. A Learning-based Testing Architecture for Reactive Systems

Fig. 2 .

 2 Fig. 2. TCP Mealy Machine Model

  The rewrite relation

				R -→ associated
	with a TRS R is a binary relation on terms defined by t	R -→ t if there exists
	a rule l → r ∈ R, a position p ∈ O(t) and a substitution σ such that t| p ≡
	σ(l) and t ≡ t[σ(r)] p . We call t	R -→ t a rewrite step. We let	R * -→ denote the
	reflexive transitive closure of	R -→ . A TRS R is strongly normalising if there is
	no infinite sequence of rewrite steps t 0 (or Church-Rosser) if for any terms t, t 1 , t 2 ∈ T (Σ, X) s if t R -→ t 1 R R -→ . . . and R is confluent -→ t 2 R * -→ t 1 and t R * -→ t 2
	then there exists t ∈ T (Σ, X) s such that t 1	R * -→ t and t 2	R * -→ t . A complete
	TRS is confluent and strongly normalising.

Table 1 .

 1 Random testing versus LBT: a performance comparison

	Hyp_size

Acknowledgement

We gratefully acknowledge financial support for this research from the Chinese Scholarship Council (CSC), the Swedish Research Council (VR) and the European Union under project HATS FP7-231620. We also acknowledge the helpful comments of the referees in producing the final version of this report.


Christian Schwarzl
email: christian.schwarzl@v2c2.at

Bernhard K Aichernig
email: aichernig@ist.tugraz.at

Franz Wotawa
email: wotawa@ist.tugraz.at

Compositional Random Testing using Extended Symbolic Transition Systems

Keywords: symbolic transition system, concurrent reactive behavior, test case generation

The fast growth in complexity of embedded and software enabled systems requires for automated testing strategies to achieve a high system quality. This raise of complexity is often caused by the distribution of functionality over multiple control units and their connection via a network. We define an extended symbolic transition system (ESTS) and their compositional semantics to reflect these new requirements imposed on the test generation methods. The introduced ESTS incorporates timed behavior by transition execution times and delay transitions. Their timeout can be defined either by a constant value or an attribute valuation. Moreover we introduce a communication scheme used to specify the compositional behavior and define a conformance relation based on alternating simulation. Furthermore we use the conformance relation as the basis for a simple random test generation technique to verify the applicability of the presented approach. This formal framework builds the foundation of our UML test case generator.

Introduction

Since testing is an important task to ensure a certain system quality, the used techniques and approaches in this field strongly advanced in recent years. Nevertheless testing still remains a laborious task and is -due to the high degree of manual interaction -error prone. The steadily increasing complexity of embedded systems requires a high degree of test automation to be able to execute and analyze the large amount of needed test cases.

A further increase in automation can be achieved by the generation of test cases from formal specifications, which has gained a lot of attention in research in recent years and becomes more and more popular in the industry. However, the currently available industrial-and scientific-tools based on unified modeling language (UML) state machines or symbolic transition systems (STSs) [START_REF] Frantzen | Test generation based on symbolic specifications[END_REF] are limited to a single model. This situation does not meet the requirements of modern embedded systems, which often consists of communicating components.

For this reason we have implemented a test case generation algorithm, which works on the basis of an extended symbolic transition system (ESTS) composition presented in this work. This prototype supports a systematic and randomized test generation approach, which detailed description is beyond the focus of this paper.

Our contribution in this work is the extension of the STS by delay-and completion-transitions, timing groups, transition priorities and their execution duration. In addition we provide a precise semantics and formally define the model composition. Furthermore we show the applicability of the presented symbolic framework by a randomized test generation approach and the conformance relation to the system under test (SUT).

The remainder of the paper is structured as follows: Section 2 defines the structure of an ESTS and Section 3 precisely describes the compositional behavior. In Section 4 a conformance relation based on alternation simulation is provided and the applicability of the presented approach is demonstrated in Section 5. Section 6 presents an overview of the related work and Section 7 concludes the paper and gives a short outlook.

Extended Symbolic Transition System

In this section we define the structure of an ESTS and its semantics with respect to its contained states and transitions. Based on this structure we explain the creation of traces through the ESTS caused by external interactions.

Definition 1 (Extended Symbolic Transition System

). An ESTS is a tuple S, Λ, A, P, T , G, s 0 , ι 0 , where S is a set of states, Λ are the signals, A are the attributes, P are the signal parameters, T is the transition relation and G is a set of timing groups. Moreover s 0 is the initial state and ι 0 is the initial attribute valuation. 3We define the set of signals Λ = Λ i ∪ Λ o as the union of input Λ i and output Λ o signals. The set Λ * = Λ ∪ {τ, γ, δ} is the complete set of all defined signals, whereas the constants τ, γ, δ / ∈ Λ represent the special unobservable-, completion-and delay-signal types, respectively. The attributes A are the variables of an ESTS and the parameters P are variables attached to input-or output-signals λ ∈ Λ. Further it holds that A ∩ P = ∅ and we use V = A ∪ P.

The transition relation of an ESTS is defined as T ⊆ S × Λ * × F(V ) × T(V ) × P × S, where F(V ) is a first order logic formula without quantifiers, T(V ) are attribute value assignment statements given as mathematical terms over the variables V and P are the priorities.

We write a transition t ∈ T as s λ,ϕ,ρ,pt -----→ s , where s ∈ S is its source state, s ∈ S is the destination state, λ ∈ Λ * defines its type, ϕ ∈ F(V ) is the guard, the action ρ = ρ 1 , ρ 2 , .., ρ n is an ordered list of assignment terms ρ j ∈ T(V ) with list index j and p t ∈ P is its priority, where p t ∈ N 0 . A transition t ∈ T has a traversal probability α t ∈ R and an execution duration d t ∈ N 0 in addition. We omit the presentation of the priority p t in the remainder for simplicity if the context allows it.

Definition 2 (Timing Group). A timing group g is a tupel c, S δ , T δ , T r , where c is its clock, S δ ⊆ S are the contained states, T δ ⊆ T are the delay transitions and T r ⊆ T are the clock reset transitions.

A timing group g ∈ G specifies a set of states S δ where each of these states has an outgoing delay transition t δ ∈ T δ with the same timeout n δ ∈ N 0 . The states in the timing group share a clock c, which is used to trigger the traversal of one of these outgoing delay transitions. The timeout of a delay transition can either be defined by a constant-or by an attribute-value like n δ = 100 or n δ = x if x ∈ A. Our delay transitions should not be confused with the similar delay transitions in timed automata semantics. In timed automata semantics, delay transitions serve to express the possible waiting times in a state and hence are reflexive transitions increasing time only. Our delay transitions increase time and change the state.

We require that every state s ∈ S δ has an outgoing delay transition t δ ∈ T δ to the same destination state s ∈ S. This ensures that one of the delay transitions is traversed after the defined amount of time -specified by the timeout of the delay transitions -within the timing group has elapsed. The timing group clock is set to zero if one of the clock reset transitions t r ∈ T r is traversed.

We use ϑ = ι ∪ ς as variable valuation containing the values of attributes ι and the current signal parameters ς. Accordingly we denote the update of a variable valuation ϑ according to an action ρ as ϑ → ϑ (ρ). Given a valuation ϑ and a guard ϕ we write ϑ |= ϕ if the valuation satisfies the guard ϕ, which is a first order logical formula.

Example 1. Figure 1 shows an illustrative example of two communicating ESTS, where we use ? to mark input-and ! for output-signals, the keyword delay(x) to indicate delay transitions, the parameter x to denote the delay time and show only the guard of the completion transition γ. Blocking states as given in Definition 4 are shown with two border lines and states belonging to the same timing group are filled gray. Since each of these ESTSs contains only one timing group their presentation is unambiguous. Transition guards are shown within squared brackets and actions follow a slash.

Definition 3 (Configuration).

A configuration q is a tuple s, ι , where s ∈ S is an explicit state and ι specifies the values of all attributes in A.

A configuration fully defines the current state of an ESTS and accordingly we define the initial state q 0 = s 0 , ι 0 , where s 0 is the initial state and ι 0 the For the following definitions we use t ∈ T , λ ∈ Λ, λ * ∈ Λ * and g ∈ G.

The function src(t) returns the transition source state, dest(t) its destination state, signal(t) the signal of a transition, arity(λ) ∈ N 0 the number of signal parameters and dur(t) the execution duration d t .

In addition we use out(s, λ * ) = {t ∈ T | signal(t) = λ * ∧ source(t) = s} returning all outgoing transitions of s having signal λ * , delay(t) = n if signal(t) = δ or n = 0 otherwise, providing the delay time of a transition and delay min (t) = min ( delay(t δ ) | t δ ∈ out(src(t), δ)), which is is the minimum delay of currently active delay transition.

The function prio(t) returns the transition priority p t and prio max (s, λ) = max ( {prio(t) | t ∈ out(s, λ)}) calculates the maximum priority of all outgoing transitions from state s having signal λ. clk(t) = {c(g) | src(t), dest(t) ∈ states(g) ∧ t / ∈ r(g)} returns the set of all timing groups to which the given transition belongs.

The function reset(t) = {c(g) | t ∈ r(g)} defines the clocks which are reset by a traversal of t, where c(g) returns the clock c, r(g) the clock reset transitions T r and states(g) the contained states S δ of the given timing group g.

Example 2. Let the ESTS A shown in Figure 1 be initialized with the configuration q 0 = A0, {x = 0, y = 0} . After the traversal of the transition ------------------------→ A1 with the parameters p1 = 70 and p2 = 6 the ESTS A has the configuration q = A1, {x = 70, y = 6} as defined by the transition action.

A0 ?a[0≤p1≤200&0≤p2≤10]/x=p1;y=p2;

Semantics

This section describes the behavior of every allowed transition type, which is defined by the prerequisites of the transition traversal and the performed state and attribute value changes.

We define the semantics of an ESTS in the Rules ( 1) to ( 6), where we require ϑ |= ϕ if not stated differently, we use Q ⊆ Q as the set of configurations after a transition traversal and → denotes an assignment mapping. The shown semantics is similar to the one presented by Frantzen et. al, but we only describe the evaluation of the post state to highlight the extensions.

Rule Empty (1) states that the state and the valuation does not change if the empty signal is executed, where indicates that the guard is always satisfied and id is the identity function.

s , ,id ----→ s Q → { s, ϑ } (1)
In Input (2) the semantics of a signal reception λ i ∈ Λ i is defined, where a signal reception can only be executed if it is sent before an active timeout. Rule Timed (3) shows that a delay transition with the shortest delay is executed as soon as the defined amount of time has elapsed. After the traversal the current state and the attribute valuation are updated and the clocks of the timing groups where t ∈ T r are set to zero.

s λi,ϕ,ρ,pt ------→ s ∧ p t = prio max (s, λ i ) ∧ ∀c ∈ clk(t) | c < delay min (t) Q → { s , ϑ (ρ) }, ∀c ∈ clk(t) | c → c + dur(t), ∀c ∈ reset(t) | c → 0 (2) s δ,ϕ,ρ,pt -----→ s ∧ p t = prio max (s, δ) ∧ c(t) ≥ delay(t) ∧ delay(t) = delay min (t) Q → { s , ϑ (ρ) }, ∀c ∈ clk(t) | c → c + delay(t) + dur(t), ∀c ∈ reset(t) | c → 0 (3)
The rules Output (4) and Completion (5) have the same behavior in terms of updating configurations and the handling of the clock updates as in ( 2), but are executed as soon their guard is satisfied. They differ in the IO behavior, because in (4) a signal is sent and ( 5) only allows for a deterministic configuration update.

s λo,ϕ,ρ,pt ------→ s ∧ p t = prio max (s, λ o ) Q → { s , ϑ (ρ) }, ∀c ∈ clk(t) | c → c + dur(t), ∀c ∈ reset(t) | c → 0 (4) s γ,ϕ,ρ,pt -----→ s ∧ p t = prio max (s, γ) Q → { s , ϑ (ρ) }, ∀c ∈ clk(t) | c → c + dur(t), ∀c ∈ reset(t) | c → 0 (5)
Unobservable (6) defines the semantics of a non-deterministic configuration update. The traversal of an τ transition is not observable and the resulting symbolic states in Q are its source and destination state.

s τ,ϕ,ρ,pt -----→ s ∧ p t = prio max (s, τ ) Q → { s, ϑ , s , ϑ (ρ) }, ∀c ∈ clk(t) | c → c + dur(t), ∀c ∈ reset(t) | c → 0 (6)

Simulation

In this section the execution of an ESTS is explained by the creation of execution traces caused by signal receptions or delays. Such execution traces are always embedded between two blocking states described in Definition 4.

Definition 4 (Blocking State

). A blocking state s is a state s ∈ S for which it holds that ∃λ ∈

λ i ∪ δ | |out(s, λ)| = 0 ∨ out(s, λ * ) = ∅.
This means a blocking state is a state having at least one outgoing transition of type λ i or δ or no outgoing transition λ * ∈ Λ * at all. Accordingly we denote a blocking configuration as q = s, ι . Note that a blocking state does not limit the occurrence of outgoing τ, γ or λ o ∈ Λ o transitions, which makes a mixed state possible. Since we allow outgoing output transitions, the state is not a quiescent state as defined in [START_REF] Frantzen | Test generation based on symbolic specifications[END_REF] or [START_REF] Tretmans | Test generation with inputs, outputs, and quiescence[END_REF].

Based on Definition 4 we can define an execution trace as shown in Definition 5, which connects two blocking states and must not be interrupted. It is a sequence of transitions and consists of a triggering η t and completion η c part, where η t consists only of transitions with signals

Λ t = Λ i ∪ δ and Λ c = Λ o ∪ γ ∪ τ .

Definition 5 (Execution Trace

). An execution trace η = t 1 , t 2 , . . . , t n is a sequence of transitions t 1 , . . . , t n , where

η t = t 1 , η c = t 2 , . . . , t n and ∀t i ∈ η \ t 1 | dest(t i ) = source(t i+1 ).
The length of an execution trace is denoted as |η| and it holds that |η| ≥ 1, where |η t | = 1 and |η c | ≥ 0. Due to the allowed non-deterministic behavior of an ESTS a signal reception or a time lapse can cause multiple execution traces leading to the resulting list E(q, λ). Its recursive generation is defined by E (q, λ) = {e(η) | η ∈ E(q, λ)}, where λ ∈ Λ c is the triggering input, q ∈ Q is the current configuration and E (q, λ) is initialized with t ∈ out(q, λ) | ϑ |= ϕ.

The function e(η) is defined in Equation ( 7), where q is the destination state of the last contained transition in η and • is the concatenation of traces.

e(η) =          tc {e(η • t c ) | t c ∈ out(q , Λ c )} if out(q , Λ t ) = ∅ ∧ out(q , Λ c ) = ∅ η ∪ tc {e(η • t c ) | t c ∈ out(q , Λ c )} if out(q , Λ t ) = ∅ ∧ out(q , Λ c ) = ∅ η otherwise (7)
The recursive generation of the completion steps in [START_REF] Hessel | Testing real-time systems using UPPAAL[END_REF] creates an infinite number of traces if a loop of completion transitions exists, which actions do not falsify one of its guards.

Example 3. Let ESTS A shown in Figure 1 again be initialized with q 0 = A0, ι 0 , where ι 0 = {x = 0, y = 0}. Then we can build the list of initial ex-

ecution traces E( q0 , λ) = A0 ?a[0≤p1≤200&0≤p2≤10]/x=p1;y=p2; ------------------------→ A1, because we use λ = a, ϑ = ι 0 ∪ ς and ς = {p1 = 30, p2 = 9},
which satisfies the transition guard. If we would use ς = {p1 = 30, p2 = 15} instead, then E(q, λ) = ∅ because p2 > 10. The recursive update of this list leads to the final trace list

E( q0 , λ) = A0 ?a[0≤p1≤200&0≤p2≤10]/x=p1;y=p2; ------------------------→ A1 !b[p1=y] -----→ A2 [x>50]
----→ A3, where the first transition is the triggering-η t and the last two transitions are the completionη c part. The last transition has to be added, because ϑ = {x = 30, y = 9} |= ϕ of the completion transition, which is executed immediately after its guard is satisfied.

Composition

In this section the model composition based on the signal communication between the involved ESTSs is explained. Furthermore we clearly define the observations and interactions, which can be made by the environment.

Model Communication

In this work we use a deterministic communication scheme using a global queue Q to pass signals between ESTSs. Since we required that an execution trace must not be interrupted, the system behavior can be described by an concatenation of such traces. This concept is similar to the approach presented in the language Creol [START_REF] De Boer | A complete guide to the future[END_REF], where only one thread is active at a time.

The reception of a signal λ or the lapse of time in the state q leads to a list of execution traces η ∈ E (q, λ). The needed execution time or the sent signals by a trace η can cause reactions in other ESTSs or the environment. Therefore a list of system execution traces E M (q, λ) has to be created, where M ⊆ M is the set of all involved ESTSs. These traces contain the initial trace η and its concatenated reaction traces of the other ESTSs.

Since not every signal needs to be sent or be observable by the environment -e. The required state updates in the other ESTSs are performed using the signals in obs(η), which are passed via the global message queue Q. The execution uses the same algorithm as described above and leads to the execution trace η m ∈ E m (q, λ) in the ESTS m ∈ M . We call a trace η M ∈ E M (q, λ) containing the initial execution trace η and all according reactions η m system execution trace in the remainder.

Definition 7 (System Execution Trace). A system execution trace η

M = η m1 • • • • • η m N is the catenation of execution traces η mi of an ESTS m ∈ M , where i = 1..N , N = |M | is the number of entries in M and M ⊆ M is the set of involved ESTS. rt(η) =    η if obs(η) = ∅ η {η • η | η ∈ rt (η m ∈ E m (q m , λ) | λ ∈ obs(η))} otherwise (8)
The creation of system execution traces is defined recursively by the reception trace function rt(η) shown in Equation ( 8), where qm is the current configuration of m ∈ M . It shows that a system trace is a recursive concatenation of all execution traces of other ESTSs caused by the output signals on the initial path. Given the initial traces η ∈ E(q, λ), we can build a list of all possible execution traces E M (q, λ) = rt(η) | η ∈ E(q, λ) This algorithm ensures that all signals stored in the queue are processed before the next execution step can begin. However, each execution trace can also produce output signals, which are also enqueued as described above. This allows for the creation of infinite loops between the involved ESTS, where a signal reception causes an output signal received in another ESTS, which reception causing the initial signal sending responsible for the initial stimuli.

Since the reception of signals has a higher priority than the traversal of delay transitions, their influence was neglected during the finding of the system execution traces. Due to the fact that the traversal of a transition t needs the time dur(t) to be completed, the execution time is calculated in the function time(η) given in [START_REF] Schwarzl | Static-and dynamic consistency analysis of UML state chart models[END_REF].

time(η) = N i=1 dur(t i ) + delay(t i ) -time(η g (t i )) (9)
In ( 9) η g is the connected sub-trace of η consisting of the transitions contained in the timing group g to which the transition t i belongs. Since an execution trace can also contain transitions not belonging to the ESTS m, which is the owner of the timing group g, these transitions still have to be included. A formal definition of the sub-trace creation is given in [START_REF] Schwarzl | Test sequence generation from communicating UML state charts: An industrial application of symbolic transition systems[END_REF], where i is the index of t i in η. It uses [START_REF] Tretmans | Test generation with inputs, outputs, and quiescence[END_REF] to extract the trace from η according to the given indices and ( 12) to find the start index of the trace based on (13) returning the transitions of the ESTS to which the transition t i belongs.

η g (t i ) = sub(η, i, k) | k = idx e (t i , T m ), T m = gtrace(η, t i ) (10)
Using Definition 5 a sub-trace of η is given by [START_REF] Tretmans | Test generation with inputs, outputs, and quiescence[END_REF], which consists of the transitions in η lying in the range [i, j], which is defined by the given indices.

sub(η, i, j) = t i , ..,

t j | t i , t j ∈ η ∧ 1 ≤ i, j ≤ |η| ∧ j ≥ i (11)
In [START_REF] Veanes | Alternating simulation and IOCO[END_REF] the minimum index k of the of the given transition t in T m is calculated, which references to the first transition of the trace stored in T m .

idx e (t, T m ) = k ∈ N | (∃t k ∈ T m | k = min idx (T m )) (12)
The function gtrace(η, t i ), as defined in [START_REF] Veanes | Model-based testing of object-oriented reactive systems with Spec Explorer[END_REF], returns all transitions and their indices in η satisfying the following criteria, where g is the timing group belonging to t i . The first term of the constraint t j ∈ η requires that the transition belongs to η and the second term src(t j ), dest(t j ) ∈ states(g) that the transitions are contained in the same timing group as t i . Term three dest(t j ) = src(t j+1 ) ensures that the transitions represent a trace without any structural holes. The last term ∃t j = t i requires that the given transition t i is contained in that connected trace to prevent an ambiguous result if t i is traversed multiple times in trace η.

gtrace(η, t i ) = {t j |t j ∈ η ∧ src(t j ), dest(t j ) ∈ states(g) ∧ dest(t j ) = src(t j+1 ) ∧ ∃t j = t i } (13)
The elapsed time time(η M ) is used to trigger active delay transitions after the processing of the enqueued output signals has finished. This is done by finding the transition with the smallest time overdue δ due = delay(t)time(η M ). If such a transition exists it is executed using the same algorithm as described above. The execution can again cause the sending of new output signals, which are processed before the next delay transition is taken into account. This algorithm again allows for the modeling of an infinite loop, if two traces exist with time(η 1 ) ≥ delay(t 2 ) and time(η 2 ) ≥ delay(t 1 ) and which lead to their own source state, where η 1 and η 2 are the execution traces to the transitions t 1 and t 2 , respectively. The execution traces gained from the processing of the delayed transitions are then concatenated to η being the final result.

In this approach we defined that the treatment of a signal reception has a higher priority than the traversal of an delayed transition. These rules allow that an active delay transition, whereas enough time has elapsed to trigger the traversal, is not traversed in favor to the transition receiving a signal from Q, even if the signal was enqueued after the timeout of a delayed transition.

Conformance

In this section the correctness of an implementation under test (IUT) with respect to a specification using alternating simulation [START_REF] Alur | Alternating refinement relations[END_REF] is explained. For simplicity, we only discuss the conformance of deterministic ESTS here. In the nondeterministic case the two ESTSs need to be determinized beforehand, similar to [START_REF] Veanes | Alternating simulation and IOCO[END_REF]. Generally it is required that the IUT can follow all inputs generated from and only produces outputs allowed by the specification. To provide a precise understanding we introduce the function moves(q, Λ) shown in Equation ( 14) first, where M ⊆ M is a set of ESTSs, qM = qm | m ∈ M and qm is the blocking configuration of an ESTS m ∈ M . This function returns the union of all outgoing transitions of all m ∈ M at state qm , which guard is satisfied and signals are contained in the given set Λ.

moves(q M , Λ) = {t | src(t) = qM ∧ qM |= ϕ t ∧ signal(t) ∈ Λ} (14)
The meaning of alternating simulation as defined in [START_REF] Veanes | Alternating simulation and IOCO[END_REF] is formalized in Equation ( 15) and ( 16), where q1 ∈ Q 1 and q2 ∈ Q 2 are the sets of configurations of the IUT and the specification, respectively. Accordingly λ 1 = signal(t 1 ) and λ 2 = signal(t 2 ) are the signals of these transitions and q 1 and q 2 are the destination configurations.

∀t 2 ∈ moves(q 2 , Λi ∪ δ) | (∃t 1 ∈ moves(q 1 , Λi ∪ δ) | λ 2 = λ 1 ∧ q 2 = q 1 ) (15)
Equation ( 15) states that all input or delay transition traversable in the specification in state q2 ∈ Q 2 , which has a certain attribute valuation must also be executable on the IUT.

∀t 1 ∈ moves(q 1 , Λo ) | (∃t 2 ∈ moves(q 2 , Λo ) | λ 1 = λ 2 ∧ q 1 = q 2 ) ( 16
)
The inverse is true for outputs as shown in Equation ( 16), where it is required that every output produced by the IUT must be allowed by the specification. If both equations hold, then the basic I/O behavior of the implementation is correct with respect to the specification.

Since Equation ( 15) and ( 16) do not provide any information on the time behavior, we require in addition that the obtained output of the IUT fulfills the the timing constraints given in the ESTSs. Therefore we require that Equation (17) holds, where η ∈ E 2 (q 2 , signal(t 2 )) and η ∈ E 1 (q 1 , signal(t 2 )) are the execution traces created for a given input on the IUT and specification respectively.

∀ λ o , d j ∈ obs(η) | (∃η | λ o , d j ∈ obs(η ) ∧ λ o = λ o ∧ min( d) ≤ d ≤ max( d))
(17) Equation ( 17) requires that for every observable output λ o at time d part of the trace η produced by the IUT an according transition t o ∈ η exists, which contains the same outputs λ o within the time range d. In (17) j = 1..|η| is the index of the output occurrence in η. The time range d is given in Equation ( 18), which is the sum of the execution time elapsed up to the transition at position k = idx(t o , η ) and includes a transition time jitter

ε k . d = time(sub(η , 1, k)) ± ε k (18)
Since we have now defined the required outputs including the occurrence time of the IUT after an input was provided by the specification, we can now check the correctness of the IUT with respect to a given specification. Alternating simulation has the advantage in comparison to ioco that the conformance check is computational less intense and provides the same expressive power in the deterministic case [START_REF] Veanes | Alternating simulation and IOCO[END_REF].

Application

We show the applicability of the presented approach on a simple random test case generation example based on the ESTSs shown in Figure 1. In this example the external communication consists of the signals Λi = {a, c} and Λo = {d} and the internal communication is given by Λi = {b} and Λo = {b}.

In this random approach named random walk, we explicitly trigger the traversal of outgoing transitions from the current state q. This is done by the generation of feasible data for the transitions t ∈ moves(q, Λi ) and the lapse of time for delay transitions. The input generation is done separately for each transition t by a constraint solver e.g. provided by GNU Prolog as in our case, which tries to find solutions satisfying the transition guards.

If multiple transitions are possible during this phase, meaning they leave the current state and their guard can be satisfied, we normalize their probabilities α and perform a random selection. Since we also want to generate sequences, which vary in their temporal behavior, the random selection of an explicit wait can also be chosen. In such a case the used wait time t w has to be 0 ≤ t w ≤ δ min , where δ min is the smallest timeout of all active delay transitions.

In the case an input action has been selected it is sent to and executed on the according ESTS. Wait actions in contrast are executed on the whole system, because the smallest active delay can belong to any of the involved ESTSs. After the input or wait action was performed the system execution traces E M (q, λ) are generated.

Figure 2 shows three traces, which can be obtained if the inputs are applied as given in Table 1 time is longer than the required delay. For these examples we assumed that ever transition has the same execution duration t d = 10.

Both tables also show the observable output generated by each trace, which can be used during the execution of the test case on the SUT. Since it also includes the latest point in time of the real signal reception, it is possible to check given timing constraints.

The random walk can be used for on-the-fly and offline test case generation. During on-the-fly testing the SUT is executed in parallel to the model and the input and outputs can be processed immediately. The advantage of this approach is that the current state is always known, which limits the state space especially in the presence of non-determinism. For offline test case generation all possible traces have to be stored and extended with every step during the random walk. Since non-determinism is allowed, the possible execution traces can be seen as a tree. This requires that the random walk has to continue in one step from every active leaf of this tree, to generate feasible test cases. Depending on the model these trees can become quite big due to the high number of possibilities.

Related Work

Several approaches based on symbolic transition systems have been studied in recent years. STG [START_REF] Clarke | STG: A symbolic test generation tool[END_REF] is a symbolic extension of the test tool TGV and allows the generation of test cases with respect to a given test purpose. The presented framework extends the approach described in [START_REF] Frantzen | Test generation based on symbolic specifications[END_REF], by timed behavior, completion transitions and model composition. The approach in [START_REF] Frantzen | Test generation based on symbolic specifications[END_REF] is implemented in the STSimulator, which provides a framework for on-the-fly random testing and is used in the Jambition Project [START_REF] Frantzen | On-the-fly modelbased testing of web services with Jambition[END_REF] to automatically derive test cases for web applications. It uses sioco as conformance relation, which is the symbolic variant of ioco based on labeled transition systems (LTS).

Although the approaches described above were used successfully in various applications, they do not incorporate time as part of the specification. For this reason several extensions were introduced to lift the well understood approaches to timed models. This lead in the case of an LTS to its timed version and the according implementation relations like tioco and rtioco. A detailed discussion is given in [START_REF] Schmaltz | On conformance testing for timed systems[END_REF], where a survey about the similarities and differences between these approaches and their variants is provided. However, these techniques still rely on an enumerative treatment of data limiting the scalability in data intense applications.

Also model checkers based on timed automata (TA) like UPPAAL [START_REF] Hessel | Testing real-time systems using UPPAAL[END_REF][START_REF] Behrmann | A tutorial on UPPAAL[END_REF] were used for behavior specification and test case generation. The timing constraints in a timed automata are given as time invariants on states and clock guards on transitions. UPPAAL also allows the interaction of data and time, meaning that attribute values can be used in the timing constraints. Their approach still relies on an explicit modeling of data and therefore faces the same scalability problems as methods based on an LTS. For the generation of test cases UPPAAL requires a deterministic specification, which limits the range of applicable use cases.

A symbolic variant based on timed automata is defined in [START_REF] Styp | A conformance testing relation for symbolic timed automata[END_REF], where the symbolic timed automata (STA) is introduced. It is a combination of an STS with the timing handling of TA and also allows the usage of attribute values as bounds for timing constraints. On the basis of the STA the testing conformance relation stioco being an symbolic extension of tioco is described. Although an STA allows similar semantics, it does not include a formal description of a composition and neglects unobservable events at the moment.

Spec Explorer [START_REF] Veanes | Model-based testing of object-oriented reactive systems with Spec Explorer[END_REF], which can also use Spec# as specification language, uses alternating simulation to define the conformance between the IUT and the model. It was recently extended to work with UML sequence diagrams used for testing and program slicing. It also supports model composition in a similar way and allows the generation of test sequences based on a model composition. In contrast to the presented work no timed behavior can be modeled, which is which is one of the key features of the presented approach. Since Spec Explorer does no full symbolic state space exploration it allows a wider range of supported data types in contrast to this work, where we are limited to integer and boolean values.

Conclusion

We presented in this work an extended symbolic transition system based on the STS defined in [START_REF] Frantzen | Test generation based on symbolic specifications[END_REF]. Our approach extends this framework by the incorporation of delay-and completion-transitions for which we also provide a formal semantics. On top of the ESTS we defined a communication scheme, which uniquely defines the compositional behavior. In contrast to [START_REF] Frantzen | Test generation based on symbolic specifications[END_REF] we use alternating simulation as testing relation instead of ioco, for which we used the distinction between internal-and external-communication. This distinction allows for a clear sepa-ration between observable or controllable signals by the environment and those used internally.

We used this symbolic framework for a sample application allowing a random test case generation, which can be performed on-the-fly and offline. The incorporation of delay transitions and transition execution times allows for timing checks of the SUT like the verification of trace files containing time stamps.

The presented ESTS in this work contains similar elements as defined in UML state machines and therefore allows for a straight forward model transformation. For this reason it can be used as a formalization of the UML state machine semantics, which is required for test case generation. This is the first time we presented the formal framework on which basis we have implemented our test case generation prototype from UML state machines. Parts of the tools chain and its application on industrial use cases have been described in [START_REF] Schwarzl | Static-and dynamic consistency analysis of UML state chart models[END_REF] and [START_REF] Schwarzl | Test sequence generation from communicating UML state charts: An industrial application of symbolic transition systems[END_REF].

Future work includes the investigation of other communication schemata and an extension of the transition attributes to allow uncertainties in the timed behavior like t d = 100 ± 5. This would allow for checks ensuring that a certain signal did not arrive before a given point in time, which is required for modeling real time networks.

Fig. 1 .

 1 Fig. 1. Two communicating ESTSs A and B

  g. communication within one component -we split the signals into two categories. The first category contains signals observed or created by the environment Λ = Λi ∪ Λo | Λi ⊆ Λ i ∧ Λo ⊆ Λ o to which we refer as external communication in the remainder. The second category is the internal communication, which contains the signals Λ = Λo ∪ Λi | Λo = Λ o \ Λo ∧ Λi = Λ i \ Λi sent and received by one of the ESTSs. Note that signals part of the external communication must be and signals of the internal communication might be created or received by the environment. The trace output signals used for the communication are defined in Definition 6 and are independent of the observability by the environment. Definition 6 (Observables). Let obs(η) = λ o , d 1 , . . . , λ o , d N be the output signals of a trace η ∈ E (q, λ), where its result is a list of tuples, N is the number of output signals on the trace, λ o ∈ Λ o are the signals and d is the time period in which the signal has to be sent. We define the observableobs(η) = obs(η) | λ o ∈ Λo and unobservable obs(η) = obs(η) | λ o ∈ Λo output signals of η.

Fig. 2 .

 2 Fig. 2. Three system execution traces T 1, T 2 and T 3

Table 1 .

 1 and Table2. The inputs in Table2lead to the same trace T 3, but in the second case no additional wait is necessary, because the execution Inputs and outputs for traces T 1 and T 2

	XIII

Table 2 .

 2 Two possible inputs and outputs for trace T 3

In[START_REF] Frantzen | Test generation based on symbolic specifications[END_REF] a different naming convention is used, where states are locations, transitions are switches, attributes are location variables and parameters are interaction variables.

Acknowledgment

The authors wish to thank the reviewers, the "COMET K2 Forschungsförderungs-Programm" of the Austrian Federal Ministry for Transport, Innovation and Technology (BMVIT), the Austrian Federal Ministry of Economics and Labour (BMWA), Österreichische Forschungsförderungsgesellschaft mbH (FFG), Das Land Steiermark and Steirische Wirtschaftsförderung (SFG) for their financial support.