Alexandre Petrenko
email: petrenko@crim.ca

Adenilso Simao
email: adenilso@icmc.usp.br

Checking Experiments for Finite State Machines with Symbolic Inputs

Keywords: Finite State Machines, Extended Finite State Machines, Symbolic Automata, Conformance testing, Checking experiments, Fault model based test generation 1

There exists a significant body of work in the theory of checking experiments devoted to test generation from FSM which guarantees complete fault coverage for a given fault model. Practical applications require nevertheless methods for fault-model driven test generation from Extended FSMs (EFSM). Traditional approaches for EFSM focus on model coverage, which provides no characterization of faults that can be detected by the generated tests. Only few approaches use fault models, and we are not aware of any result in the theory of checking experiments for extended FSMs. In this paper, we lift the theory of checking experiments to EFSMs, which are Mealy machines with predicates defined over input variables treated as symbolic inputs. Considering this kind of EFSM, we propose a test generation method that produces a symbolic checking experiment, adapting the well-known HSI method. We then present conditions under which arbitrary instances of a symbolic checking experiment can be used for testing black-box implementations, while guaranteeing complete fault coverage.

Introduction

Research in Model Based Testing (MBT) is currently advancing rapidly trying to match the growing demand from industry for more effective and better scalable test development technologies. Since the cost for leaving undetected faults in software grows with its complexity, code and model coverage by tests is often considered insufficient and the guaranteed fault detection becomes the ultimate goal. Accordingly, research in MBT has been addressing fault modeling and fault model driven test gen-eration problems, see, e.g., [START_REF] Bochmann | Fault models in testing[END_REF], [START_REF] Yannakakis | Testing finite state machines: fault detection[END_REF]. Fault models usually refer to test models which formalize reference specifications and/or requirements. State-oriented test models seem to be most popular models among test engineers. Finite state machines (FSM) and input output transition systems (IOTS) are state-oriented models; test generation methods have traditionally been developed separately for these models, even though, as has already been demonstrated, many ideas, especially for fault model based test generation, developed for testing from FSM can successfully be used for testing from IOTS [START_REF] Simao | Generating complete and finite test suite for ioco: is it possible?[END_REF].

There exists a significant body of work devoted to the development of methods for test generation from a given FSM to guarantee the complete fault coverage, once a fault model is defined. The pioneering work of Moore [START_REF] Moore | Gedanken-experiments on sequential machines[END_REF] and Hennie [START_REF] Hennie | Fault-detecting experiments for sequential circuits[END_REF] led to the development of the theory of checking experiments, where faults are modeled by a universe of FSMs with a given number of states, see, e.g., [START_REF] Chow | Testing software design modeled by finite-state machines[END_REF], [START_REF] Dorofeeva | Experimental evaluation of FSM-based testing methods[END_REF], [START_REF] Fujiwara | Test selection based on finite state models[END_REF], [START_REF] Vasilevskii | Failure diagnosis of automata[END_REF]. Checking experiments have already been lifted to FSMs more general than the classical (completely specified and deterministic) Mealy machine, such as partially defined and nondeterministic state machines, see, e.g., [START_REF] Petrenko | Conformance tests as checking experiments for partial nondeterministic FSM[END_REF]. However, practical applications require more extensions to the classical FSM model. These are commonly known as the Extended Finite State Machine (EFSM) models. Various flavors of EFSMs are used in Harel's statecharts [START_REF] Harel | The STATEMATE Semantics of Statecharts[END_REF], SysML/UML [START_REF] Friedenthal | A practical guide to SysML: the systems modeling language[END_REF], Simulink/Stateflow [START_REF] Tiwari | Formal semantics and analysis methods for Simulink Stateflow models[END_REF], SDL [START_REF] Glässer | The formal semantics of SDL-2000: status and perspectives[END_REF] and other modelling languages. Extensions are often suggested without a formal semantics; this creates a big hurdle for fault-model based test generation. Whenever the semantics of a particular specification language is defined by the tool which supports it, fault models become specific to the tool provider and may not be adequate for implementations coming from other suppliers. General testing approaches usually rely on formally defined extensions of Mealy machine, see, e.g., [START_REF] Petrenko | Confirming configurations in EFSM testing[END_REF], [START_REF] Wang | Generating test cases for EFSM with given fault model[END_REF].

Most of the existing work on test generation from EFSM concentrates on the model coverage, see, e.g., [START_REF] Cheng | Automatic Functional test generation using the extended finite state machine model[END_REF], [START_REF] Hong | A temporal logic based theory of test coverage and generation[END_REF], [START_REF] Kalaji | Generating feasible transition paths for testing from an extended finite state machine (efsm)[END_REF], [START_REF] Petrenko | A method and tool for test optimization for automotive controllers[END_REF], which provides no characterization of faults that can be detected by the generated tests. There are some techniques for test generation from EFSM which use certain fault models [START_REF] Wang | Generating test cases for EFSM with given fault model[END_REF], [START_REF] Petrenko | Confirming configurations in EFSM testing[END_REF] and limited state/configuration identification sequences [START_REF] Chun | Test case generation for protocols specified in Estelle[END_REF], [START_REF] Li | Automatic generation of extended UIO sequences for communication protocols in an EFSM model[END_REF], [START_REF] Petrenko | Confirming configurations in EFSM testing[END_REF]. The work of [START_REF] Huang | Complete model-based equivalence class testing[END_REF] uses checking experiment methods, but requires first to determine input/output equivalence classes from a given specification EFSM and choose concrete inputs. To the best of our knowledge, there is no result in lifting the theory of checking experiments to extended FSMs. This observation is one of the main motivations of this work.

Another motivation comes from research on symbolic automata and transducers, which is driven by several practical problems. The work of [START_REF] Veanes | Applications of symbolic finite automata[END_REF] mentions applications ranging from modern regex analysis to advanced web security analysis where the socalled sanitizers, string transformation routines are extensively used as the first line of defense against cross site scripting attacks. A large class of sanitizers can be described and analyzed by using symbolic finite state transducers. Symbolic finite automata are introduced as an extension of classical finite state automata that allows transitions to be labeled with predicates. Automata with predicates instead of concrete symbols are also used in [START_REF] Watson | Implementing and using finite automata toolkits[END_REF] and discussed in [START_REF] Noord | Finite state transducers with predicates and identities[END_REF] in the context of natural language processing. The work on learning symbolic automata [START_REF] Maler | Learning regular languages over large alphabets[END_REF] has also to be mentioned here, since the automata learning shares certain aspects with the testing problem in the following sense. If a black box passes a checking experiment, then under well-defined conditions it is recognized as some automaton. Hence it is important to investigate checking experiments for symbolic automata.

The community focusing on testing from IOTS has also considered extensions to symbolic representation of transition systems which avoid enumerations of its components, see, e.g. [START_REF] Frantzen | Test generation based on symbolic specifications[END_REF], [START_REF] Rusu | An approach to symbolic test generation[END_REF], but these approaches are not fault model driven, they use one or another test purpose. More references on symbolic approaches in testing could be found, e.g., in [START_REF] Anand | An orchestrated survey of methodologies for automated software test case generation[END_REF] and [START_REF] Jéron | Symbolic methods in testing[END_REF].

In this paper, we attempt to lift the theory of checking experiments to a special type of EFSM, which extends the deterministic Mealy machine with predicates defined over input variables, considered as its symbolic inputs. We propose a test generation method that produces a symbolic checking experiment, adapting the well-known HSI method [START_REF] Yevtushenko | Synthesis of test experiments in some classes of automata[END_REF]. We then investigate under which conditions instances of a symbolic checking experiment can be used for testing black-box implementations, guaranteeing the full fault coverage.

The paper is organized as follows. In Section 2, we define the model of FSM with symbolic inputs. In Section 3, we study the relations between SIFSMs. Symbolic and concrete checking experiments are introduced in Section 4, where we also investigate fault detection capability of concrete tests obtained from symbolic checking experiments. Section 5 summarizes our contributions and presents future work.

2

Definitions and Notations

Preliminaries

We define an (input) alphabet as a set of guards over variables of well-defined types. Let G denote the universe of guards that are predicates over variables in a fixed set V for which a decision theory, e.g., an SMT solver, exists, excluding the predicates that are always false. G* will denote the universe of input sequences. Let D V denote the set of all the valuations v of the input variables in the set V, called concrete inputs. A set of concrete inputs is called a symbolic input; both, concrete and symbolic, inputs are represented by guards in G. Henceforth, we use settheoretical operations on symbolic inputs. In particular, we write v  g, when concrete input v satisfies g. We define some relations between input sequences in G*.

Definition 1. Given two input sequences ,   G* of the same length k,  = g 1 ...g k ,  = g 1 ...g k , we let   = g 1  g' 1 …g k  g' k denote the sequence of intersections of inputs in sequences  and and  are compatible, if for all i = 1, …, k, g i  g' i  . We say that  is a reduction of, denoted  , if  =  . If  is a sequence of concrete inputs as well as a reduction of then it is called an instance of ; given a finite set of input sequences E  G*, a set of concrete input sequences I is called an instance of the set E, if I contains at least one instance for each input sequence in E.

Symbolic Input FSM

We define a model, called a symbolic input finite state machine (SIFSM), which operates in discrete time as a synchronous machine reading values of input variables and setting up the values of output variables. Output variables are assumed to have a finite number of valuations and form a finite output alphabet. On the other hand, there may exist an infinite set of input valuations. SIFSM uses guards on transitions which are executed one at a time.

Definition 2. A symbolic input finite state machine S (or machine, for short) is a 7tuple (S, s 0 , V, O, F, , ), where  S is a finite set of states with the initial state s 0 ,  V is a finite set of input variables over which guards in G are defined,  O is a finite set of outputs,  F  S  G is a finite specification domain,  : F  S is a transition function, and  :

F  O is an output function.
Examples of SIFSM are given in Figure 1. Examples of realistic systems which can be specified as SIFSM could be found in [START_REF] Huang | Exhaustive model-based equivalence class testing[END_REF] and in [START_REF] Petrenko | A method and tool for test optimization for automotive controllers[END_REF]. In the first work, the Ceiling speed monitoring following the public ETCS system specification [START_REF]European Railway Agency: ERTMS-System Requirements Specification-UNISIG SUBSET[END_REF] is modelled, it has two input and two output variables. In the second work, an HVAC controller specified in Simulink/Stateflow is considered, it has nine input variables, Boolean and naturals, the most complex transition guard comprises 13 terms.

The semantics of SIFSM is defined by a Mealy state machine with a possibly infinite input set, where the state and output sets remain finite.

Given (s, g)  F, we say that input g is defined in state s  S. Then, G(s) = {g  G | (s, g)  F} contains all inputs defined at s. The machine S is deterministic, if for any (s, g), (s, g)  F, it holds that g  g' = . State s of the machine S is input-complete, if for each input valuation v, at least one of its guards evaluates to True, i.e., {v  g | g  G(s)} = D V . The machine S is input-complete, if each state is input-complete. The machine S is normalized, if for all (s, g), (s, g)  F, (s, g) = (s, g) implies that (s, g)  (s, g); in other words, the machine has at most one transition with a given output for each ordered pair of states. Any machine that is not normalized can always be converted into a normalized one by merging transitions with the same start and end states as well as the same output and forming the disjunction of their guards. This is a unique compact form of a SIFSM. We will consider only normalized deterministic input-complete specification machines.

An input sequence   G*,  = g 1 ...g k , is defined in state s  S, if each input in  is defined in a corresponding state, i.e., if there exist states s 1 , ..., s k , s k+1 , where s 1 = s, such that (s i , g i )  F and (s i , g i ) = s i+1 for each 1 ≤ i ≤ k. Let S(s) denote the set of input sequences defined in state s, and S denote sequences defined in the initial state of S. Moreover, S(s) denotes the set S(s) closed under the reduction relation, called the set of input sequences admissible in state s, i.e., S(s) = {   G* |   S(s),   }, and S denotes sequences admissible in the initial state of S. Notice that for an input-complete machine S any concrete input sequence is admissible in every state, i.e., D V * = S(s), for each s  S. We lift the transition and output functions from inputs to admissible input sequences, including the empty sequence , as usual: for s  S, (s, ) = s and (s, ) =  and for input sequence   S(s) and input g  S((s, )), (s, g) = ((s, ), g') and (s, g) = (s, )((s, ), g'), if g'  GS(((s, )) and g  g'.

Considering the input alphabet G, we further extend the transition and output functions to the set of all possible input sequences in G*. The extended transition function describes the set of all possible states which a deterministic machine from a given state can reach in response to input sequence and the extended output reaction function gives the set of all possible corresponding output sequences; these sets are singletons if the input sequence is admissible for the starting state. We define the function

 : S  G*  2 S as follows. Given s  S and   G*, we let (s, ) be {(s, ) |  ,   S(s)}. Obviously, for any   S(s), (s, ) = {(s, )}. Similarly, we define the function : S  G*  2 O* . For s  S and   G*, we define (s, ) = {(s, ) |  ,   S(s)}.
We call the functions  and  the extended transition and output functions. For any

  S(s), (s, ) = {(s, )}. Given a set of symbolic input sequences   G*, the SIFSM S is said to be a -converter if for each   , |(s 0 , )| = 1.
Given input sequence , we use pref() to denote the set of all prefixes of .

Similar, pref(A) denotes the set of prefixes of sequences in

A. The set A is prefix- closed if pref(A) = A.

Relations Between SIFSMs

In this section, we extend the classical equivalence and distinguishability relations to SIFSMs and introduce new types of distinguishability which have no counterparts in the classical deterministic Mealy machine. We define a designated symbolic machine which can be used to check the distinguishability of symbolic input finite state machines.

In this paper, we focus our attention on deterministic systems, in which different output sequences produced by two states in response to the same symbolic input sequence indicate that the two states can be distinguished by the input sequence.

Definition 3. Given states s, sS of S, states s, s S are distinguishable, denoted s ≄ s, if there exist compatible input sequences   S(s) and   S(s), such that (s, ( ))  (s', ( )); the sequence   is called a separating sequence for distinguishable states s and s.

Since the machine is deterministic, its reacts to a given admissible input sequence as it does to any of its reduction. We have therefore the following corollary.

Corollary 1. Any instance of a separating sequence is a separating sequence. The importance of this property of separating sequences becomes evident in the context of testing, as we discussed later.

Given a prefix-closed set of input sequences E G*, we let s ≄ E s to denote the fact that the set E contains a separating sequence. If E contains no separating sequence then states s and s are said to be E-equivalent, denoted s ≃ E s, and if E = G*, then the states are equivalent, denoted s ≃ s'. The machine is reduced if it has no equivalent states. We further assume that the specification machine S is reduced.

As usual, we define equivalence and distinguishability of machines as the corresponding relation between their initial states.

To decide distinguishability we define a designated machine, where, instead of composing transitions caused by the same input as in the case of FSMs [START_REF] Petrenko | Conformance tests as checking experiments for partial nondeterministic FSM[END_REF], we compose transitions with compatible inputs. The machine has the common behavior of the given machines, as the classical automata product (even lifted to symbolic automata [START_REF] Veanes | Applications of symbolic finite automata[END_REF]), but in addition it signals when they disagree on output and enters a sink state.

Definition 4. Given two SIFSMs S = (S, s 0 , V, O, FS, S, S) and P = (P, p 0 , V, O, FP, P, P) over the same set of input variables V, a SIFSM C = (C  {}, c 0 , V, O  {}, FC, C, C), where  is a designated sink state,  is a designated output, is the distinguishing machine for S and P denoted S P, if We further assume that the distinguishing machine is normalized by merging, if needed, transitions with the designated output from the same state. By the definition, any input sequence reaching the sink state of the distinguishing machine is a separating sequence for the given machines; the distinguishing machine could be used

 c 0 = (s 0 , p 0 )  FC  C  G such that for (s, p)  C, g  g  GC(s, p), if g  GS(s), g  GP(p), and g  g    For (s, p)  S  P and g  g  GC(s, p), C((s, p), g  g)  (S(s, g), P(p, g)) and C((s, p), g  g) = S((s, g)), (S(s, g), P(p, g))  S  P if S(s, g)  P(p,
1 2 (xa)/0 (x>a)/1 T/1 3 (xa)/0 (x>a)/1 (x>a)/1 (xa)/1 4 SIFSM S SIFSM P 13 (x>a)/1 24 (xa)/0 23 (xa)/1  (xa)/ (x>a)/1 (x>a)/1
to decide the equivalence of two distinct machines as well as states in the same machine. To illustrate the above we consider the SIFSMs in Figure 1, where x is an input variable, a is a constant, 0, 1 and 2 are outputs and T stands for True.

The machines Sand P are distinguishable, as the distinguishing machine S P shows. The shortest separating sequence is (x  a)(x  a)(x  a). Indeed, in response to it Sproduces 011, while P produces 010.

In this example, we have that the separating sequence is admissible in both machines, as required; however, it is defined only in one of them, namely, (x  a)(x  a)(x  a)P, though (x  a)(x  a)(x  a)S. This sequence is a reduction of the symbolic sequence (x  a)(T)(T) defined in the machine S. Considering the relations between separating and defined sequences we further refine the distinguishability relation.

Definition 5. Given distinguishable states s, s  S of S, s is stronglydistinguishable from s if there exists a separating sequence defined in state s, i.e.,  S(s); if state s is not strongly-distinguishable from state s, then s is said to be weakly-distinguishable from state s.

For two arbitrary states, they could be equivalent, one can be stronglydistinguishable from another, both can be strongly-distinguishable from each other, or both can be weakly-distinguishable from each other. In the last case, they are just distinguishable. Notice that the strongly-distinguishability relationship is not symmetric.

In our example, the machine S is strongly-distinguishable from P, because the separating sequence (x  a)(x  a)(x  a) is defined in P. The machine P, in turn, is weakly-distinguishable from S, since all the separating sequences in the distinguishing machine are not defined in S.

As follows from Corollary 1, if the machines are distinguishable, they are distinguished by any instance of a separating sequence; this is also the case when one machine is strongly-distinguishable from another machine and by the definition the separating sequence is defined in the latter. However, an arbitrary instance of such a sequence may not distinguish a machine that is weakly-distinguishable from another. This difference becomes crucial in conformance testing, when one machine represents a specification and another an implementation under test (IUT). To test the latter, only concrete input sequences would be used, when the IUT is treated as a black box. In the example, assuming that the machine P is the specification and S is the IUT, any instance of the separating sequence (x  a)(x  a)(x  a) can be used to detect nonconformance of the IUT S, as it is not equivalent to P, moreover, S is stronglydistinguishable from P. On the other hand, if the machines swap their roles then since P is weakly-distinguishable from S, then non-conformance of the IUT P cannot be detected by an arbitrary instance of the separating sequence (x  a)(x  a)(x  a).

We formulate a condition under which a SIFSM is either equivalent to or stronglydistinguishable from another SIFSM. It is based on the property of one machine being a converter for all symbolic input sequences defined in another machine. Intuitively, the condition |(m 0 , )| = 1 corresponds to the case when the two machines are equivalent as well as to the case when they produce different output sequences in response to .

Theorem 1. Given a (specification) machine S and an (implementation) machine M, if M is a S-converter then M is either equivalent to or strongly-distinguishable from S.

Proof. Assume that M is a S-converter, i.e., |(m 0 , )| = 1 for each S. As S is deterministic, we have that |(s 0 , )| = 1 for each S. Assume also that M is not strongly-distinguishable from S. Thus, for each S, (m 0 , )  (s 0 , ). It implies that for each S, (m 0 , ) = (s 0 , ), since |(m 0 , )| = |(s 0 , )| = 1. Hence, there is no separating sequence for S and M, i.e., they are equivalent.  Clearly, the sufficient condition is not a necessary one. Consider the machine P in Figure 1 as an IUT and assume that both transitions from state 4 have the output 0. The modified machine is strongly-distinguishable from S, but it has |(m 0 ,(x  a)(T))| = 2.

Symbolic and Concrete Checking Experiments

In this section, we define symbolic checking experiments following a usual framework for defining complete test suite for a given machine, conformance relation, and fault domain [START_REF] Petrenko | Fault models for testing in context[END_REF]. In this case, we are dealing with specification and implementation SIFSMs in a fault domain containing only normalized deterministic input-complete machines; the conformance relation is the machine equivalence. Complete test suite is considered as checking experiment, which could be symbolic or concrete. In the context of symbolic execution and constraint solving, symbolic experiments are of interest for white box testing, while concrete ones for back box testing, where all test data should be concrete. Another specific feature of testing from SIFSM is that a nonequivalent implementation machine in a fault domain can either be weakly-or strongly-distinguishable, which as we show later has a significant impact on fault detection capability of concrete checking experiments. Let (V, m) be the universe of SIFSMs over the input variables V with at most m states. A subset of (V, m) is called a fault domain for a specification machine S = (S, s 0 , V, O, F, , ); it includes SIFSMs which model all possible implementations of S.

A set of input sequences E  S is a checking experiment for S in a fault domain Σ  (V, m) iff S ≃ E M implies S ≃ M, for each M  Σ.
We now define main ingredients of symbolic checking experiments, following the classical approach of state identification.

A symbolic state cover C for the machine S is a set which contains the empty sequence and for each state s  S a single defined input sequence   S, such that (s 0 , ) = s. A symbolic transition cover T for the machine S is a set {g

|   C, g  G((s 0 , ))},
= {Id(s) | s  S}, a symbolic HSI experiment is {γ |   (C  T), γ  Id(δ(s 0 , ))}.
As an example, we construct a symbolic checking experiment for S in Figure 1. The state cover is {, (x  a)}, the transition cover is {(x > a), (x  a), (x  a)(T)}. The symbolic input (x  a) separates states, so

Id(1) = Id(2) = (x  a). Then the HSI exper- iment becomes {(x > a)(x  a), (x  a)(x  a), (x  a)(T)(x  a)}, which could be sim- plified to {(x > a)(x  a), (x  a)(T)(x  a)}.
Recall that we assume that a specification SIFSM S = (S, s 0 , V, O, F, , ) is reduced, normalized, deterministic, and input-complete.

Theorem 2. Let S be a specification SIFSM, an HSI experiment is a checking experiment for S in the fault domain (V, n).

Before proving Theorem 2, we demonstrate some auxiliary results. Lemma 3. Let S = (S, s 0 , V, O, F, S, S) be a specification SIFSM, E be an HSI experiment for S and M = (M, m 0 , V, O, FM, M, M) be a SIFSM from the fault domain (V,

n). If M ≃ E S then M has n states.
Proof. Let s and s' be two states of S. There exist , '  C, such that δS(s 0 , ) = s and δS(s 0 , ') = s'. There also exists   pref(Id(s))  pref(Id(s')), such that , '  E and (s, ) ≠ (s', ); thus, ((s 0 , ), ) ≠ ((s 0 , '), ). As S ≃ E M, we have that (s 0 , ) = (m 0 , ) and (s 0 , ') = (m 0 , '). Hence, ((s 0 , ), ) = ((m 0 , ), ) and ((s 0 , '), ) = ((m 0 , '), ). Thus, ((m 0 , ), ) ≠ ((m 0 , '), ) and, therefore, (m 0 , ) ≠ (m 0 , '). We conclude that for each pair of states of S, there exists at least a pair of states of M which are distinct. Therefore, M has at least n states. As M  (V, n), M has at most n states. Thus, M has n states.  Lemma 4. Let S = (S, s 0 , V, O, FS, S, S) be a specification SIFSM, E be an HSI experiment for S and M = (M, m 0 , V, O, FM, M, M) be a SIFSM from the fault domain

(V, n). If M ≃ E S then there exists a bijection f : S  M, such that for each  (C  T), f((s 0 , )) = (m 0 , ).
Proof. C contains n symbolic input sequences, one for each state of S. By Lemma 3, M has n states. Thus, we can define a bijection f : S  M, such that for each  C, f((s 0 , )) = (m 0 , ). It thus remains to show that for each   T, we also have that f((s 0 , )) = (m 0 , ). Let   T and s = (s 0 , ). There exists   C, such that s = (s 0 , ). We have that f(s) = (m 0 , ). Let '  C, such that s' = (s 0 , ') ≠ s. Thus, f(s') = (m 0 , '). There also exists   pref(Id(s))  pref(Id(s')), such that , '  E and (s, ) ≠ (s', ); thus, ((s 0 , ), ) ≠ ((s 0 , '), ). As S ≃ E M, we have that (s 0 , ) = (m 0 , ) and (s 0 , ') = (m 0 , '). Hence, ((s 0 , ), ) = ((m 0 , ), ) and ((s 0 , '), ) = ((m 0 , '), ). Thus, ((m 0 , ), ) ≠ ((m 0 , '), ) and, therefore, (m 0 , ) ≠ (m 0 , ') = f(s') and (m 0 , ) ≠ f(s'). It follows that f(s) = (m 0 , ) and, thus,

f((s 0 , )) = (m 0 , ).  Corollary 2. If M ≃ E S then for any ,   S, if (s 0 , ) = (s 0 , ) then (m 0 , ) = (m 0 , ).
Proof. Let M ≃ E S and ,   S, (s 0 , ) = (s 0 , ). First, we prove by induction on the prefixes of  that there exists a sequence   C, such that (s 0 , ) = (s 0 , ) and (m 0 , ) = (m 0 , ).

For the base case, we have  = . As   C, the property holds for  =  = , since obviously (s 0 , ) = (s 0 , ) and (m 0 , ) = (m 0 , ).

For the inductive case, assume that  = 'g and there exists '  C, with (s 0 , ') = (s 0 , ') and (m 0 , ') = (m 0 , '). We have that 'g  T. As C is a state cover for S, there exists   C, such that (s 0 , 'g) = (s 0 , ); hence (s 0 , ) = (s 0 , ). Thus, due to the properties for the bijection f, it follows that f((s 0 , 'g)) = (m 0 , 'g) and f((s 0 ,

)) = (m 0 , ). It then follows that (m 0 , ) = (m 0 , 'g) = f((s 0 , 'g)) = f((s 0 , )) = (m 0 , ), hence (m 0 , ) = (m 0 , ), concluding the induction proof.
In the same vein, we can prove that there exists a sequence '  C, such that (s 0 , ) = (s 0 , ') and (m 0 , ) = (m 0 , '). As (s 0 , ) = (s 0 , ) and C contains only one sequence that reaches each state, we have that  = '. Thus,

(m 0 , ) = (m 0 , ) = (m 0 , ') = (m 0 , ), i.e., (m 0 , ) = (m 0 , ). 
Now we are ready to prove Theorem 2. Proof of Theorem 2. Let M = (M, m 0 , V, O, FM, M, M) be a SIFSM from the fault domain (V, n), such that M ≃ E S. We prove by contradiction that M ≃ S. Assume that M ≄ S. Let  be the shortest symbolic input sequence such that M ≃ {} S and there exists g  G* such that g is a separating sequence, i.e., M ≄ {g} S. Thus, ((m 0 , ), g) ≠ ((s 0 , ), g).

Since E is an HSI experiment {γ |   (C  T), γ  Id(δS(s 0 , ))}, it contains a sequence   C, such that (s 0 , ) = (s 0 , ). Then (m 0 , ) = (m 0 , ), according to Corollary 2. Since ((m 0 , ), g) ≠ ((s 0 , ), g), it also holds that ((m 0 , ), g) ≠ ((s 0 , ), g). The HSI experiment contains a transition cover of S then there exists a symbolic input g, such that ((s 0 , ), g)  FS, g gand g  E. M ≃ E S implies that M ≃ {g} S. We have that (m 0 , ) = (m 0 , ), then ((m 0 , ), g) = ((s 0 , ), g). This contradicts the assumption that ((m 0 , ), g) ≠ ((s 0 , ), g), as g g For simplicity, we have considered symbolic experiments for the fault domain (V, n). Nevertheless, based on the previous results, e.g., [START_REF] Simao | Generating reduced tests for FSMs with extra states[END_REF], [START_REF] Vasilevskii | Failure diagnosis of automata[END_REF], the case of a wider fault domain (V, m), where m > n can also be considered.

Symbolic experiments could be used in the context of white-box testing when symbolic execution of code/model of an implementation SIFSM is possible; however, they cannot be executed against an implementation SIFSM considered as a black box. We further assume that only instances of symbolic experiments can be executed against any implementation SIFSM in a given fault domain.

Consider first the case, when an SIFSM S has a finite number of concrete inputs, in other words, it is a compact representation of a Mealy FSM S over the finite input set D V . Then the set of all possible instances of a symbolic checking experiment is finite and is in fact a concrete checking experiment for the SIFSM S. The latter is also a classical checking experiment for the FSM S.

Theorem 3. Given a specification machine S with a finite input set D V , let E be a symbolic checking experiment for S in (V, n). Let also E' be the set of all possible instances of E and S be the FSM obtained by unfolding S. Then, E' is a concrete checking experiment for S and S in (V, n).

Proof. As E is a symbolic checking experiment for S in (V, n), for each M in (V, n), E contains a separating sequence  distinguishing S and M. Thus, there exists an instance of  which distinguishes S and M and E' contains this instance; hence E' distinguishes S and any SIFSM in (V, n) which is distinguished by E. As E is a symbolic checking experiment for S in (V, n), it follows that E' is a checking experiment for S in (V, n). As S' is equivalent to S, we have that E' is also a checking experiment for S' in (V, n). 

The theorem suggests that checking experiments for SIFSMs with a finite set of concrete inputs can be constructed directly from a given specification machine without first unfolding it into a classical Mealy machine and using one of the existing methods for checking experiment generation. It might also be computationally simpler to first determine all the ingredients of a checking experiment in the symbolic form and then generate all the concrete instances of symbolic sequences one by one.

Next we consider the case when the input variables do not yield a finite set of concrete inputs and we investigate faults detectable by concrete experiments. Since we can execute only a finite number of concrete input sequences, it is interesting to know in which cases the set of single instances of each sequence in a symbolic checking experiment remains a checking experiment for a given fault domain. In the following, we identify several such cases.

Let E be a symbolic checking experiment for S in (V, n) and let  be a subset of (V, n). We say that E is safely-instantiable for  if any instance of E is a concrete checking experiment for S in . We will use (V, n, S) to denote the subset of (V, n), which consists of S-converters.

Theorem 4. Let E be a symbolic checking experiment for S in (V, n). Then, E is safely-instantiable for (V, n, S).

Proof. Let M (V, n, S); thus, for each S, |(m 0 , )| = 1. According to Theorem 1, the machine M is either equivalent to or strongly-distinguishable from S. Let C be an instance of E. Assume that M is not equivalent to S; thus, M is stronglydistinguishable from S. As E is a symbolic checking experiment for S in (V, n) and (V, n, S)  (V, n), there exists a symbolic separating sequence   E, such that M ≄ {} S; by Corollary 1, any instance of the sequence  is also a separating sequence. Thus, the result follows.  Theorem 4 says that any concrete experiment derived from a symbolic checking experiment is also a checking experiment for the machine S in the fault domain (V, n, S). In other words, a complete concrete test suite can be obtained from a symbolic checking experiment. The question arises as to which structural faults in the implementation machines preserve their property of being S-converters. Addressing this question, we follow the same approach for describing faults as in the classical deterministic Mealy machines, see, e.g., [START_REF] Bochmann | Fault models in testing[END_REF], [START_REF] Petrenko | Test suite generation for a given type of implementation errors[END_REF]. Implementation faults are usually modeled by mutants of a given machine. Elements of transitions, namely, output and end state, are subjects for mutations, which yield output faults, transfer faults and transition faults combining the first two types of faults.

It is not difficult to see that all possible mutants of the specification SIFSM S with output faults are S-converters, i.e., they are in the fault domain (V, n, S).

As to transition faults, they should not violate the property of S-converters, namely, a mutant with transition faults should react to any symbolic input sequence defined the specification with a single output sequence. It turns out that mutants with transition faults remain to be S-converters under the following conditions.

Assume that the specification SIFSM S has a fixed set of guards in each and every state, i.e., G(s) = G(s) = GS for all states s, s  S. Let GM denote the set of guards of an implementation SIFSM M with the same property.

Theorem 5. Given a specification SIFSM S with the set of guards

GS then {M  (V, n) | GM = GS}  (V, n, S). Proof. Let M  (V, n), such that GM = GS. Indeed, GM = GS implies M = S. As (V, n) includes only deterministic machines, we have that |(m 0 , )| = 1 for each M; therefore |(m 0 , )| = 1 for each S. Thus, M  (V, n, S). 
We identify another sufficient condition considering the case when the set of defined input sequences of each implementation machine in a fault domain is a superset of that of the specification machine. Intuitively, an implementation machine is assumed to preserve in each state guards of the specification or merge some of them. Theorem 6. Given a specification SIFSM S, it holds that {M  (V, n) | S, g GS((s 0 , )),  g GM((m 0 , )), g g}  (V, n, S).

Proof. Let M  (V, n), such that for each S and each g GS((s 0 , )), there exists g GM((m 0 , )) such that g g. We prove by induction that for each   S, |(m 0 , )| = 1.

For the basis step, we have that (m 0 , ) = {}, i.e., |(m 0 , )| = 1. For the induction step, assume that  = g  S and |(m 0 , )| = 1. Let also g GS((s 0 , )), g GM((m 0 , )), such that g g. We can see that |((m 0 , ), g')| = 1; thus |((m 0 , ),

g)| = 1. Consequently, |(m 0 , g)| = 1, i.e., |(m 0 , )| = 1; therefore, |(m 0 , )| = 1 for each S. Thus, M  (V, n, S). 
This theorem addresses a specific fault model of symbolic implementation machines representing the mutation by merging transitions along with their guards which is not possible in classical FSM, since an implementation FSM should have all the inputs of a specification FSM. In case of SIFSMs, implementation machines have all the input variables of a specification machine, but not necessarily its guards.

Consider SIFSMs in Figure 1. The machine S can be considered a mutant of the specification machine P, where transitions with guards (x  a) and (x > a) are merged into a transition with the guard T. On the other hand, when the machine S serves as a specification and the machine P is an implementation this mutant has a specific fault of splitting a guard used in the specification SIFSM. To detect such a fault, one has use to use at least two instances of a symbolic input sequence from the checking experiment. Since P is treated as a black box testing, and the way a guard is split is unknown, two concrete tests suffice if they properly "guess" it.

Conclusions

We investigated possibilities for lifting the checking experiments theory developed for the classical (Mealy) finite state machine model to its extension, where input alphabet is finite, but consists of predicates defined over input variables with large or even infinite domains. We call it FSM with symbolic inputs, SIFSM. On one hand, this model can be considered as a special type of Extended FSMs (EFSMs) [START_REF] Petrenko | Confirming configurations in EFSM testing[END_REF], without context variables and operations on variables; on another hand, as symbolic automaton or symbolic transducer [START_REF] Noord | Finite state transducers with predicates and identities[END_REF], [START_REF] Veanes | Symbolic finite state transducers: algorithms and applications[END_REF]. The recent grow of interest towards symbolic models could be explained by advances in constraint solving technology, as SMT solvers become efficient [START_REF] Moura | Z3: An efficient SMT solver[END_REF]. We lifted the machine equivalence and distinguishability relations to SIFSM and identified new distinguishability relations which have no counterparts in classical deterministic Mealy machines. Then, we defined symbolic checking experiments for deterministic SIFSMs and demonstrated that they could be obtained by mimicking, e.g., a classical HSI method for constructing checking experiments of FSMs (other types of state identification facilities, such as W and Wp, might also be used). Since symbolic experiments could be used for white-box testing, but not for black-box testing, which requires concrete test values, we focused on investigating fault domains for which any concrete instance of a symbolic checking experiment remains a checking experiment.

As expected, in the most general setting, an arbitrary instance of a symbolic checking experiment may not be a checking experiment in the same fault domain. Nevertheless, we found some sufficient conditions for the specification and implementation machines under which any instance of a symbolic checking experiment is also a checking experiment in well-defined fault domains. Under these conditions, nontrivial faults modeled by the identified fault domains are detectable by concrete tests obtained from abstract (symbolic) tests in a symbolic checking experiment. These faults include transition merging, which is only relevant to implementations of SIFSM and not to classical Mealy machines.

The novelty of the results comes from the fact that while FSM checking experiments are known for about 60 years, EFSMs for about 30 years, there are no published results on checking experiments for EFSM which cannot be unfolded into FSM. To the best of our knowledge, it is the first attempt to advance the checking experiment theory to FSMs with a symbolic extension.

While the problem of handling more general EFSMs remains open, we believe that the presented results open a new line of research in checking experiments for symbolic state machines and transition systems.

Our current work concerns, on one hand, relaxing the sufficient conditions of safeinstantiability, and on the other hand, extending the SIFSM model with operations on output variables, thus lifting the checking experiments theory to a wider class of extended finite state machines. We also plan to investigate other fault models for which symbolic checking experiments could be used as efficiently as for the faults satisfying the formulated sufficient conditions.

Fig. 1 .

 1 Fig. 1. SIFSMs S, P, and the distinguishing machine SP.

  where C is a symbolic state cover.

	exists a
	separating sequence   pref(Id(s))  pref(Id(s')). A straightforward way of con-
	structing HSIs is to determine a distinguishing machine for each pair of states and
	include the found sequence in the identifiers of the states in the pair.
	Given a symbolic state cover C, a symbolic transition cover T and a set of harmo-
	nized state identifiers H

Given state s  S of the reduced machine S, a finite set E  S(s) is a state identifier for s, denoted Id(s), if s ≄ E s for each s'  s. State identifiers in a set H = {Id(s) | s  S} are harmonized if for each pair of distinguishable states s and s', there

Acknowledgements. The first author acknowledges financial support of NSERC via Discovery grant RGPIN/194381-2012. The second author had financial support of Brazilian Funding Agencies, CNPq, Capes and FAPESP.


Sylvain Hallé

Edmond La Chance

Sébastien Gaboury

Graph Methods for Generating Test Cases with Universal and Existential Constraints

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

Introduction

In recent years, combinatorial testing has gathered increasing interest as a testing technique that can exercise interactions between parameters in an efficient way. Various testing tools, such as PICT [START_REF] Mccaffrey | Pairwise testing with QICT[END_REF], have been developed to produce a series of test cases that cover all interactions of t parameters through a test suite containing as few tests as possible. Various approaches attempt to expand the problem by providing constraints on what values each parameter can take; for example, one may require that when a = 0, then b = 0, thereby limiting the number of valid test cases that are available. A variety of tools support constraints of such kind, which must be fulfilled by every test case returned by the tool.

However, the problem of generating test cases where a set of conditions has to be fulfilled at least once by some test has seldom been studied. In this paper, we introduce the concept of Φ-way covering, a generalization of classical t-way test case generation where each Boolean condition in an arbitrary set must be validated by at least one test case. Section 2 formally defines Φ-way covering, and shows a number of testing scenarios where existential (rather than universal) constraints are required, and which cannot be handled by current combinatorial test generators.

In Section 3, we show how Φ-way test case generation can be reduced to finding a colouring of some graph, and link the minimal number of tests to its chromatic number. However, this reduction is shown to work only when the resulting graph satisfies a property called maximal satisfiability. Therefore, in Section 4, we construct a second reduction, this time to the problem of hypergraph vertex covering, which drops the maximal satisfiability requirement and works for arbitrary conditions. Moreover, this second construction also allows us to handle universal constraints that are supported by existing combinatorial testing tools and algorithms.

We have implemented a test-generation tool that uses our graph-based approaches to produce a set of test cases for parameters with arbitrary domains. Experimental results, presented in Section 5, show that a straightforward application of existing graph heuristics, without any further optimization, already produces test suites whose size is comparable to the output of existing tools, and in particular shares the same asymptotic complexity, both in terms of the number of attributes and the number of values. Moreover, this is obtained while our proposed solutions solve a more general problem than existing tools, as they allow both universal and (most importantly) existential conditions on test cases.

Φ-way Covering

In this section, we introduce the problem of Φ-way test covering and describe a number of testing scenarios where such form of test covering naturally arises.

Formalization

Let D 0 , D 1 , . . . D n-1 be domains (sets of possible values) for n different parameters p 0 , . . . , p n-1 . Let Φ = {ϕ 0 , . . . , ϕ m-1 } be a set of m Boolean formulae whose ground terms are of the form p i = d, for p i one of the parameters and d ∈ D i . A Φ-way covering is a set Σ ∈ 2 D0ו••×Dn-1 , such that for every ϕ i ∈ Φ, there exists an assignment of values σ ∈ Σ that makes ϕ i evaluate to true (which we shall note σ |= ϕ i ).

One can see how this problem is a generalization of classical t-way test case generation. Given parameters p 0 , . . . , p n-1 with domains D 0 , D 1 , . . . D n-1 , we can construct Φ as the smallest set such that for every set of t parameters p 1 , . . . , p t and values d 1 , . . . , d t in their respective domains, the formula

p 1 = d 1 ∧• • •∧p t = d t is in Φ.
Since the resulting Φ-way covering ensures that every formula in Φ is true, it follows that every combination of values for t parameters is present in the set. As an example, Table 1 gives the set of constraints representing the 2-way covering of the set of parameters a, b and c, each having two possible values.

However, we can show that Φ-way covering is a strict generalization of tway test case generation, as finding one solution to the problem is in the same complexity class as finding the best solution for a t-way test case generation problem [START_REF] Tai | A test generation strategy for pairwise testing[END_REF].

Theorem 1 Finding a solution to the Φ-way Covering problem is NP-complete.

Proof. Given a set Σ, verifying that each ϕ i ∈ Φ is satisfied at least once amounts to evaluating it with every σ ∈ Σ, which is done in polynomial time; hence the problem is in NP. Solving Φ-way covering when Φ consists of a single Boolean expression ϕ is nothing but solving the satisfiability problem (SAT) for ϕ; hence the problem is NP-hard.

{a = 0 ∧ b = 0, a = 0 ∧ b = 1, a = 1 ∧ b = 0, a = 1 ∧ b = 1, a = 0 ∧ c = 0, a = 0 ∧ c = 1, a = 1 ∧ c = 0, a = 1 ∧ c = 1, b = 0 ∧ c = 0, b = 0 ∧ c = 1, b = 1 ∧ c = 0, b = 1 ∧ c = 1}

A Case for Φ-way Covering

While t-way test case generation has proved useful in many scenarios, it was shown how in some situations, constraints must be added to the original tway requirement to correctly handle the problem at hand. Current tools and algorithms have focused up to now on universal constraints, which must hold true on every test case of the test suite. For example, in some situations, a combination of values for two parameters might be mutually exclusive: one can imagine a function which can send its output either to stdout or to a file; it does not make sense, in such a case, to set the output parameter to stdout, and to have a non-empty value for parameter filename. This constraint must apply to every test case produced by an algorithm.

However, the question of existential constraints, as is the case in the Φ-way covering presented above, has been studied much less often. Yet, in the following, we show three test case scenarios where such constraints are required -that is, the same functionality cannot be obtained, or expressed differently, using only universal constraints.

Example 1: Completing an existing test suite As a first example, suppose we have an existing test suite, which does not cover all t-combinations of values. One would like to extend that test suite, keeping existing test cases but adding the minimum number of new tests so that 100% coverage of all t-combinations is achieved. 1 Imagine for example parameters a, b and c, each with domain {0, 1}, and a test suite T composed of only two tests: {(a = 0, b = 0, c = 0), (a = 0, b = 0, c = 1)}.

To find an extension to that test suite, it suffices to first generate the set Φ of conditions corresponding to t-way coverage as described above (for example, for t = 2, we obtain the set in Table 1). We then create one existential condition for each test in T ; in the present case, this would lead to the addition of conditions a = 0 ∧ b = 0 ∧ c = 0 and a = 0 ∧ b = 0 ∧ c = 1 to Φ. We then solve the Φ-way covering problem. By construction, any minimal solution for this problem is the smallest way to obtain t-way covering while preserving the existing tests. With a graph theory approach, completing a test suite is faster than producing one from scratch because the generated graph is smaller.

Example 2: Equivalence classes In some cases, the original requirement of t-way coverage might prove needlessly strict. Φ-way coverage allows one to relax these conditions, while still looking for an optimal test suite. Consider for example parameters a, b and c with domains {0, . . . , 9}, {0, 1} and {0, 1}, respectively. Suppose that some values of a are equivalent in its relationship with b; for example, all values of a < 5 behave in the same way when b = 0. In other words, when b = 0 and c has some arbitrary values, all values of a < 5 exercise the same functionality, and do not need to be tested separately.

It is not possible to express such a fact using standard t-way test covering algorithms, which will produce an overly strong (and large) test suite, as they will try to cover all combinations of values for a, b, and c. Moreover, it is not possible either to recover from this issue by writing universal constraints, unless one forces the selection of one value for a when b = 0, which in turn might prevent the resulting test suite from being optimal. Finally, one can imagine more complex dependencies on parameter values where imposing fixed values to parameters in an optimal way amounts to nothing but hard-coding the solution by hand inside the constraints.

On the other hand, this situation is nicely handled in Φ-way covering. When generating the set Φ of constraints for t-way covering, it suffices to replace all conditions a = x ∧ b = 0 ∧ c = x (where x i < 5 and some fixed value x ) by the single condition a < 5 ∧ b = 0 ∧ c = x , and then to solve the resulting Φ-way problem.

The reader shall remark that the same thing can be achieved by replacing the values 0 to 4 in the domain of a by a symbolic value meaning "a < 5", and to solve the corresponding t-way problem. Indeed, all combinations of values of parameters a and c are still considered distinct; these combinations will be missed if values 0 to 4 are amalgamated into a single symbol.

Example 3: MC/DC testing

The modified condition/decision coverage [START_REF] Hayhurst | A practical tutorial on modified condition/decision coverage[END_REF] (MC/DC) is a code coverage criterion for test cases which, among other things, requires that each condition in a decision takes on every possible outcome, and that each condition in a decision is shown to independently affect the outcome of the decision.

The question of performing both t-way testing and MC/DC testing in a single test suite has only been recently studied [START_REF] Vilkomir | Relationship between pair-wise and MC/DC testing: Initial experimental results[END_REF]. Current approaches have measured the amount of MC/DC coverage provided by a t-way test suite, without providing any specific adaptation of existing algorithms for MC/DC coverage (and vice versa). Therefore, any good MC/DC coverage obtained by a t-way test suite is, for the moment, unintentional.

However, this can be handled with Φ-way covering. One first generates the set Φ of conditions required for t-way coverage, as was described earlier. To obtain MC/DC coverage, one simply adds to Φ the conditions corresponding to MC/DC. By construction, any solution to the resulting problem will make sure that each of the t-way conditions is met by at least one test case, and that each of the MC/DC conditions will also be met by at least one test case. Note that this may result in more test cases than for any problem taken separately; however, any minimal solution of the combined problem is guaranteed to be optimal.

Reduction to Graph Colouring

Assuming a few restrictions on the set of conditions Φ, we shall now show how the problem of generating Φ-way test cases can be reduced to a well-known graph problem.

Construction

Given a set of Boolean formulas Φ, the conjunctive closure of Φ is the smallest set

Φ ⊇ Φ such that if ϕ, ϕ ∈ Φ , then ϕ ∧ ϕ ∈ Φ . 2 A
set Φ is said to be maximally satisfiable if every formula in its conjunctive closure is satisfiable.

We shall now devise a construction that reduces the problem of Φ-way covering to the problem of graph colouring. Let G = V, E be a graph such that V = Φ, and E is such that there is an edge between two vertices ϕ, ϕ if and only if ϕ ∧ ϕ is unsatisfiable. Let C be a set of vertex "colours" and κ : V → C a function assigning a colour to every vertex of the graph. For k = |C|, the function κ is called a k-colouring if it is surjective and moreover, any two adjacent vertices are not assigned the same colour. We will define V c ⊆ V as the set of vertices that are assigned colour c by κ (and by extension, the set of all Boolean expressions assigned to these vertices). Figure 1 shows an example of such a colouring, for the set of constraints given in Table 1.

Theorem 2 Let Φ be a set of formulae, G be the graph constructed from Φ as described above and κ be a k-colouring of G. If V c is maximally satisfiable for every c ∈ C, then there exists a Φ-way covering Σ such that |Σ| = k.

Proof. Define Φ c as the conjunction of all expressions in V c . One can construct a test case from V c by choosing any satisfying assignment of variables of Φ c . Such an assignment exists, since V c is maximally satisfiable. Let Σ be the set of all test cases constructed in such a way, for every colour c ∈ C. Since every vertex is given a colour, taken together, the test cases in Σ satisfy every condition of Φ at least once, and hence constitute a Φ-way covering.

a=0 ∧ b=0 a=1 ∧ b=0 a=1 ∧ b=1 a=1 ∧ c=0 a=1 ∧ c=1 a=0 ∧ b=1 b=1 ∧ c=0 b=1 ∧ c=1 b=0 ∧ c=0 b=0 ∧ c=1 a=0 ∧ c=0 a=0 ∧ c=1
Fig. 1: The graph constructed from the constraints given in Table 1, and a possible 5-colouring.

This result shows that a minimal Φ-way coverage can be computed by converting the problem into the classical graph colouring problem, provided that the resulting colouring produces maximally satisfiable sets of vertices. This is not always true in the general case; Figure 2 shows a graph whose colouring is not maximally satisfiable. One can see that for every pair of vertices, it is possible to find values for a and b that satisfy both conditions; this is why no vertex is connected to any other. Hence it is possible to assign the same colour to every vertex; however, one can see that the conjunction of the condition of all three nodes is a contradiction -in other words, it is not possible to form a test case out of it. a=0 ∨ b=0 a=1 b=1

Fig. 2: A graph whose colouring is not maximally satisfiable.

However, we can show that a colouring is always maximally satisfiable if we impose restrictions on Φ.

Theorem 3 Let Φ be a set of Boolean formulae {ϕ 1 , . . . , ϕ n }, where each ϕ i is a conjunction of atomic propositions of the form p j = d. If ϕ i ∧ ϕ j is satisfiable for any pair of formulae ϕ i , ϕ j ∈ Φ, then Φ is maximally satisfiable.

Proof. Suppose the contrary. Then there exists a set S ⊆ 2 [1,n] of indices such that i∈S ϕ i is unsatisfiable. Since every ϕ i is a conjunction of parameter-value equalities, this entails that there exist two assertions p j = d and p j = d such that

d = d . Let k, k ∈ [1, n]
such that the first assertion occurs in ϕ k and the second occurs in ϕ k . Then ϕ k ∧ ϕ k is unsatisfiable, which contradicts the hypothesis.

Complexity Results

This result has a couple of important consequences. First, we can show that any classical t-way covering problem generates a graph that satisfies the hypotheses of Theorem 3.

Corollary 1

Let G = V, E be a graph generated from a t-way problem instance and let κ : V → C be a colouring of G as defined above. For any colour c ∈ C, V c is maximally satisfiable.

Proof. Since every vertex in V c is a conjunction of expressions of the form p j = d, the result follows from Theorem 3.

Hence finding a set of k test cases, if it exists, can be solved by converting the problem to k-colouring. Second, and perhaps most importantly, the previous construction provides us with a means of calculating the exact lower bound to the number of tests required to achieve t-way coverage. This bound is nothing but the chromatic number of the graph. Moreover, it is possible to compute this optimal size without even generating the solution, by constructing the chromatic polynomial of the graph; the chromatic number (and hence the smallest number of tests cases required) is the smallest integer that is not a root of this polynomial.

The current best known algorithm can find a k-colouring in time O(2 n • n), where n represents the number of constraints. Given the chromatic number can be known directly through the method described above, this gives us the same complexity for generating a minimal set of test cases. In the absence of the known value, one can fall back on simple dichotomic search, as the desired value k lies between 1 and C(t, n) × |D| t , the total number of combinations for values of t parameters.

Heuristics for Graph Colouring

One main advantage of reducing the test case generation problem to an existing mathematical problem is that one can then tap directly into a number of optimizations specific to that problem, rather than trying to solve it from scratch. This is precisely the case for graph colouring, which has been the subject of extensive study for decades. In particular, a number of methods for computing an approximate solution, called heuristics, can be used to produce a test suite whose size can be bounded in terms of the size of the optimal solution.

The most well known heuristic for graph colouring is DSATUR from Brélaz [START_REF] Brélaz | New methods to color the vertices of a graph[END_REF]. This heuristic is partially built on the observation that more often than not, vertices with a bigger degree generally end up with a colour of their own instead of being assigned an existing colour. The algorithm starts out by selecting the biggest degree vertex, colouring it, and then it colours the neighborhood of that vertex using the DSAT (Degree Saturation) measure. When the DSAT of two vertices is the same, the degree is used for tie-breaker. The DSAT of all vertices is updated at every colouring of a vertex. The DSAT of a vertex is an integer representing how many adjacent colours are in the neighborhood.

The DSATUR heuristic is unfortunately not great for combinatorial testing because in the generated graph files, every graph node has the same degree. Therefore, the heuristic cannot really work like it is supposed to.

The depth-first search (DFS) greedy heuristic is perhaps the most simple heuristic of all. The graph is simply explored in a typical depth-first-search fashion and the colours are assigned turn by turn. The quality of the solution depends exclusively on the sequence of the vertices. In fact, the DFS algorithm can be modified into an exact backtracking algorithm. For instance, if the backtracking algorithm is called with the task of finding a 13-colour permutation and the current colour count is 14, it does not make any sense to keep colouring the graph. The algorithm needs to backtrack and change it's permutation until it can colour the whole graph with the proper number of colours. This backtracking algorithm is almost impossible to use in practice for combinatorial testing because the graphs are too big.

Since trying every path leads to the exact solution, sampling the paths by using randomness is also a good way to go and leads to better solutions than greedy algorithms. The random DFS heuristic works in this way. For each vertex exploration, the neighborhood will be explored in a random way a number of times. When the k random explorations fail, the algorithm falls back to regular neighborhood exploration, until it can return or go to the next vertex. This is done because of course, true random exploration could slow the algorithm to a stall.

Since adding randomness to the DFS exploration scheme turns out to be very cheap and not increasing the time complexity, this heuristic is usually ran hundreds of times and the best result is used.

Reduction to Hypergraph Vertex Cover

As we have seen in the previous section, the graph colouring approach can only be applied when the set of assertions resulting from the initial constraints is maximally satisfiable. Yet, there exist situations where this additional hypothesis does not hold. In this section, we present an alternate method that attempts to alleviate this problem.

This method is a reduction of the Φ-way covering problem to finding a vertex covering of some hypergraph. As a reminder, a hypergraph is a tuple G = V, E , where V is a set of vertices and E ⊆ 2 2 V is a set of edges. A hypergraph generalizes a classical graph by having edges that may link more than two vertices. A vertex covering of some hypergraph G = V, E is a set of vertices V ⊆ V , such that for every edge e = {v 0 , v 1 , . . . , v k } ∈ E, we have that e ∩ V = ∅. Hence every hyperedge of the graph is adjacent to at least one vertex in V .

Construction

Given parameters p 0 , . . . , p n-1 with domains D 0 , D 1 , . . . D n-1 , let Φ be a set of Boolean constraints whose ground terms are parameter-value equalities. Define

V = D 0 × D 1 × • • • × D n-1
as the set of all possible combinations of values for each parameter. The set of hyperedges E is then constructed such that e = {v 0 , v 1 , . . . , v k } ∈ E if and only if there exists some ϕ ∈ Φ, such that v i ∈ e if and only if v i |= ϕ. In other words, each condition ϕ ∈ Φ is associated to exactly one hyperedge, linking all vertices giving values for parameters that make that condition evaluate to true. One can see that the hyperedge labelled "1" links all vertices with values satisfying the first condition (a = 0); similarly, the hyperedge labelled "2" links all vertices with values satisfying the second condition (b = 0). Finally, the hyperedge labelled "3" links all vertices with values satisfying the last condition (a = 0 ∨ b = 0); this last edge links three vertices.

We shall now demonstrate how one can extract a Φ-way covering out of a vertex cover. Theorem 4 Let p 0 , . . . , p n-1 be parameters with domains D 0 , D 1 , . . . D n-1 , and Φ be a set of Boolean constraints whose ground terms are parameter-value equalities. Let G = V, E be the hypergraph constructed from a set of conditions Φ as described above, and let V be a vertex covering for G. There exists a set

Σ ⊆ D 0 × D 1 × • • • × D n-1 that is a Φ-way covering; moreover, this set is of size |V |.
Proof. It suffices to show that Σ = V is the set we are looking for. By construction, every hyperedge of G is adjacent to some v ∈ V . By construction, this entails that for every ϕ ∈ Φ, there exists a combination of parameter values v such that v |= ϕ, hence V is a Φ-way covering.

In Figure 3, vertices forming a possible covering of size 2 have been identified in yellow. One can see how every hyperedge is indeed adjacent to some yellow vertex. Moreover, it is easy to see that no covering of size 1 could achieve the same result. Hence, finding the the minimal Φ-way covering amounts to finding the minimal vertex covering of the hypergraph G constructed from Φ.

Universal constraints Contrary to the graph colouring reduction described in Section 3, the reduction to hypergraph vertex cover works for arbitrary existential conditions, thus dropping the requirement for maximal satisfiability that was necessary in the former. Moreover, universal conditions (which must be true for every test case) can also be taken into account in a very straightforward way. Given a set Φ of such constraints, it suffices to remove from V any vertex for which one of the constraints in Φ evaluates to false. Since each vertex completely defines the values of all parameters, such an evaluation is always possible, and the fate of every vertex can always be determined. The computation of a vertex cover can then proceed on the pruned graph.

By construction, all vertices in the graph that remains fulfill all the conditions in Φ . In addition, the vertex cover guarantees that each hyperedge (i.e. each existential condition) is covered at least once. Hence this construction allows us to handle both arbitrary universal and arbitrary existential conditions at the same time.

Complexity Results

We have already shown that finding a vertex covering of a given size k is NPcomplete. However, finding the minimal value such that a covering exists is a much harder problem in the general case. Providing the latest complexity results for this problem is out of the scope of this paper, as abundant literature on the subject can easily be found. It is known, for example, that if d is the maximal cardinality of hyperedges and n is the size of the hypergraph, there exists an algorithm that finds a covering of size k in time d k n O (1) [START_REF] Flum | Parameterized Complexity Theory[END_REF].

Upper bounds have also been demonstrated for approximation algorithms. For example, one can construct a maximal matching by greedily adding edges and then let the vertex cover contain all endpoints of each edge in the matching. It can be shown that this algorithm produces a vertex covering at most d times larger than the optimal solution. For d = 2, a slightly lower factor of 2 -o(1) has been demonstrated [START_REF] Halperin | Improved approximation algorithms for the vertex cover problem in graphs and hypergraphs[END_REF][START_REF] Karakostas | A better approximation ratio for the vertex cover problem[END_REF].

Hypergraph colouring is equivalent to another problem called hitting set. Given a set of sets of elements E = {e 1 , . . . e n }, a hitting set is a subset V that intersects with every e i ∈ E. When E is the set of hyperedges of G, a hitting set is precisely a set of vertices covering every edge of the hypergraph.

These results can be transferred directly to Φ-way and t-way covering. Given uniform domains of size |D| for each parameter, classical t-way covering for a set of n parameters generates a hypergraph with |D| n vertices whose edges are of uniform cardinality k = |D| n-t . Applying a result from Khot and Regev [START_REF] Khot | Vertex cover might be hard to approximate to within 2[END_REF] which assumes the so-called unique games conjecture, this entails that finding the minimal number of tests is hard to approximate within any constant factor better than k.

Experimental Results

We implemented both approaches into an open source and mixed-language combinatorial test case generator, which is publicly available. 3 First, a PHP script takes as input a file in the PICT format, giving the name of each parameter and its possible values. Since our tool also handles universal and existential constraints, we extended the PICT format to allow the expression of these conditions. They either begin by the reserved word Once or Always, and can express any Boolean combination of elementary condition on the file's declared parameters. Figure 4 shows a sample input file. The script returns a file in the Graphviz format (DOT) representing either the graph for which a colouring needs to be found, or the hypergraph for which a covering must be computed. Then, a C++ implementation of both graph algorithms reads this file and applies the corresponding heuristics, and outputs the resulting colouring or vertex cover, which can then be directly reinterpreted as a set of test cases, as explained earlier.

To assess the interest of the approach, we designed a benchmark pitting our implementation against four other tools: QICT [START_REF] Mccaffrey | Pairwise testing with QICT[END_REF], AllPairs4 , Jenny5 and TCases 6 . These where the only tools listed on the Pairwise Testing website7 that were both free and usable from the command-line. They vary in their support of features outside standard t-way covering, as is illustrated in Figure 5. AllPairs and QICT only work for 2-way covering without constraints. Jenny supports t > 2, and allows the user to specify forbidden tuples, a restricted form of universal constraints, while TCases supports arbitrary universal constraints. Finally, our graph colouring approach handles existential constraints, while the hypergraph vertex cover handles both universal and existential constraints.

The task of exhaustively comparing our proposed implementation with a large sample of existing tools is clearly out of the scope of this paper, especially given that most of these tools are comparable only for the simplest case ( Beyond pairwise: t > 2 The same trend continues when the strength of the test suite is extended beyond pairwise testing. This time, AllPairs and QICT are no longer able to solve these problems, and Jenny, TCases and our two graph solutions remain. As Figures 7a and7b show, our tool produces test suites that are again of size smaller than TCases', and identical to Jenny's. Universal constraints We complexify the tests even further by introducing universal constraints. This time, only TCases and our hypergraph vertex covering can handle such a problem. We experimented both approaches with t = 2, and with the universal constraint ¬(p 3 = 1 ∧ p 4 = 1). The results are given in Table 2. As one can see, the graph-based approach provides smaller test suites of a factor of roughly 2× with respect to TCases's algorithm. Existential constraints In this last category, only the hypergraph approach subsists. We experimented it with t = 2, and with the existential constraint

¬(p 3 = 1 ∧ p 4 = 1)
. The results are given in Table 3. Table 3: Test suite size output by the hypergraph approach, for a varying number of parameters when t = 2.

Related Work

As far as we could check, the problem of generating t-way test cases has never been generalized to account for a set of arbitrary Boolean conditions that must each apply in at least one test. Given some condition ϕ, Φ-way covering requires that there exists at least one test in T that satisfies ϕ, i.e. ∃t ∈ T : t |= ϕ. On the contrary, tools like TCases, PICT, Jenny and VPTag8 to write conditions that must be true for some attribute to be allowed to take a given value, using some form of if-then construct or by specifying forbidden value combinations. A constraint ψ in these tools must be true for all test cases, i.e. ∀t ∈ T : t |= ψ. This is in fact the exact logical dual of Φ-way covering. It follows easily that it is impossible to find ϕ and ψ that make both expressions equivalent for any arbitrary set T . As we have seen, the introduction of Φ-way coverage allows us to express and solve some problem instances that current approaches cannot.

The use of graph colouring for t-way test case generation was first suggested by Cheng et al. [START_REF] Cheng | Generating small combinatorial test suites to cover input-output relationships[END_REF]. However, there are several differences between this related approach and the one suggested here. First, while the approach allows one to pick sets of parameters for which coverage is required, it is assumed that all combinations of their values must be present in the resulting solution. Our construction is more flexible and allows us to express arbitrary tuples of values of irregular length (e.g. a = 0 ∧ b = 0, a = 1). Moreover, graph colouring is used by Cheng et al. only to pick a subset of parameters on which an initial t-way must then be generated by some other means; that solution is then "blown up" to include coverings for the remaining parameters; as a consequence, the minimality of the resulting covering is not ensured.

Recently, an optimization of the IPOG algorithm's vertical growth phase was suggested [12]. This optimization relies on a "conflict graph", whose colouring allows the algorithm to identify the next best missing tuples to add to the test suite. However, to the best of our knowledge, the present paper is the first time the smallest covering array is expressed directly in terms of the minimal colouring of some graph.

The use of hypergraphs for test case generation appears to be even less common. They have been used to reason about orthogonal arrays [START_REF] Raaphorst | A construction for strength-3 covering arrays from linear feedback shift register sequences[END_REF], although not directly to compute an optimal set of test cases.

Conclusion

We have shown how Φ-way covering, a generalization of t-way test case generation, can be reduced to the classical graph colouring problem, thereby providing (in theory) a way to compute the minimal number of test cases required by any problem instance. This result applies, provided an additional hypothesis on the shape of possible solutions -a hypothesis fulfilled by any classical tway covering problem. Moreover, in our second modelling, which relies on a translation to the hypergraph vertex covering problem, the Φ-way covering offers the possibility to express conditions in a fashion that goes outside the expressiveness of existing solutions based on dependencies, allowing both universal and existential constraints of arbitrary nature on test cases. Experimental results have shown that, compared to a set of existing test generation tools, both our approaches generate test suites of comparable size, while being strictly more general in terms of expressiveness.

These promising experimental results warrant future work on the approach. First, additional graph colouring and vertex covering heuristics could be implemented and evaluated experimentally. Second, improvements on the efficiency of the generation of the graph from a given problem instance are currently being worked on. Finally, a third graph-based reduction, merging the two approaches presented in this paper, is also planned. It is hoped that, in the longer term, the use of our graph-based algorithms shall provide a drop-in replacement for the existing methods used in current tools and systems.

Fig. 3 :

 3 Fig. 3: The hypergraph constructed from the constraints Φ = {a = 0, b = 0, a = 0 ∨ b = 0}. Numbers are used to label segments belonging to the same hyperedge.

Figure 3

 3 Figure 3 gives an example of such a construction, for the simple set of conditions Φ = {a = 0, b = 0, a = 0 ∨ b = 0}, assuming that parameters a and b have the same domain D = {0, 1}. One can see that the hyperedge labelled "1" links all vertices with values satisfying the first condition (a = 0); similarly, the hyperedge labelled "2" links all vertices with values satisfying the second condition (b = 0). Finally, the hyperedge labelled "3" links all vertices with values satisfying the last condition (a = 0 ∨ b = 0); this last edge links three vertices.We shall now demonstrate how one can extract a Φ-way covering out of a vertex cover.

Fig. 4 :

 4 Fig. 4: An extended PICT input file for our test case generator.

2 Fig. 6 :

 26 Fig. 6: Test suite size output by various tools, for a varying number of parameters when t = 2.

3 Fig. 7 :

 37 Fig. 7: Test suite size output by various tools, for a varying number of parameters when t > 2.

Table 1 :

 1 The set of Boolean constraints representing the 2-way coverage of three 2-valued parameters named a, b, c.

  t = 2 with no Support of various features by the testing tools included in our study. constraints). Nevertheless, we carried four sets of experiments, and measured the size of the resulting test suites for all tools that could solve the problem.Simplest case: t = 2 In the first set of experiments, we considered only pairwise testing with no constraints, and computed the impact on the size of the test suite by varying the values of |D| (the size of the domain) and n (the number of parameters). The results are plotted in Figure6bfor increasing values of |D|, and in Figure6afor increasing values of n. One can see that graph colouring performs comparably to QICT, AllPairs and Jenny, with TCases producing slightly larger test suites. The hypergraph vertex covering provides the best results with respect to n, but shows a steeper increase than other tools with respect to |D|.

	E Colouring	Vertex cover	A TCases
		Jenny Forbidden tuples
		t >2
	AllPairs	t=2	QICT
	Fig. 5:

Table 2 :

 2 Test suite size output by various tools, for a varying number of parameters when t = 2.

Note how this is different from finding the minimum number of tests from scratch, as the existing test cases may not be part of an optimal solution, yet must be kept.

Although Φ is potentially infinite, it can be restricted to a finite subset by avoiding constructing expressions of the form ϕ ∧ ϕ, which are equivalent to ϕ.

https://bitbucket.org/sylvainhalle/gcases

http://www.mcdowella.demon.co.uk/allPairs.html

http://burtleburtle.net/bob/math/jenny.html

https://code.google.com/p/tcases/

www.pairwise.org/tools.asp

http://sourceforge.net/projects/vptag/. VPTag is limited to the case where t = 2, while our approach generalizes to other values of t