Boutheina Bannour
email: b.bannour@sherpa-eng.com

Jose Pablo Escobedo
email: jose-pablo.escobedo@cea.fr

Christophe Gaston
email: christophe.gaston@cea.fr

Pascale Le Gall
email: pascale.legall@ecp.fr

Off-line Test Case Generation For Timed Symbolic Model-Based Conformance Testing

Keywords: Model-based testing, off-line testing, real-time systems, test suite generation, verdict computation, symbolic execution, timed outputinput symbolic transition systems

Model-based conformance testing of reactive systems consists in taking benefit from the model for mechanizing both test data generation and verdicts computation. On-line test case generation allows one to apply adaptive on-the-fly analyzes to generate the next inputs to be sent and to decide if observed outputs meet intended behaviors. On the other hand, in off-line approaches, test suites are pre-computed from the model and stored under a format that can be later performed on testbeds. In this paper, we propose a two-passes off-line approach where: for the submission part, a test suite is a simple timed sequence of numerical input data and waiting delays, and then, the timed sequence of output data is post-processed on the model to deliver a verdict. As our models are Timed Output Input Symbolic Transition Systems, our off-line algorithms involve symbolic execution and constraint solving techniques.

Introduction

Using formal methods to generate test cases and to compute verdicts has been widely studied in the frame of Model Based Testing. In the domain of reactive systems, models are often given as labeled transition systems which describe the expected sequences of input and output data (called traces). Real executions of the System Under Test (SUT) can also be seen as traces. Testing an SUT comes to interact with it to build traces which are analyzed regarding to its model to provide verdicts. In black box testing, an SUT is often hardly controllable at the test execution phase, typically because, for the sake of abstraction, its reference model may include non-deterministic situations (i.e. after a given trace, several outputs may occur). For this reason, when dealing with automatic test case generation, approaches in which inputs to be sent to the SUT are computed Work partially supported by the ITEA project openETCS.

on-the-fly are very popular: they permit to stimulate it in a flexible manner depending on observed SUT executions, and depending on the goal of the testing process in terms of behaviors to cover. Such approaches are often qualified as on-line testing.

The other alternative consists in: computing the full input sequence; submitting the sequence to the SUT; storing the output sequence of the SUT during the execution phase; computing a posteriori a verdict by analyzing the trace resulting from the merge of input and output sequences. Such approaches, qualified as off-line testing ones, have several advantages. First, computed input sequences can be stored and later translated into several formats, in particular to become compatible with various home made test benches in different industrial contexts. This allows one to avoid the intertwining (unavoidable in on-line approaches) of the test generation/test execution/verdict computation processes, which may be technically hard to achieve. Second, tests can be replayed as many times as desired which makes off-line methods particularly well-adapted for non-regression testing. Third, by construction, no constraint solving delays can interfere with the test data execution. To sum up, off-line testing eases the deployment of input sequences in the test environment and enables their reuse. However, a particular source of concern about off-line testing is to know at which instants precisely the tester has to send the successive data of the input sequence. Those instants can be identified from the knowledge of a clock cycle or of an hypothesis of an instantaneous reaction in synchronous frameworks (e.g. testing from the clocked data-flow language Lustre in [START_REF] Marre | Test Sequences Generation from LUSTRE Descriptions: GATeL[END_REF] or from Finite State Machines -FSM-in [START_REF] Petrenko | Testing from Partial Deterministic FSM Specifications[END_REF]). In asynchronous systems, the waiting delay between two successive inputs is important because the SUT takes time to compute outputs to be sent, and because sending an input before the output computation is complete, or after it is completed, leads to define different execution traces. Therefore, timed models introducing time delays between communication actions are good candidates to support input sequence generation. Moreover, in order to properly identify the trace observed at the test execution step, one needs a mechanism to know the order of occurrences between inputs and outputs: in fact, measuring delays between outputs permits to reconstruct the full trace of inputs, outputs and delays.

In this paper, we propose an off-line testing approach in a timed modelbased framework. The approach is decoupled in different steps: (a) the coveragebased selection of an input sequence with delays; (b) the execution of the SUT for the input sequence which generates an output sequence with delays as a result. Input and output sequences are then merged to generate a complete execution trace; (c) the verdict computation based on a traversal of the model guided by the execution trace. The first and last steps are conducted off-line with Timed Input Output Symbolic Transition Systems (TIOSTS) for models. TIOSTS are extensions of Input/Output Symbolic Transition Systems (IOSTS) [START_REF] Gaston | Symbolic Execution Techniques for Test Purpose Definition[END_REF] and of Timed Automata (TA) [START_REF] Alur | The Theory of Timed Automata[END_REF], in which both data and time properties are expressed symbolically. Our framework is situated within the context of the tioco conformance relation [START_REF] Bohnenkamp | Timed Testing with TorX[END_REF][START_REF] Krichen | Black-box time systems[END_REF][START_REF] Schmaltz | On Conformance Testing for Timed Systems[END_REF]. Section 2 gives preliminaries about time and data denotation as first order structures. In Section 3, we recall the tioco setting. Then, we present the syntax of TIOSTS and give their semantics as timed traces in Section 4. We show in the same section how to compute these traces using symbolic execution techniques. In Section 5, we introduce our off-line testing algorithm. Section 6 reviews relevant state of the art concerning timed conformance testing.

Data and Time Denotation

We use classical multi-typed first order logic to symbolically denote data and time. A signature Ω is a triple (S, Op, P ) where S is a set of types, Op (resp. P ) is a set of operations (resp. predicates) provided with a profile in S + (resp. S * ). For any set V of variables typed in S, we note T Ω (V ) (resp. P Ω (V )) the set of terms (resp. predicate terms) over V and Ω inductively defined as usual. An Ω-model M = s∈S M s is provided with a function f :

M s1 × • • • × M sn → M s (resp. a predicate p : M s1 × • • • × M sn ) for each f : s 1 • • • s n → s in Op (resp. for each p : s 1 • • • s n in P ).
Substitutions (resp interpretations) are applications from V to T Ω (V ) (resp. M ) preserving types and can be canonically extended to T Ω (V ). 4The set Sen Ω (V ) of all formulas contains the predicate terms (including the truth values and ⊥ denoting resp. the true and false values), the equalities t = t for t, t terms of the same type and all formulas built over the usual connectives ¬, ∨, ∧ and quantifiers ∀x, ∃x with x variable of V .

The satisfaction of a formula ϕ by an interpretation ν : V → M is denoted M |= ν ϕ where M |= ν t = t (resp. M |= ν p(t 1 , . . . , t n ) with t 1 , . . . , t n terms of T Ω (V )) is defined by ν(t) = ν(t ) (resp. (ν(t 1 ), . . . , ν(t n )) ∈ p), and connectives and quantifiers are handled as usual in more complex formulas.

We suppose that Ω contains a particular type time to denote durations. For readability sake, M time is denoted D (for Duration) and is assimilated to the set of positive (or null) real numbers. 5 Op and P contain some classical operations + : time × time → time, -: time × time → time, or predicates <, ≤: time × time, provided by default with their usual meanings. 6 . Variables of type time are called clocks For a set of clocks T , we note Sen time (T ) the set of formulas only containing conjunctions of formulas of the form z ≤ d, d ≤ z, z < d or d < z, where d is a constant and z is in T .

In the sequel, Ω = (S, Op, P ) and M are supposed given.

System Under Test

In order to reason about Systems Under Test, we denote them as Timed Input Output Labeled Transition Systems (TIOLTS) [START_REF] Briones | A Test Generation Framework for quiescent Real-Time Systems[END_REF][START_REF] Krichen | Black-box time systems[END_REF][START_REF] Schmaltz | On Conformance Testing for Timed Systems[END_REF]. TIOLTS are automata whose transitions are labeled either by actions (inputs, outputs) or by delays. For simplicity, the unobservable action τ is not introduced (see [START_REF] Andrade | Abstracting Time and Data for Conformance Testing of Real-Time Systems[END_REF]). Let C be a set of channels. The set of actions over C, denoted Act M (C), is

I M (C) ∪ O M (C) where I M (C) = {c?v | v ∈ M, c ∈ C} denotes the set of inputs and O M (C) = {c!v | v ∈ M, c ∈ C}
denotes the set of outputs. Thus, c?v (resp. c!v) stands for the reception (resp. emission) of v by the SUT on the channel c.

Definition 1 (T IOLT S).

A T IOLT S over C is a triple (Q, q 0 , T r) where Q is a set of states, q 0 ∈ Q is the initial state, and

T r ⊆ Q × (Act M (C) ∪ D) × Q is a set of transitions.
For any tr = (q, a, q ) of T r, source(tr), act(tr), and target(tr) stand respectively for q, a, and q . The set of paths of a TIOLTS A = (Q, q 0 , T r) is the set P ath(A) ⊆ T r * containing the empty sequence ε and all sequences tr 1 . . . tr n such that source(tr 1 ) = q 0 , and for all i < n, target(tr i ) = source(tr i+1 ). 7 Let p be a path of A, the trace of p, denoted as trace(p), is ε if p = ε, trace(p ) if p = p .tr with act(tr) = 0, and act(tr).trace(p ) if p = p .tr with act(tr) = 0. T races(A) is the set of traces of all paths of P ath(A). The set T T races(A) of timed traces of A is the smallest set containing T races(A) and such that:

• for any σ = σ .d.σ in T T races(A), σ .d 1 .d 2 .σ is in T T races(A), • for any σ = σ .d 1 .d 2 .σ in T T races(A), σ .d.σ is in T T races(A),
• for any σ.r in T T races(A) with r in Act M (C)∪(D\{0}), σ is in T T races(A), where d, d 1 and d 2 are any delays of D\{0}

verifying d = d 1 + d 2 .
We introduce a normalization operation whose purpose is to compute a trace in which the occurring delays are the largest possible (by adding all consecutive delays of a trace). Let σ be a trace of (Act M (C) ∪ (D\{0})) * , σ is ε if σ = ε, σ .a if σ = σ .a with a ∈ Act M (C), and σ .(

d 1 + • • • + d n ) if σ = σ .d 1 • • • d n
where for all i ≤ n, d i ∈ D \ {0}, and σ is either ε or terminated by an action in Act M (C).

We naturally define the trace duration as the sum of all delays occurring in a trace. More precisely, for a trace σ, duration(σ) is 0 if σ = ε, duration(σ ) if σ = σ .r with r ∈ Act M (C), and duration(σ

) + d if σ = σ .d with d ∈ D \ {0}.
Definition 2 (SU T ). A SU T over C is a TIOLTS S = (Q, q 0 , T r) over C satisfying the following properties:

• Input enableness: ∀ q ∈ Q, c ∈ C, v ∈ M , there exists (q, c?v, q ) in T r,

• Time elapsing: ∀q ∈ Q s.t. there is no transition of the form (q, c!v, q ) in T r, then there exists (q, d, q ) in T r with d in D\{0}.

Input enableness condition is very classical: it expresses that an SUT cannot refuse an input. Time elapsing condition expresses that the absence of a reaction amounts to observe no reaction during a strictly positive delay.

The conformance relation tioco [START_REF] Bohnenkamp | Timed Testing with TorX[END_REF][START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF][START_REF] Krichen | Black-box time systems[END_REF][START_REF] Schmaltz | On Conformance Testing for Timed Systems[END_REF] defines the correctness of an SUT w.r.t a TIOLTS model.

Definition 3 (tioco).

Let S be an SU T and A a TIOLTS, both defined over C. S conforms to A, denoted S tioco A, if and only if for any σ in T T races(A) and r in O M (C) ∪ (D\{0}) we have:

σ.r ∈ T T races(S) =⇒ σ.r ∈ T T races(A)

In the Introduction, we argued that test data, in off-line testing, is made of a test input sequence to be submitted to the SUT and of a test output sequence produced by the SUT. A natural testing hypothesis expresses that when these two sequences are grouped, they form a trace of the SUT. In order to make the connection between test data and the SUT, we start by introducing some functions to handle traces: the projection function allows us to extract a subtrace, and the merge allows to combine two traces according to delays occurring in them. Formally, for any trace σ, the input projection of σ, denoted σ ↓ I , is:

ε if σ = ε; σ ↓ I if σ = σ .o with o ∈ O M (C), and σ ↓ I .x if σ = σ .x with x ∈ I M (C) ∪ (D\{0}).
Similarly, the output projection of σ, denoted σ ↓ O , is defined by exchanging the roles of inputs and outputs. Let us define the merge operation by induction on the trace structure. For that purpose, let us consider two traces

σ i in (I M (C) ∪ (D\{0})) * and σ o in (O M (C) ∪ (D\{0})) * defined over C. M erge(σ i , σ o ) is defined as follows: -σ o (resp. σ i ) if σ i = ε (resp. σ o = ε), -o.M erge(σ i , σ ) if σ o = o.σ with o ∈ O M (C), -i.M erge(σ , σ o ) if σ i = i.σ with i ∈ I M (C) and σ o = d.σ with d ∈ D\{0}, -with σ i = d i .σ i , d i ∈ D\{0}, and σ o = d o .σ o , d o ∈ D\{0} • d i .M erge(σ i , (d o -d i ).σ o ) if d i < d o • d i .M erge(σ i , σ o ) if d i = d o • d o .M erge((d i -d o ).σ i , σ o ) if d o < d i .
For merging two traces beginning with an input i and then an output o, we choose to prioritize the output o: if from the point of view of the tester, i and o are perceived as occurring at the same time, it is likely that o follows from the previous inputs of the input sequence, not from i. Thus, placing o before i in the merging trace explicits that i cannot be a cause of o.

As already explained, off-line test input sequences are modeled as sequences of inputs and strictly positive delays.

Definition 4 (input sequence

). An input sequence over C is a sequence of

(I M (C) ∪ (D\{0})) * .
Once an input sequence is considered, the test execution phase amounts to play it on S so that it produces an output sequence σ o made of outputs and strictly positive delays. Modeling S as a TIOLTS leads to the following facts:

• there exists a trace σ of T T races(S), such that the input (resp. output) projection of σ corresponds to the submitted input sequence (resp. the output sequence collected when executing the input sequence);

• the duration of the test output sequence is strictly greater than the one of the input sequence. Indeed, when collecting the output sequence, the tester will at least wait a moment after sending the last input to the SUT.

Definition 5 (execution).

Let S be an SUT over C, and let σ i be an input sequence over C.

An execution of σ i on S, is defined as a sequence

σ o of (O M (C) ∪ (D\{0})) * verifying: (1) M erge(σ i , σ o ) ∈ T T races(S) and (2) duration(σ o ) > duration(σ i ).
σ o is called an output sequence of σ i for S and we note σ i ; S σ o .

The condition (2) ensures that the trace M erge(σ i , σ o ) is terminated by either an output or a delay, as verified on the example of Figure

Timed Input Output Transition Systems

TIOSTS are defined over a signature Σ = (C, A, T ) where C is a set of channels, A is a set of variables (whose type is not time) called attribute variables, and T is a set of clocks. The set of symbolic actions Act(Σ) is

I(Σ) ∪ O(Σ) with I(Σ) = {c?x|x ∈ A, c ∈ C} and O(Σ) = {c!t|t ∈ T Ω (A), c ∈ C}.

Definition 6 (TIOSTS).

A TIOSTS over Σ is a triple (Q, q 0 , T r), where Q is a set of states, q 0 ∈ Q is the initial state and T r is a set of transitions of the form (q, φ, ψ, T, act, ρ, q ) where q, q ∈ Q, φ ∈ Sen time (T ), ψ ∈ Sen Ω (A), T ⊆ T , act ∈ Act(Σ), and ρ : A → T Ω (A) is a substitution s.t. x does not occur in ψ if act is of the form c?x.

When firing a transition (q, φ, ψ, T, act, ρ, q ), φ is a formula constraining the delay at which the action act occurs, ψ is a firing condition on attribute variables, ρ assigns new values to attribute variables, and clocks in T are reset. The restriction about the occurrence of the reception variable x in the firing condition ψ is due to the fact that both formulas φ and ψ are evaluated precisely at the reception instant.

Example 1 (Trajectory module of a Flight Management System).

The Trajectory module is embedded in a plane and orchestrates the computation of plane trajectories. Figure 2 depicts its specification: it waits to receive the current location of the aircraft (transition q 0 → q 1 ); it sends a request to access the flight plan in less than 1 time units (transition q 1 → q 2 ); then, either it receives the requested flight plan in less than 2 time units (transition q 2 → q 3 ) or it does not receive it and sends an error message to its environment in less than 3 time units (transition q 2 → q 0 ); after this step, the trajectory module sends a request for parameters (typically, fuel quantity, speed, etc.) related to the state of the plane (transition q 3 → q 4 ), and again either receives them in less than 1 time unit or sends a warning message in less than 2 time units (two transitions q 4 → q 5 ); then, the module sends in less than 1 time unit the location, the flight plan and the parameters to a calculator (transitions q 5 → q 6 ), which replies by sending the new trajectory of the plane in less than 2 time units (transition q 6 → q 7 ) unless it fails to meet the time constraint, in which case the module sends an error message in less than 3 time units; if the calculator succeeds to react on time, the computed navigation commands are transmitted to the environment (transition q 7 → q 0 ) in a total of less than 9 time units. Executions of TIOSTS transitions are called runs and modeled as TIOLTS transitions whose states are called snapshots: Definition 7 (runs of transitions). Let G = (Q, q 0 , T r) be a T IOST S over Σ. The set Snp M (G) of snapshots of G is the set Q × D × M A∪T . For any tr = (q, φ, ψ, T, act, ρ, q ) ∈ T r, the set of runs of tr is the set Run(tr) ⊆ Snp M (G) × Act M (C) × Snp M (G) s.t. ((q, T , ν), act M , (q , T , ν )) ∈ Run(tr) iff there exist d ∈ D and ν i : A ∪ T → M satisfying:

• T = T + d, • for all w ∈ T , ν i (w) = ν(w) + d, • if act = c!t then for all x ∈ A, ν i (x) = ν(x),
• if act = c?x then for all y ∈ A \ {x}, ν i (y) = ν(y), such that we have:

act M = ν i (act), ∀x ∈ A, ν (x) = ν i (ρ(x)), ∀w ∈ T, ν (w) = 0, ∀w ∈ (T \ T), ν (w) = ν i (w), M |= νi φ and M |= νi ψ.
Based on runs of transitions, we associate a TIOLTS to a TIOSTS: Definition 8 (TIOLTS associated to a TIOSTS). The TIOLTS over C associated to G, denoted LT S G = (Snp M (G) ∪ {init, q δ }, init, T r ), is defined as follows: init, q δ are two distinct states not belonging to Snp M (G) and T r is the smallest subset of

(Snp M (G) ∪ {init, q δ }) × (Act M (C) ∪ D) × (Snp M (G) ∪ {q δ }) s.t.
Initialization: for any ((q 0 , 0, ν 0 ), act M , (q, T , ν)) ∈ Run(tr) with tr ∈ T r and ∀w ∈ T, ν 0 (w) = 0, • if 0 < T , (init, T , (q 0 , T , ν 0 )) and ((q 0 , T , ν 0 ), act M , (q, T , ν)) are in T r ,

• else (T = 0) ((q 0 , 0, ν 0 ), act M , (q, 0, ν)) is in T r , Runs: for ((q, T , ν), act M , (q , T , ν )) ∈ Run(tr) with tr ∈ T r and q = q 0 , • if T < T , ((q, T , ν), T -T , (q, T , ν)), ((q, T , ν), act M , (q , T , ν )) are in T r ,

• else (T = T ) ((q, T , ν), act M , (q , T , ν )) is in T r , Quiescence: let snp in Snp M (G) ∪ {init} be a snapshot s.t. there does not exist (snp, act M , snp ) ∈ T r with act M ∈ O M (C) ∪ (D\{0}), then (snp, d, q δ ) ∈ T r for any d ∈ D\{0}.
Initialization transitions are introduced to consider any possible interpretation of attribute variables at the beginning of executions (clocks are set to 0), Runs transitions naturally correspond to the execution of TIOSTS transitions, and Quiescence transitions state that if no reaction (output or delay transitions) is specified at a given state, then waiting for any delay from this state is possible. We note T T races(G) for T T races(LT S G ).

In the sequel, we will reason about traces of T T races(G) by using symbolic execution techniques. They consist in: executing the TIOSTS for symbolic values rather than numerical ones, and computing constraints on those values for all possible TIOSTS executions. In order to represent symbolic values, we suppose that a set of fresh variables F = s∈S F s is given. Symbolic states are structures used to store pieces of information concerning an execution: Definition 9 (symbolic state). A symbolic state for G is a tuple (q, θ, π, ϑ, λ) where q ∈ Q, θ ∈ Sen time (F time ), π ∈ Sen Ω (F ), ϑ ∈ T Ω (F time ) and λ : A ∪ T → T Ω (F ) is an application preserving types.

We note S the set of all symbolic states over F .

For a symbolic state η = (q, θ, π, ϑ, λ), q denotes the state reached after an execution leading to η, θ is a constraint on symbolic delay values called time path condition, π is a constraint on symbolic data values called data path condition, ϑ denotes the duration from the beginning of the execution leading to η, and λ denotes terms over symbolic variables in F that are assigned to variables of A.

In the sequel, Σ F stands for (F, C). Moreover for any symbolic state η = (q, θ, π, ϑ, λ), q(η), θ(η),π(η), ϑ(η) and λ(η) stand resp. for q, θ, π, ϑ and λ. For an application λ : A ∪ T → T Ω (F ), we extend it in a canonical way to T Ω (A ∪ T ), Sen Ω (A∪T ) and Act(Σ). All these extensions are also simply denoted by λ. The symbolic execution of a TIOSTS is based on symbolic executions of transitions: Definition 10 (symbolic execution of transitions). Let G = (Q, q 0 , T r) be a T IOST S over Σ and tr = (q, φ, ψ, T, act, ρ, q ) be in T r. A symbolic execution of tr from η in S is st = (η, act F , η ) ∈ S × Act(Σ F ) × S such that q(η ) = q , ϑ(η ) = ϑ(η) + z where z ∈ F time is a new fresh variable, and there exists

λ i : A ∪ T → T Ω (F ) satisfying: • if act ∈ O(Σ), then that for all x ∈ A, λ i (x) = λ(x),
• if act ∈ I(Σ) of the form c?y then λ i (y) is a fresh variable of F and for all x ∈ A \ {y}, λ i (x) = λ(x),

• for all w ∈ T we have λ i (w) = λ(w) + z, such that act F = λ i (act), for all x ∈ A, λ(η

)(x) = λ i (ρ(x)), for all w ∈ (T \ T), λ(η )(w) = λ i (w), for all w ∈ T, λ(η )(w) = 0, Finally π(η ) = π(η) ∧ λ i (ψ) and θ(η ) = θ(η) ∧ λ i (φ).
The variable z is called the delay of st and is denoted delay(st). source(st), act(st) and target(st) stand respectively for η, act F and η . In the sequel, for any symbolic transition st = (η, act F , η ), we note F resh(st) = {delay(st)} if act ∈ O(Σ) and F resh(st) = {delay(st), λ i (y)} if act = c?y. The symbolic execution tree associated to the TIOSTS is then defined as follows:

Definition 11 (symbolic execution of a TIOSTS). A symbolic execution of G = (Q, q 0 , T r) is a couple SE(G) = (Init, ST ) where:

• Init = (q 0 , , , 0, λ 0 ) is such that ∀x ∈ T, λ 0 (x) = 0 and for all distinct variables x, y in A, λ 0 (x) and λ 0 (y) are distinct variables of F , • ST is the set of all symbolic executions st of tr in T r from η ∈ S with q(η) = source(tr) and F resh(st) ∩ λ 0 (A) = ∅. Moreover for any two distinct st 1 , st 2 ∈ ST , F resh(st 1 ) ∩ F resh(st 2 ) = ∅.

Example 2 (Symbolic execution). Figure 3 depicts the symbolic execution of the Trajectory module of Example 1. For the sake of clarity: only one path of the tree is shown, representing a complete cycle of the Trajectory module, transitions deviating from this path are cut; we show the delay of the transition together with its symbolic action; and, only the information associated with symbolic state η 1 is detailed -note that values of clocks are actually summations of delays (e.g. f Clock 1 represents the summation 0 + z 1 ).

In order to deal with quiescence, we complete symbolic executions by new transitions. Contrarily to TIOLTS, transitions of TIOSTS carry actions that are necessarily inputs or outputs (not delays). For this reason, we artificially introduce a new symbol δ! denoting the absence of reactions. • Time based quiescence: Let θ δ (η) be if React(η) = ∅ and let θ δ (η) be st∈React(η) ∀delay(st).¬(θ(target(st))) otherwise. Then, (η, δ!, η t δ ) ∈ ∆ST with η t δ = (q δ , θ(η) ∧ θ δ (η), π(η), ϑ(η) + z, λ(η)) with z is a new variable in F time .

• Data based quiescence: Let π δ (η) be if React(η) = ∅ and let π δ (η) be st∈React(η) ¬π(target(st)) otherwise. Then, (η, δ!, η d δ ) ∈ ∆ST with η d δ = (q δ , θ(η), π(η) ∧ π δ (η), ϑ(η) + z, λ(η)) with z is a new variable in F time .

Time based quiescence transitions can be executed only if no transition labeled by an output can be executed anymore due to unsatisfiable time constraints. By noting that delay(st) is the symbolic delay associated wit the transition st, θ δ (η) precisely states that for all output transitions st of source η, whatever the delay is, the time path condition (θ(target(st))) to fire st cannot be satisfied. Similarly, Data based quiescence transitions can be executed only if no transition labelled by an output can be executed anymore due to unsatisfiable data constraints.

Example 3 (Quiescence enrichment).

The Trajectory module example takes all possible deadlock situations into account. This is normal, since in an flight management system, we do not want to have any of those situations. For illustration purposes, let us consider Init, since there is no output transition leaving from it, a Data based quiescence is detected, and as according to Definition 12, the transition (Init, δ!, η d δ ) is added to the tree, representing the fact that the module can remain silent until it receives a location from the environment. If we consider η 1 , let us examine if we can detect a Time based quiescence. That is, let us examine the formula ∀z 1 .¬(θ 1 ), where θ 1 = f Clock 1 < 1. Since f Clock 1 = 0 + z 1 , there is no way that for all z 1 , z 1 ≥ 1 is true. Thus, no Time based quiescence is added to the tree. SE(G) δ characterizes in an intentional way the set of all timed traces of the TIOLTS associated to G: we define paths of SE(G) δ as finite sequences st 1 • • • st n of transitions of ST , such that source(st 1 ) = Init and for every i < n, we have target(st i ) = source(st i+1 ). For any finite path p = st 1 • • • st n , target(p) is Init if n = 0 and target(st n ) otherwise. We note P ath(SE(G) δ ) the set of all such paths. For a path p, we note Seq(p) the sequence defined as ε if p = ε, Seq(p ).delay(st) if p is of the form p .st with act(st) = δ! and Seq(p ).delay(st).act(st) if p is of the form p .st with act(st) = δ!. The set T T races(p) is defined as {σ|∃ν.(M |= ν θ(target(p)) ∧ π(target(p)) ∧ σ = ν(Seq(p)))}. 8 We note T T races(SE(G) δ ) the set p∈P ath(SE(G) δ ) T T races(p).

Off-line Testing Algorithms

We present our algorithms w.r.t. the input sequence selection, the test execution, and the verdict computation.

Input sequence selection. We propose to extract input sequences, as introduced in Definition 4, from SE(G) δ . Following our previous works [START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF][START_REF] Gaston | Symbolic Execution Techniques for Test Purpose Definition[END_REF], we propose to use paths of SE(G) δ as test purposes, that is, we build input sequences corresponding to traces of a selected path. Given a test purpose p in P ath(SE(G) δ ), an input sequence is built by applying the input projection on a trace chosen in T T races(p). Indeed, such input sequences are clearly good candidates to put the SU T S in a configuration where S can reach the test purpose. Therefore, we introduce the set IS(p) = {σ ↓ I | σ ∈ T T races(p)} of input sequences of p. We can capture the set IS(p) by simply building the corresponding normalized traces and by highlighting the interpretations which satisfy the constraints defining the target state of p:

{ν(Seq(p)) ↓ I | ν |= θ(target(p)) ∧ π(target(p))}
Thus, defining a normalized input sequence for p comes to exhibit an interpretation ν : F → M that satisfies both the time and data path conditions of the target of p by constraint solving techniques, to compute ν(Seq(p)), and finally "forget" output in the result thanks to the ↓ I operator. We suppose that an SU T S, a test purpose p and an input sequence σ p ↓ I are given (σ p is thus a timed trace of p, normalized or not).

Test execution. As discussed in Section 3, the test execution is to submit σ p ↓ I to S, which in turn sends an output sequence σ o , such that σ p ↓ I ; S σ o . We note σ S = M erge(σ p ↓ I , σ o ). Recall that, due to potential non determinism of G, even in the case S tioco G, we may have σ S = σ p . Verdict computation. Our algorithm takes as inputs three arguments, SE(G) δ , p and σ S , and computes verdicts concerning the correctness of S assessment and concerning the coverage of p by σ S . This algorithm can be seen as an off-line version of the one defined in [START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF]. We begin by introducing some intermediate definitions that are needed in the algorithm. A context is a mathematical structure denoting a path of SE(G) δ = (Init, ST ) potentially covered by a trace, together with additional identification constraints induced by the trace. Formally, a context is a tuple (η, f t , f d , d) where: η ∈ S denotes the target state of the potentially covered path; f t ∈ Sen T ime (F time ) expresses identification constraints between time variables of F and numerical delays occurring in the trace; f d ∈ Sen Ω (F ) expresses identification constraints between data variables and values emitted and received in the trace; and finally, d is a numerical delay that identifies how much time has elapsed in the given context. Intuitively, when time elapses, if there is no modification of state, then the value d is simply increased, else, the value d is reset to 0. In the sequel, state((η, f t , f d , d)) names the state η. Since there may be more than one path which is covered by a trace, we manipulate sets of contexts. We introduce the function N ext(a, SC), which computes the set of all contexts that can be reached from a given set of contexts SC, when an action occurs or a delay elapses, i. The general idea of the algorithm is to read one by one the elements of the trace σ S , and to compute either the next set of contexts or to emit a verdict. Let us suppose that σ S can be written as σ pref .a.σ suf where a is an action or a delay. SC(a) is a notation grouping the set of contexts SC reached after reading the beginning σ pref .a of the trace and the last analyzed element a. At the initialization step, when no element of σ S has been analyzed, then we use the symbol , that is SC( ). The algorithm is then given as a set of rules of the form: SC(a) σ suf Result cond σ suf is the remaining trace to be analyzed with respect to the first analyses stored in SC(a), to SE(G) δ , and to p; cond is a set of conditions that has to be satisfied so that the rule can be applied; and Result is either a verdict or of the form SC (a ) σ suf . Moreover, if σ suf = ε then Result is necessarily a verdict since the initial trace σ S is fully analyzed. If Result is SC (a ) σ suf , then σ suf can be written as a .σ suf . We will access respectively to a and σ suf from σ suf by using the usual notations head(σ suf ) and tail(σ suf ).

Rule 0 corresponds to the initialization phase: the set of contexts contains only one context stating that we begin at the symbolic state Init, there are no constraints identified yet, and the associated delay is 0. Rule 1 is applied to compute a new set of contexts. This is done as long as SC is not empty and there are still elements of the trace to read. There are five verdicts: F AIL is emitted when the trace denotes an incorrect behavior (Rule 2); P ASS is emitted when the trace denotes a correct behaviors, and the test purpose is the only path covered (Rule 3); W EAK P ASS is emitted when the trace denotes a correct behavior, the test purpose is covered but there exists at least one other path covered (Rule 4); IN CON C r is emitted when the trace denotes a correct behavior, a path is covered but not the test purpose (Rule 5); IN CON C i is emitted when the trace is not included in SE(G) δ due to input under-specification (Rule 6). In contrast with algorithms in [START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF][START_REF] Gaston | Symbolic Execution Techniques for Test Purpose Definition[END_REF], there are two kinds of inconclusive verdicts.

IN CON C r corresponds to the classical one, while IN CON C i is produced when σ S is of the form σ pref .a.σ suf , where σ pref is in SE(G) δ while σ pref .a with a ∈ I M (C) is not. This situation does not occur in on-line testing algorithms, because they are in charge of stimulating the SUT so that it strictly follows the test purpose, and emits a verdict as soon as the test purpose cannot be covered anymore. On the contrary, unless σ S can be decomposed as σ pref .a.σ suf , where σ pref is a specified timed trace and σ pref .a is not (in which case either F AIL or IN CON C i depending on the nature of a), all actions of σ S will be analyzed even though the emission of P ASS is not possible anymore. This choice is made in order to always emit F AIL for a trace revealing a non conformance, even if we may be sure (several steps before) that P ASS can not be emitted anymore.

in [START_REF] Bohnenkamp | Timed Testing with TorX[END_REF] have defined a pure on-the-fly testing algorithm. Without any preprocessing on the model, at each moment, the algorithm computes on-the-fly a random input and its corresponding submission delay from the model and checks outputs and their timing against the model. This is reiterated until a verdict is emitted.

In [START_REF] Bertrand | Off-line test selection with test purposes for non-deterministic timed automata[END_REF], authors model the testing activity with the help of test cases which are deterministic timed automata with inputs and outputs, whose states are labeled by verdicts. These test cases are derived from a given test purpose and result from some approximate determinisation mechanisms preserving the tioco conformance relation. Such a design of test cases tends to reduce choice points at runtime: however, decisions have still to be made when running test cases on SUT, for example, concerning the choice between waiting for a delay or sending a data to the SUT. So [START_REF] Bertrand | Off-line test selection with test purposes for non-deterministic timed automata[END_REF] may be viewed as a mixed approach, off-line for the selection, by converting a test purpose as a test case, on-line for guiding the progress in the test case during the execution. Recently, authors of [START_REF] Andrade | Abstracting Time and Data for Conformance Testing of Real-Time Systems[END_REF][START_REF] Bannour | Eliciting unitary constraints from timed Sequence Diagram with symbolic techniques: application to testing[END_REF][START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF][START_REF] Von Styp | A conformance testing relation for symbolic timed automata[END_REF] have defined seemingly different reference models where both time and data are represented symbolically as extensions to TA or/and input output symbolic transition systems (IOSTS) [START_REF] Gaston | Symbolic Execution Techniques for Test Purpose Definition[END_REF][START_REF] Rusu | An Approach to Symbolic Test Generation[END_REF], still based on tioco. In addition, approaches [START_REF] Andrade | Abstracting Time and Data for Conformance Testing of Real-Time Systems[END_REF][START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF] have suggested on-line testing algorithms guided by a test purpose: in [START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF], symbolic execution paths are selected as test purposes while the work in [START_REF] Andrade | Abstracting Time and Data for Conformance Testing of Real-Time Systems[END_REF] is conducted in the spirit of [START_REF] Bertrand | Off-line test selection with test purposes for non-deterministic timed automata[END_REF]. To our knowledge, we are the first to propose in the context of the tioco conformance relation a framework where test inputs are presented statically, without any further processing to be done, while remaining executable and usable for verdict computation.

Conclusion

We have proposed an off-line testing approach based on the tioco conformance relation and on TIOSTS models which handle both data and time symbolically. The approach includes three steps: (1) first, test input sequences are extracted from a TIOSTS; for this, traces are extracted from paths of the symbolic execution tree by using solving constraints and projection techniques; (2) test executions produce output sequences that are merged with input sequences to form input output traces; (3) resulting traces are analyzed in order to provide verdicts. We highlight a verdict, specific to our off-line approach: the verdict IN CON C i , stating that an input can become unspecified in the context of the test execution even if it was a specified input in the context of the test selection.

Our approach has been implemented using the symbolic execution tool Diversity. Diversity is an extension of the tool AGATHA [START_REF] Rapin | Behavioural unfolding of formal specifications based on communicating automata[END_REF] that integrates several sat-solvers and can analyze several languages, in particular TIOSTS or UML sequence diagrams extended with time constraints [START_REF] Bannour | Eliciting unitary constraints from timed Sequence Diagram with symbolic techniques: application to testing[END_REF][START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF]. 9 Concerning data, our implementation handles booleans, presburger integers, and could be extended to any decidable data theory as in [START_REF] Gaston | Symbolic Execution Techniques for Test Purpose Definition[END_REF]. Until now, we have not investigaged zonebased techniques usually undertaken with timed automata, essentially because run-time efficiency is not of primary importance in an off-line framework. We are investigating techniques to reduce the occurrence of inconclusive verdicts. As several reactions are possible after a given trace, the submission of an input sequence to SUT may result in a trace which runs outside the test purpose without questioning conformance. To control non-determinism as much as possible, we are studying under which hypotheses we can over constrain the input sequence computation in order to force a correct SUT to follow a given path.

Fig. 1 :

 1 Fig. 1: Example of merging two test traces. Timed Input Output Symbolic Transition Systems (TIOSTS) are models where data and time are symbolically specified. They are well-accepted concise representations of TIOLTS: symbolic data allow one to characterize internal states, to express firing conditions of transitions and to denote exchanged messages, while real-time properties are handled with constraints and resets on clock variables. Since tioco defines conformance of an SUT w.r.t. a TIOLTS specification, TIOSTS model semantics (Definition 8) is given in the form of TIOLTS.

Fig. 2 :

 2 Fig. 2: TIOSTS for the Trajectory module.

Definition 12 (

 12 quiescence enrichment). Let SE(G) = (Init, ST ) be a symbolic execution. For all η ∈ S let us note React(η) the set of st in ST with Init : (q0, θ0, π0, ϑ0, λ0) η1 : (q1, θ0, π0, ϑ1, λ1) η2 : (q2, θ1, π0, ϑ2, λ2) η3 : (q0, θ2, π0, ϑ3, λ3) η5 : (q1, θ2, π0, ϑ5, λ5) z4•location?loc2 z2•error!f T imeout0 η4 : (q3, θ3, π0, ϑ4, λ4) η6 : (q4, θ4, π0, ϑ6, λ6) η7 : (q5, θ5, π0, ϑ7, λ7) z6•notif !cP arams0 η8 : (q5, θ6, π0, ϑ8, λ8) η9 : (q6, θ7, π0, ϑ9, λ9) η10 : (q0, θ8, π0, ϑ10, λ10) z9•error!cT imeout0 η11 : (q7, θ9, π0, ϑ11, λ11) η12 : (q0, θ10, π0, ϑ12, λ12) z11•nCmd!cmds1 z10•calc?cmds1 z8•calc!data1 z7•param?dP arams1 z5•param!askP0 z3•plan?f P lan1 z1•plan!askF p0 z0•location?loc1 η 12 : (q 0 , θ 10 , π 0 , ϑ 12 , λ 12 ) θ 10 : ∧ f Clock 1 <1 ∧ f Clock 4 <2 ∧ dClock 5 <1 ∧dClock 7 <1 ∧ cClock 8 <1 ∧ cClock 9 <2 ∧aClock 11 <9 π 0 : ϑ 12 : z 0 + z 1 + z 3 + z 5 + z 7 + z 8 + z 10 + z 11 λ 13 : loc ← loc 1 , askF p ← askF p 0 , f P lan ← f P lan 1 , . . .

Fig. 3 :

 3 Fig. 3: Symbolic execution for the Trajectory module example. source(st) = η and act(st) ∈ O(Σ F ). The quiescence enrichment of SE(G) is the couple SE(G δ ) = (Init, ST ∪ ∆ST ) where for all η ∈ S: • Time based quiescence: Let θ δ (η) be if React(η) = ∅ and let θ δ (η) be

  e. a ∈ Act M (C) ∪ (D \ {0}): Case a ∈ Act M (C) of the form c t with ∈ {?, !}: if there exists (η, f t , f d , d) ∈ SC, and a symbolic transition st= (η, c u, η ) in ST , then: (η , f t ∧ d = delay(st), f d ∧ (t = u), 0) ∈ N ext(a, SC) provided that both f t ∧ d = delay(st) ∧ θ(η ) and f d ∧ π(η ) are satisfiable. Case a ∈ D \ {0}: if there exists (η, f t , f d , d) ∈ SC,and a symbolic transition st in ST with source(st) = η, then: (η, f t ∧ ∃delay(st).(delay(st) ≥ d + a ∧ θ(target(st))), f d , d + a) ∈ N ext(a, SC) provided that f t ∧ ∃delay(st).(delay(st) ≥ d + a ∧ θ(target(st))) ∧ θ(η) is satisfiable.

Rule 2 :Rule 3 :Rule 4 :Rule 6 :

 2346 Rule 0: Initialization {(Init, , , 0)}( ) σ S Rule 1: An action or a delay is read from the trace, SC is not empty. SC(a) σ N ext(head(σ), SC)(head(σ)) tail(σ) SC = ∅, σ = An unspecified output o or delay d is read from the trace. SC(a) σ F AIL SC = ∅; a ∈ OM (C) ∪ D \ {0} The read action permits to cover the test purpose, and no other paths. SC(a) σ P ASS σ = ; ∀ct ∈ SC, state(ct) = target(p); SC = ∅ The read action permits to cover the test purpose, and at least one other path. SC(a) σ W eak P ASS σ = ; ∃ct ∈ SC, state(ct) = target(p); ∃ct ∈ SC, state(ct ) = target(p); SC = ∅ Rule 5: Some paths are covered but not the test purpose. SC(a) σ IN CON Cr σ = ; ∀ct ∈ SC, state(ct) = target(p); SC = ∅ An unspecified input i is read. SC(a) σ IN CON Ci SC = ∅; a ∈ IM (C)

  1. Moreover, let us point out that due to non-determinism, there can exist two distinct traces σ o and σ o such that σ i ; S σ o and σ i ; S σ o .

	test input sequence 4•c?a•23•e?x•39•c?w	SUT	test output sequence 12•c!b•31•e!y•65•c!m
	Corresponding timeline
	4•c?a•8•c!b•15•e?x•16•e!y•23•c?w•42•c!m

The set of applications from A to B is denoted as B A .

In practice, any set of values used in a constraint solver for approaching real numbers.

For simplicity, +, < . . . are also denoted by +, <.

A * is the set of words on A with ε as the empty word and "." as the concatenation law.

An interpretation ν can be extended to sequences as follows: ν(Seq(p)) = ε if p = ε, ν(Seq(p)) = ν(ω).ν(a) if Seq(p) = ω.a with a ∈ Act(ΣF ) and ν(Seq(p)) = ν(ω).ν(d) if Seq(p) = ω.d with d ∈ TΩ(F )time.

e.g. CVC3 http : //www.cs.nyu.edu/acsys/cvc3/

Example 4. Let us apply our rule-based algorithm to the Trajectory module example. Let us suppose that there is a mapping between messages and integers. Then, we choose the path of Figure 3 leading to η 13 , representing a complete loop for the module, i.e., the path p:

Thus, the tester chooses the appropriate values and performs the input projection of the trace, obtaining σ p ↓ I : 0.1 location?4 2.8 plan?5 1.8 param?2 1 calc? What is interesting to notice in Figure 4 is that, if use an on-line test purposeguided algorithm as in [START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF], we emit the verdict IN CON C as soon as we find the delay 2.1 of output error!6 ((d) in the figure). One advantage of this offline algorithm is that we can emit better verdicts (less IN CON C) since we are analyzing the entire trace.

Related Work

Model-based conformance testing with tioco was addressed in [START_REF] Bertrand | Off-line test selection with test purposes for non-deterministic timed automata[END_REF][START_REF] Bohnenkamp | Timed Testing with TorX[END_REF][START_REF] Escobedo | Timed Conformance Testing for Orchestrated Service Discovery[END_REF] where models are essentially timed automata (TA) [START_REF] Alur | The Theory of Timed Automata[END_REF] (without symbolic data). Authors


Magri

Extending Coverage Criteria by Evaluating Their Robustness to Code Structure Changes

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Extending Coverage Criteria by Evaluating their

Robustness to Code Structure Changes Angelo Gargantini, Marco Guarnieri, and Eros Magri hipF di sngF dell9snformzione e wetodi wtemtiiD niversità di fergmoD stly {angelo.gargantini,marco.guarnieri,eros.magri}@unibg.it

Abstract. gode overge is usully used s mesurement of testing qulity nd s dequy riterionF nfortuntelyD ode overge is very sensitive to modi(tions of the ode strutureD ndD thereforeD the sme test suite n hieve di'erent degrees of overge on the sme progrm written in two synttilly di'erent wysF por this resonD ode overge n provide the tester with misleding informtionF sn order to understnd how testing riterion is 'eted y ode struE ture modi(tionsD we introdue wy to mesure the sensitivity of overge to ode hngesF e formlize the modi(tions of the ode struture using semnti preserving odeEtoEode trnsformtions nd we propose frmework to evlute overge roustness to these trnsE formtionsD extending tul existing overge riteriF his llows us to de(ne whih progrms nd whih test suites n e onsidered roust with respet to ertin set of trnsformtionsF e n identify when the otined overge is frgile nd we extend the onept of overge riterion y introduing n index tht mesures the frgility of the overge of given test suiteF e show how to ompute the frgility index nd we evidene tht lso wellEwritten industril ode nd relisti test suites n e frgileF woreoverD we suggest how to del with this kind of testing frgilityF 1 Introduction

The notion of code coverage and testing criteria dates back to the early sixties [14,19]. Although, as Dijkstra claimed in 1972 [6], program testing can be used to show the presence of bugs, but never their absence , the initial research focused on nding ideal testing criteria, i.e. those capable, under certain assumptions, of demonstrating the absence of errors in programs by testing them [10].

Researchers soon realized that nding such ideal testing criteria was impractical if not impossible [23] and the community started to introduce, compare, and study testing criteria, which are not ideal but they have proved to be useful to measure the quality of testing and to nd faults in programs. However, there still exists some skepticism around the actual signicance of coverage criteria. It is well known that some faults may be completely missed by test suites adequate to some coverage criteria (for instance statement coverage cannot discover omission faults) and that testing criteria are very sensitive to the structure and to the syntax of the code, regardless its actual behavior. Rajan et al. [17] show that the MCDC, required by FAA for software on commercial airplanes, and often considered a very tough criterion to achieve, can be easily cheated by simple folding/unfolding of conditions inside guards.

Despite their weakness, coverage criteria give an immediate and easy to compute (at least for simple criteria) feedback about the quality of the testing activity. Once a test suite has been developed or built, one wants to know which parts of the code are exercised and which are not, and this information can be simply obtained by running the code with the tests. Coverage is often used as acceptance threshold: if a test suite achieves a given coverage, it is considered adequate, and the tested software accepted as good. For this reason, reaching a given level of coverage becomes a critical factor during the testing activity.

We can state that the coverage data are easily obtained and are widely used as acceptance measure, but have a questionable signicance. In this paper we try to augment the information one can retrieve from the coverage data by considering also the structure of the code and its possible transformations.

There are two main scenarios in which it is important knowing how the coverage oered by a test suite behaves with respect to the changes in the code structure.

A. The code has been transformed in the past before being tested and the coverage may depend on the transformations applied. In this way, testing criteria can easily be cheated, and hence an additional measure of the coverage fragility helps in identifying well-tested classes from poorly tested ones.

B. The code structure will change in the future without changing the semantics of the program by applying some refactoring rules, by some automatic transformations, or by introducing particular patterns. This may inuence the coverage after the application of these transformations. In this context, the tester would like to know if the level of coverage provided by the test suite will be preserved, i.e., if the coverage is robust w.r.t. future changes.

In this paper we make use of code transformations that preserve code functional behavior to model code changes. We formally dene when a test suite achieves a fragile vs robust coverage. Roughly speaking, a fragile coverage depends on the structure and syntax of the code, and the test suite would not achieve the same level of coverage on the transformed code. A robust coverage and a robust test suite do not suer from modications of the code structure.

We introduce a measure of fragility by extending the usual coverage criteria.

In Section 2 we present some related work on testing, coverage, and code transformations. Section 3 presents the theoretical framework in which our work will be integrated and contains some examples of useful code transformations.

In Section 4 we show the limitations of actual coverage criteria in terms of their fragility with respect to code changes by giving several examples in which the obtained coverage is fragile. We introduce and formally dene the concept of coverage robustness and several measure of coverage fragility. Section 5 reports some experiments. In Section 7 we present our conclusions. (2) a canonical way of structuring code so that such conditions do not occur in the rst place. Their approach dier from ours, since we propose a framework able to evaluate existing coverage criteria with respect to their robustness to code structure and syntax changes and to extend them by computing some information about their robustness/fragility. No change of the existing code is required in our approach either.

So far, the main solution in the literature to overcome coverage criteria weaknesses has been trying to introduce more powerful and tough testing criteria. For instance, testing criteria that consider also the information ow can be introduced. In [18], the authors dene a family of program test data selection criteria derived from data ow analysis techniques similar to those used in compiler optimization. We believe that introducing complex coverage criteria may be avoided if code transformations are taken into account as proposed in our approach.

Testing criteria are very sensitive to code structure also when used for test Transformations and code coverage is studied by Weissleder [22]. In this case the transformation is used to obtain information of the coverage over the original code from the information about the coverage over the transformed code. The goal is to nd a transformation such that if a test suite achieves the coverage C 1 over the transformed code, than the same test suite achieves the coverage C 2 over the original code. In this case C 1 simulates the coverage C 2 .

The fact that transformations can disrupt coverage is also tackled by Kirner.

In [12], he addresses the challenge of ensuring that the structural code coverage achieved for a program P is preserved when P is transformed. If the code transformation fullls some formal properties, than it preserves also the coverage. The considered code transformations allow to obtain machine level code from higher level programs. He also identies three classes of transformations:

1. the ones that change the reachability of program elements, 2. the ones that add new paths to the program and 3. the ones that preserve the coverage. His work is more focused on preserving structural code coverage into compilers and code generators, whereas our work is more focused on measuring the impact of transformations of the code structure on the coverage.

Code transformations

There exist several, theoretically innite, programs which have the same behaviour but have dierent code structure and thus can achieve dierent results in terms of coverage for a particular criterion. So how, given a program p ∈ P , can we obtain new programs with the same behaviour of p? We can do this by means of code-to-code transformations, which are functions that take as input a program p and return another program p . Formally, a transformation t is a function P -→ P , where P is the set of all the programs.

However not all the transformations produce a transformed program with the same behaviour of the original program. This kind of transformations are called Semantic Preserving Transformations (SPT). A SPT [2] is a code-to-code transformation that modies the syntax of the program to which it is applied, without changing its semantics. Thus given a SPT t ∈ T , where T is the set of all the SPTs, and a program p ∈ P , p and t(p) must have the same behaviour.

In the following of the paper we will consider only SPTs and, thus, we will call them just transformations.

In the following we present ve SPTs which we will use in the paper as a case study. Each transformation is identied by using a transformation schema, composed by two snippets of code. The rst one, called input pattern, denes on which snippets of code the transformation can be applied. The second one, called output pattern, denes how the transformed piece of code will look like.

Several new transformations can be obtained by combining already dened transformations. Given a sequence of transformations T , we dene the transformation t seqT as the application of the transformations in T in sequence, i.e. t seqT = t 1 • . . . • t n where t seqT , t 1 , . . . , t n ∈ T . Given a transformation t, we dene the transformation t as the iterative application of t until the program is no longer modied by t. Given a certain transformation t, we can dene the inverse transformation t -1 by exchanging the input pattern and the output pattern.

In this paper, we consider the following transformations.

Externalized Complex Flag. All the examples show that several programs with the same behaviour can achieve the same value of coverage with dierent eort from a testing point of view, i.e. the number of test cases in the test suite, only because they have a dierent structure. This is valid for all the structural coverage criteria.

Coverage fragility and robustness

First of all, we want to formalize the sensitivity of the coverage obtained by testing a program P with a test suite, with respect to a set of possible transformations of P .

Denition 2. Fragility. Given a program p ∈ P , a coverage criterion C and a set of transformations T , we say that a test suite ts fragilely covers p, if there exists a transformation t ∈ T such that C(p, ts) > C(t(p), ts).

Fragilely covered programs can be modied by some transformation t ∈ T in a way that, also if the behaviour of the program remains the same, the coverage provided by ts on the transformed program t(p) diminishes with respect to the coverage on the original program p.

If a test suite fragilely covers the program under test, the condence in the measurement of the coverage is reduced because the possible high level of coverage may be due to the structure of the code. It may happen that the developer has used in the past a particular pattern that has increased the coverage but if the code were written in another way then the test suite would be not as good in terms of achieved coverage. Fragile coverage is not robust to transformations of the code that may be performed in the future either, such as refactoring techniques or compiler optimizations. This is a problem because, usually, after a SPT is applied, the test suite is not updated by the developer because he/she does not feel the need of new tests, and thus the old test suite can achieve lower coverage on the resulting code. For this reason, fragilely covered programs may need more testing, regardless the level of coverage achieved so far.

In order to reduce the fragility of a test suite, new tests must be added.

Generally, the new tests are built looking at the transformed program and then added to the original test suite. However, using the transformed program to derive a completely new test suite to be applied also to the original program can cause an unexpected loss of coverage, as proved by the following theorem.

Theorem 1. Let C be a coverage criterion, ts and ts be two test suites, generated respectively for p and for t(p), such that ts ts , ts ts, and t ∈ T be a transformation, C(t(p), ts ) > C(t(p), ts) does not imply C(p, ts ) > C(p, ts). C(t ecf (p), ts ) > C(t ecf (p), ts). Moreover, ts ts , ts ts is true. However, the coverage of ts over p dimishes, since C(p, ts ) = 0.5 whereas C(p, ts) = 1.0.

Theorem 1 states that, given a program p fragilely covered by a test suite ts and a transformation t, if we want to achieve a better coverage than the one obtained using the test suite ts on the program p we cannot simply generate a new test suite ts on the program t(p), because ts , also if increases the coverage on t(p) with respect to ts, maybe does not increase the coverage achieved on p.

Note that transformations allowing testers to obtain programs from which tests can be generated more easily are also called testability transformations [11].

Theorem 1 states that the use of testability transformations should be carefully considered since they may not increase the coverage obtained on the original program, even though the coverage is increased on the transformed program.

Sometimes we want to refer to the coverage as either fragile or robust. In accordance with Def. 2, we can introduce the following denition. Denition 3. Fragile [Robust] Coverage. Given a coverage criterion C, a program p, a test suite ts for p, and T a set of code transformations, we say that the coverage of p provided by ts with respect to the coverage criterion C and the code transformations T is fragile [ robust], if and only if the program p is [is not] fragilely covered by ts with respect to C and T .

The fact that a coverage is fragile or robust strongly depends on the set of transformations T one considers. With a small set T any coverage is likely to be robust, but with a large T only the best test suites will provide the robust required coverage. For this reason, the client who requires certain levels of coverage and robustness has to provide the tester with adequate transformations in order to ensure the desired condence in the code coverage. The given set of transformations T should depend on the expected set of SPTs that will be applied on the program or on the set of transformations applied in the past on the program. It is important to dene such programs whose coverage is not aected by the application of transformations, we call them robust programs. Denition 4. Robust program Given a coverage criterion C and a set of code transformations T , we say that a program p has robust structure if any test suite that provides the coverage C for p, C is robust.

Code with robust structure is of great interest for testers, since its coverage during testing cannot be diminished by code transformations, i.e. the coverage achieved by any test suite on a robust program will not diminish regardless the sequence of SPTs t 1 , . . . , t n ∈ T applied to it. Given a program p and a test suite ts, which achieves a certain level of coverage C(p, ts) for a coverage criterion C, there are two ways to increase the achieved coverage. If the program p is robust, we can generate a new test suite ts also transforming the program, because generating a test suite ts that achieves a coverage higher than C(p, ts) assure also that C(p, ts ) ≥ C(p, ts). If the program is not robust the only way to increase the coverage is extending the test suite ts, because the Theorem 1 proves that generating a new test suite ts that achieve higher coverage on a transformed version of p does not assure to obtain a better coverage on p.

Fragility and robustness measures

We dene a measure to express how much the coverage achieved by the test suite ts on the program p with respect to the criterion C is robust to the changes in the code structure introduced by a set of SPTs T . Our metrics works with any existing coverage criterion C, without the need to introduce new and possible more complex testing criteria. This allows the tester to re-use existing criteria (and associated tools) which he/she is already familiar with.

The metrics is called extended coverage (because extends the usual coverage measurement with an information on how much the coverage oered by the test suite is sensitive to transformations), and it consists of a couple of values (a, b) where a = C(p, ts) represent the usual coverage obtained by applying ts to the program p, whereas b is a fragility index such that b ∈ [0, 1], and it measures the sensitivity of the coverage to modications in the code structure. For a coverage measure in the form (a, b), b = 0 means that a is the robust coverage, while as b → 1 the coverage a is increasingly sensitive to the transformations of the code structure. If b = 1 the coverage a is completely fragile.

Let p be a program, ts a test suite, and C a coverage, we dene ∆(t) = C(p, ts) -C(t(p), ts) where t is a transformation. Let pos(x) be a function dened as max(0, x). We dene three fragility indexes. The rst one is simply the averaged fragility :

b af = pos t∈T ∆(t) |T |
The second one is called weighted fragility and it is dened as

b wf = t∈T ρ(t) * pos(∆(t))
where ρ(t) is a function that denes the weight of each transformation t ∈ T , such that t∈T ρ(t) = 1. The weighted fragility is a useful metrics in case we want to assign a dierent weight to some transformations for a particular reason, e.g. the weight can represent the likelihood that a certain transformation will be applied to the code. The third fragility index is called worst case loss of coverage.

It ANT: Apache Ant is a Java library and command-line tool widely used to compile and build Java applications.

NXML: NanoXML is a small XML parser for Java.

Code for TACAS, JTOPAS, ANT, NXML and their unit tests can be found in the SIR repository [7]. The Java implementation of ASW is included in the Java Path Finder distribution [21].

In our study we have considered statement, branch and MCDC coverage criteria. We have studied all the transformations presented in Section 3.1, and thus All the programs and test suites considered in our study suer from fragility problems: semantically equivalent programs achieve dierent results in terms of coverage, and thus SPTs can inuence greatly the coverage achieved by test suites. Our results highlight the fact that some transformations inuence only certain coverage criteria, e.g. t ecf inuences only MCDC in our study, whereas other transformations, such as t rc , seems to not inuence the coverage at all. For this reason, the choice of the transformations considered in the robustness analysis can signicantly inuence the results of the analysis itself.

No apparent correlation can be identied between the size of the test suite and their fragility: indeed, signicant losses in terms of coverage exist also for big test suites, e.g. Table 3 shows that also the random test suite with 1000 test cases has high losses. Note that even if the losses in terms of coverage may be small in some cases, this is usually due to the low coverage achieved by the test suites. For instance, in the ANT case the maximum loss is 8.4%, but the coverage achieved on the original program is only 10.9%.

Test suite with high coverage, can be fragile as well: from the results, it seems that test suites generated by hand explicitly to achieve good coverage, are those with higher losses in terms of coverage. This is due both to the fact that these test suites have small sizes and also to the fact that they are created ad-hoc to obtain full coverage of the program with a particular structure and thus the coverage is more fragile than the one of a not ad-hoc test suite.

Threats to Validity

There are three main aspects that can pose a threat to the validity of our work.

Transformations: Although the set of selected transformations is small, in our opinion it can demonstrate the eectiveness of our approach. By extending the given set of transformations, test suites become likely less robust. The selected transformations are meaningful examples. Indeed t ecf is already used in several works [11,17], whereas t cdcf , t rc , t ecf and t fbc are extracted from common refactoring techniques [8,1].

Coverage Criteria: We have considered three common structural coverage criteria, i.e. statement coverage, branch coverage and MCDC. Rajan et al. [17] show that MCDC is highly sensitive to the structure of the implementation and our experiments conrm that. Test suites adequate to other non structural coverage criteria may be less fragile.

Experiments: Our work has focused only on a limited set of Java programs.

However we think that chosen programs are representative of several classes of systems, i.e. toy examples (LEAP, TRI), critical systems (WBS, ASW, TCAS), and complex Java libraries (JTOPAS, NXML, ANT). Our experiments involved 1442 classes and more than 120kLOC, and therefore the selected programs are, in our opinion, a representative sample of real Java programs. We have also used dierent test suites which range from manually built test suites, to test suites generated by using well-known tools.

Conclusions and Future Work

In this paper we have proposed a framework to evaluate the robustness of a test suite with respect to semantic preserving transformations applied to the program under test. We have introduced the concept of fragile and robust coverage and we have identied the conditions for a code to have a robust structure with respect to a certain set of transformations. Moreover, we have dened a new extended coverage metrics that takes into account the fragility of the coverage. The extended coverage does not require either a modication of the code or the introduction of new original testing criteria. It uses a fragility index to quantitatively measure the quality of test suite in terms of its robustness. In presence of fragile code, we suggest either to (1) nd and remove fragility points by modifying the code or (2) increase the test suite until its robustness reaches a desired level. We have evaluated the fragility of several Java programs (from toy examples to Java library code) together with their test suites and we have found that the fragility problem occurs in all the considered programs.

In the future we plan to study the correlation between the fragility of the test suite and its fault detection capability. We also plan to dene a language for the formalization and denition of semantic preserving transformations. In this way, we can easily model other transformations and also extend the theoretical framework.

3

  Theoretical backgroundTesting criteria, often called coverage criteria, have the main goal of measuring the test quality. They are used as a metrics to quantify the coverage of the control ow of a program achieved by a test suite. Usually they are also used as a stopping rule to decide when the testing process can stop and the software can be accepted. Studying coverage criteria, dening new ones, and providing empirical evidence of their fault detection capability have been a major research focus for the last three decades. First of all, we introduce a framework dening them formally, mainly taken from[24], where the reader can nd an exhaustive treatment of the subject. For the purpose of our paper we do not consider directly the use of testing criteria for test suite generation, and we focus on program based structural testing, that does not consider the specication and denes testing requirements only in terms of program elements (statements, conditions, and so on). Given the set of programs P and the set of all the test suites TS, we dene a testing criterion in the following way. Denition 1. Testing Criteria. A testing criterion is a function C, C : P × T S → [0, 1]. C(p, ts) = r means that the adequacy of testing the program p by the test set ts is of degree r according to the criterion C. The greater the real number r, the more adequate the test suite ts is.Given a xed value r , such that 0 ≤ r ≤ 1, which represents the lower expected coverage for the criterion C applied to the program p ∈ P , we can consider the test suite ts ∈ T S as adequate for testing program p i C(p, ts) ≥ r .In program based structural testing, coverage requirements are expressed in terms of the coverage achieved over a particular set of elements in the structure of the program under test (e.g. the set of all the statements for statement coverage or the set of all the conditions for condition coverage ). We will focus on classical coverage criteria[3,15], including the statement and branch coverage and the Modied Condition Decision Coverage (MCDC)[5].

  Proof. We prove the theorem by showing a case in which the converse C(t(p), ts ) > C(t(p), ts) implies C(p, ts ) > C(p, ts) is false. Consider the transformation t ecf and the following program p and its transformed version t ecf (p): x = a && b && c ; && b && c ; i f ( a && b && c ) { . . . } Given the test suite ts, which has two test cases (a = true, b = true, c = false) and (a = true, b = true, c = true), and considering the condition coverage criterion, the coverage is C(p, ts) = 1.0 while C(t ecf (p), ts) = 4/6 = 0.66. If we consider then a test suite ts that has two test cases (a = false, b = true, c = true) and (a = true, b = false, c = true), the coverage that ts achieves on t ecf (p) is 5/6 = 0.83 and thus it improves the coverage of ts over t ecf (p), i.e.

  is an indicator of what is the maximum loss of coverage between the original program and any transformed one, and it is expressed as b wc = pos(max t∈T (∆(t)))In this case if the index b wc = 0 it means that a is the robust coverage, otherwise b wc indicates the maximum loss of coverage and thus the real coverage in the worst case is C(p, ts) -b wc .The extended coverage is a very useful metrics, especially if it is measured during the development phase. For instance with respect to unit testing, once the developer has measured the extended coverage, if it is not a robust coverage he/she can act in two ways to increase the robustness of the coverage: (a) he/she could extend the test suite with new test cases, maybe generated from a transformed version of the program, (b) he/she could change the structure of the code in order to remove all the points that introduces fragility issues. However, removing fragility points may be not straightforward nor possible every time (this fact highly depends on the transformations in T ). Moreover transforming the code would increase the robustness at the expenses of the coverage, which would diminish. To maintain the same level of coverage, the tester should add new tests in any case.5 ExperimentsIn order to evaluate how much the transformation of a program inuences the robustness of the coverage oered by a test suite we have analyzed several Java programs. The selected programs vary from toy examples to complex Java libraries. The programs are the following:LEAP: It contains one method checking whether the passed year is leap or not. TRI: It contains a triangle classication method, which takes as input the length of the three sides and computes the type of the triangle [3].

  The concept of code coverage was rst clearly introduced by Miller and Maloney from theUS Chemical Corps in 1963 [14], although some similar concepts were already introduced by Senko from IBM[19]. Miller and Maloney observed that it is not sucient to know that a program passes all the tests, since each test case checks a portion of the program and some portions may be not tested at all.They developed a model of programs based on ow charts and logical trees and required that every case is tested at least once. Following their approach, various notions of code coverage have been proposed as a measure for test suite quality, including statement coverage, branch coverage, method coverage, MCDC, and others[15]. These criteria consider the code structure, give a measure of the adequacy of the testing activity, and they can be used to drive the testing activity

	[20] show that test suites generated specically to satisfy coverage criteria achieve
	poor results in terms of eectiveness, whereas the use of coverage criteria as a
	supplement to random testing provides an improvement in the eectiveness of
	the generated test suites.
	It is well known that coverage criteria can be very sensitive to code structure
	both if they are used for measuring test adequacy and if they are used for test
	generation. Regarding the adequacy, there are several works arguing that code
	coverage is not robust to code structure transformations. In [13], the authors
	show how very simple transformations (like adding a new empty line) can con-
	fuse code coverage tools. More severe issues are presented in [17]. In that paper,
	the authors prove that the MCDC metrics is highly sensitive to the structure of
	the implementation and can therefore be misleading as a test adequacy criterion.
	They present six programs in two versions each: with and without expression
	folding (i.e., inlining). They nd that the same test suites performed very di-
	versely on the two versions. Their suggestion is either (1) to introduce a new
	coverage metrics that takes the use of inlined condition into consideration, or

itself, for instance, requiring that certain tests must be generated. These criteria do not guarantee that the program is correct if it passes adequate testing, i.e. they are not ideal

[10]

. However, they have practical utility and they are generally required for commercial software. For instance, the Modied Condition Decision Coverage (MCDC)

[5]

, is required for safety critical aviation software by the RCTA/DO-178B standard. The basic assumption is that a test suite is likely to be eective at revealing faults if it exercises the code where the fault is located.

Therefore, increased code coverage is expected to correlate with more revealed faults, although other factors may inuence the actual outcome

[16]

. Staats et al.

  P that achieves a certain coverage C may not achieve the same level of coverage C on the original program P .

	generation. Often the structure of the code makes hard the generation of tests,
	i.e. it reduces its testability, especially when test generation is performed auto-
	matically. The automated generation of adequate test data can be impeded by
	properties of the code itself (for example, ags, side eects, and unstructured
	control ow). For this reason testability transformations are introduced [11]. A
	testability transformation is a code-to-code transformation that aims to improve
	the ability of a given test generation method to generate test data for the original
	program. A rst dierence between our approach and the work of Harman et al.
	is that we do not tackle the problem of test suite generation but we only want
	to measure the robustness of a given test suite in order to obtain a measurement
	of how much the coverage is aected by modications in the code structure. An-
	other dierence is that testability transformations are not semantic preserving
	while the transformations dened in our work do not modify the semantics of
	the program. We will also show that the use of testability transformations should
	be carefully considered because the test suite generated from a transformed pro-

gram

  This transformation was already identied byRajan et al. [17], which showed its eects on MCDC criterion, and by Harman et al.[11], which showed how it can be used in order to enhance the test generation Code coverage is very sensitive to the code structure and it can therefore be misleading as test adequacy criterion. This fact is well explained in[17] for MCDC in case of inlining and outlining of Boolean variables (addressed by our t ecf and t ecf -1 transformations). Even though examples in literature are focused only on the extrapolation of a complex ag, the sensitivity of coverage criteria to code structure can be generalized for any code transformation and any code coverage criterion. Indeed we show several code fragments with the same semantics that achieve dierent coverage degrees with the same coverage criteria and the same test sets.Example 1. For instance consider the following code fragment, in which in_1 and in_2 are two inputs and the guard of the conditional statement has been outlined, i.e. the guard is simply a Boolean variable dened in terms of other

	Flattening Conditional Expression The transformation t fbc splits all the expressions used as guards in conditional statements until every if statement has only an atomic Boolean expression as a guard. It can be dened using two i f ( a ) { 4 Coverage robustness i f ( a && b ) { . . . . // body t fbc i f ( b ) { ⇒ . . . . // body 4.1 Code transformations and coverage } }
	} schema. The rst schema represents how the transformation splits a conjunctive The transformation does not change the behaviour of the program, but the
	condition: original test suite would cover only the rst decision on the transformed program.
			i f ( c o n d 1 ) {
	i f ( c o n d 2 ) { . . . t 1 . . . Example 4. Consider the following code fragment in which a is a Boolean vari-i f ( c o n d 1 && c o n d 2 ) { . . . t 1 . . . } e l s e { t fbc able and i an Integer variable: } e l s e { ⇒ . . . t 2 . . . i f ( a ) {
	. . . t 2 . . . i f ( a ) } i = i +1; e l s e	t cdcf ⇒	} } e l s e { . . . t 2 . . . } e l s e { i = i +1; S y s t e m . o u t . p r i n t l n ( i ) ;
	i = i +2;		}	i = i +2;
	The second schema represents how the transformation splits a disjunctive phase. It has the following schema: S y s t e m . o u t . p r i n t l n ( i ) ; S y s t e m . o u t . p r i n t l n ( i ) ;
	b o o l e a n x ; . . . condition:		b o o l e a n x ; . . .
	x = c o m p l e x B o o l E x p r ; //A . . . i f ( c o n d 1 | | c o n d 2 ) { i f ( . . . x . . . ) { //B . . . . . . t 1 . . . } e l s e { Boolean variables or expressions. t ecf ⇒ t fbc ⇒ } . . . t 2 . . . } b o o l e a n e x p r _ 1 = i n _ 1 | | i n _ 2 ; i f ( e x p r _ 1 ) { . . . t ecf ⇒	x = c o m p l e x B o o l E x p r ; i f ( c o n d 1 ) { . . . . . . t 1 . . . } e l s e i f ( c o n d 2 ) { . . . t 1 . . . } e l s e { . . . t 2 . . . i f ( i n _ 1 | | i n _ 2 ) { . . .
	}
			. . . t 0 . . .
			i f ( x==a ) {
	. . . t 0 . . . i f ( a<=x && x<=b ) { . . . t 1 . . . } e l s e { . . . t 2 . . . } Reverse Conditional The transformation t rc is associated with the Reverse t b ⇒ . . . t 1 . . . } e l s e i f ( x==b ) { . . . t 1 . . . } e l s e i f ( x>a && x<b ) { . . . t 1 . . . } e l s e { . . . t 2 . . . } i f ( c o n d ) { i f ( c o n d ) { . . . t 1 . . . . . . t 1 . . . } e l s e { t cdcf s t a t e m e n t ; ⇒ } e l s e { . . . t 2 . . . . . . t 2 . . . } s t a t e m e n t ; s t a t e m e n t ; } . . . i f ( x >=2) x=x +1; e l s e . . . t b i f ( x==2) x=x +1; ⇒ e l s e i f ( x >2) x=x +1; x=x +2; x=x +2; e l s e Meaning of transformations The meaning of code transformations regarding A test suite containing only two tests (x=0) and (x=5) achieves 100% of Conditional refactoring pattern [1]. It simply inverts the condition of the if the testing activity depends on which of two scenarios explained in the introduc-branch coverage. However the same test suite achieves only 75% of branch cov-statement and exchange the then block and the else block between them, and tion we assume. If we suspect that the code was transformed in the past, code erage on the transformed code. cond is a boolean expression. It has the following schema: i f ( c o n d ) { . . . t 1 . . . } e l s e { . . . t 2 . . . } trc ⇒ transformations bring the code to its original structure, while, if we assume that i f ( ! c o n d ) { the code will be changed in the future, code transformations model the changes Example 3. Consider the following code fragment, in which a and b are Boolean . . . t 2 . . . } e l s e { . . . t 1 . . . } the code will be subject to. For instance, t variables. To achieve a full decision coverage a test suite containing only two ecf would undo the insertion of ags for conditions in if statements done in the past. tests (a = true, b = true) and (a = false, b = true), is enough.

i f ( . . . c o m p l e x B o o l E x p r . . . ) { . . . } In the schema, complexBoolExpr is a Boolean expression that contains at least one Boolean operator, and the statements between the point A and B do not change the value of x, and of the variables referenced in complexBoolExpr.

We briey call this transformation t ecf . By applying t ecf to a program p we obtain a new program t ecf (p) in which all the ags in if statements are expanded to their denition. Several refactoring patterns [8] can be partially mapped on this transformation or its inverse, i.e. Inline Temp Variable (in case the variable is boolean and it is inlined in an if statement ), Remove Control Flag, Introduce Explaining Variable. Boundary extraction This transformation t b acts on an if statement and splits it into several if statements if it contains a condition in the form of a x b, where a, b, and x are numerical constants or variables. It has the following schema: } In both schema cond1 and cond2 are boolean expressions. It is a generalization of the Consolidate Conditional Expression refactoring pattern [8]. Note that a similar transformation may be performed during compilation (e.g. in the byte code) and therefore, a test suite that achieves the decision coverage of the original program, may not achieve the same coverage of the compiled program. This problem is also studied in [12] and it is a common transformation done when the source code is transformed into assembly code (for conjunctive expressions). Remove Consolidate Conditional Fragment The transformation t cdcf is the inverse transformation of the one associated with the Consolidate Conditional Fragment refactoring pattern [8]. It simply moves into the then block and the else block the rst statement after the if statement. It has the following schema: } A test suite containing only two tests (in_1=true, in_2=false) and (in_1=false, in_2=false) covers the MCDC for the if statement, which has a simple variable as guard, so two tests are enough. However, if we apply t ecf , the transformed code were written with the condition inlined and thus the same test suite would not achieve the MCDC of the same code. These simple patterns recur quite often in software and in models [17]. However, it would be not acceptable to force the developer to choose only the inlined version, in order to avoid that a full MCDC coverage is achieved with less test cases. The outlined version is more readable and maintainable since a complex expression is re-factored in an auxiliary variable. This situation can be also the result of an explicit extract local variable refactoring operation [8]. It could also perform better, since the Boolean ag is computed only once. Example 2. Consider the following code, where x is an integer variable and a simplied form of boundary extraction is applied: } The test suite containing only one test (a = true) achieves 60% of statement coverage. However on the code transformed by using the t cdcf transformation, the same test suite achieves only 50% of coverage.

Table 1 .

 1 esults in perentge of the roustness nlysis for vieD sD nd ge nd their test suitesD where a = C(p, ts)F Random1 test suite contains 100 tests, and Random2 contains 1000 tests for all projects. Evosuite has 4 tests for LEAP, 13 for TRI, and 16 for JTCAS.Handmade has 1 test for all the projects. JTOPAS: It is a simple, easy-to-use Java library for the common problem of parsing arbitrary text data.

	WBS: The Wheel Brake System (WBS) is a Java implementation of the WBS
	case example found in ARP 4761 [4,17]. The WBS determines what pressure
	to apply to braking based on the environment.
	TCAS: It is the Java implementation of a Trac Collision Avoidance System
	(TCAS) II, required on all commercial aircraft ying in US airspace.
	ASW: The Altitude Switch (ASW) is a synchronous reactive component from
	the avionics domain that controls the power of some devices according to
	the airplane altitude.

  For each test suite ts, for each coverage criterion C and for each program under test p, we have computed the coverage 1 achieved by ts for the criterion C on the program p and for any transformed program t(p), for each t ∈ T .Table1presents the results of the robustness analysis for the smallest case studies (LEAP, TRI, and TCAS). For each program and test suite, the table shows the results in terms of coverage a and the worst case loss of coverage b wc

	fragility index.

T = { t ecf , trc , tb , t fbc , tcdcf }. For each example we have considered an handmade test suite (for TACAS, JTOPAS, ANT and NXML the considered test suite is the one presented in the SIR repository). For the smallest case studies (LEAP, TRI, WBS, and TCAS), we have also considered a test suite automatically generated by means of Evosuite [9] and random test suites with a xed dimension of 100 and 1000 test cases. Experiments with random test suites are repeated 10 times, with dierent seeds, and only the averaged results are presented in this paper.

Table 2

 2 shows the results of our study on the biggest case studies (ASW, TOPAS, NXML, and ANT). For each program, the table shows the results in terms of coverage achieved by the provided test suite and the two fragility indexes, the worst case loss of coverage b wc and averaged fragility b af .

	Table 3 shows the detailed results of the robustness analysis for the WBS
	program. For each test case and coverage criterion, the table shows the results
	1 e use the godegover tool http://codecover.org/

Table 3 .

 3 esults in perentge of the roustness nlysis for f @IWR lines of odeA in terms of coverage achieved by the test suite and the losses in terms of coverage on the transformed versions of the program. The table shows only the results for the t fbc , t ecf and t cdcf transformations, because the WBS program is not inuenced by the t rc and t b transformations.

Acknowledgments The authors would like to thank Matt Staats for sharing some code examples. References IF eftoring tlog E wesiteF http://www.refactoring.com/catalog/F PF eF F ehoD F ethiD nd tF hF llmnF Compilers: principles, techniques, and toolsF eddisonEesley vongmn ulishing goFD snFD fostonD weD eD IWVTF QF F emmnn nd tF y'uttF Introduction to Software TestingF gmridge niversity ressD xew orkD xD eD I editionD PHHVF RF ARP 4761,Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and EquipmentF eerospe eommended rtieD oiety of eutomotive ingineersD hetroitD eD IWWTF SF tF tF ghilenski nd F F willerF eppliility of modi(ed onditionGdeision ovE erge to softwre testingF Software Engineering JournalD W@SAXIWQ!PHHD IWWRF TF iF F hijkstrF xotes on strutured progrmmingF sn yF tF hhlD iF F hijkstrD nd gF eF F roreD editorsD Structured ProgrammingF edemi ressD IWUPF UF rF hoD F qF ilumD nd qF othermelF upporting ontrolled experimenttion with testing tehniquesX en infrstruture nd its potentil imptF Empirical Software EngineeringD IH@RAXRHS!RQSD PHHSF VF wF powlerF Refactoring: Improving the Design of Existing CodeF eddisonEesleyD eugF IWWWF WF qF prser nd eF eruriF ivosuiteX eutomti test suite genertion for ojetE oriented softwreF sn Proc. of ACM SIGSOFT ESEC/FSED pges RIT!RIWD PHIIF IHF tF fF qoodenough nd F vF qerhrtF owrd theory of test dt seletionF IEEE Trans. Softw. Eng.D I@PAXIST!IUQD tune IWUSF IIF wF rrmnD vF ruD F rieronsD tF egenerD rF thmerD eF freselD nd wF operF estility trnsformtionF IEEE Trans. Softw. Eng.D QHXQ!ITD tnury PHHRF IPF F uirnerF owrds preserving model overge nd struturl ode overgeF EURASIP J. Emb. SysD PHHWXI!ITD PHHWF IQF fF wrikD tF mithD nd wF tonesF row to misuse ode overgeF sn Proc. of ICTCS'99D tune IWWWF IRF tF gF willer nd gF tF wloneyF ystemti mistke nlysis of digitl omputer progrmsF Commun. ACMD TXSV!TQD perury IWTQF ISF qF tF wyersF The art of software testing (2. ed.)F ileyD PHHRF ITF eF F xmin nd tF rF endrewsF he in)uene of size nd overge on test suite e'etivenessF sn Proc. of ISSTA 2009D pges SU!TVF egwD PHHWF IUF eF jnD wF F hlenD nd wF F reimdhlF he e'et of progrm nd model struture on mGd test dequy overgeF sn Proc. of ICSED pges ITI!IUHD PHHVF IVF F pps nd iF eyukerF eleting softwre test dt using dt )ow informtionF IEEE Trans. Soft. Eng.D iEII@RAXQTU ! QUSD pril IWVSF IWF wF iF enkoF e ontrol system for logil lok dignosis with dt lodingF Commun. ACMD QXPQT!PRHD eprF IWTHF PHF wF ttsD qF qyD wF F hlenD nd wF reimdhlF yn the dnger of overge direted test se genertionF sn Proc. of Fundamental Approaches to Soft. Eng. (FASE)D PHIPF PIF wF tts nd gF § s § renuF rllel symoli exeution for struturl test genE ertionF sn Proc. of ISSTAD pges IVQ!IWRD xew orkD xD eD PHIHF egwF PPF F eiÿlederF imulted stisftion of overge riteri on uml stte mhinesF sn Proc. of ICST 2010D pges IIU!IPTF siii gomputer oietyD PHIHF PQF iF tF eyukerF rnsltility nd deidility questions for restrited lsses of progrm shemsF SIAM J. Comput.D V@RAXSVU!SWVD IWUWF PRF rF huD F rllD nd tF wyF oftwre unit test overge nd dequyF ACM Computing SurveysD PW@RAXQTT!RPUD IWWUF