Nina Yevtushenko

Khaled El-Fakih
email: kelfakih@aus.edu

Anton Ermakov
email: antonermak@inbox.ru

On-the-fly Construction of Adaptive Checking Sequences for Testing Deterministic Implementations of Nondeterministic Specifications

Keywords: Nondeterministic finite state machines, reduction relation, fault model, test derivation, distinguishing test case, definitely reachable states, adaptive sequence

A method is proposed for deriving an adaptive checking sequence for a given deterministic implementation of a nondeterministic Finite State Machine (FSM) specification with respect to the reduction relation. The implementation is non-initialized, i.e., there is no reliable reset input. In order to obtain a sequence of reasonable length, in the proposed technique, we consider specifications with adaptive distinguishing test cases and adaptive transfer sequences. In fact, we show how under these considerations we can on-the-fly derive a checking sequence where the head part establishes the one-to-one correspondence between states of the implementation and the specification and if established the second part of the sequence is constructed for checking the one-toone correspondence between transitions of the implementation and a submachine of the specification FSM. The latter construction appropriately utilizes information from the first part to reach and check intended transitions.

Introduction

Finite State Machine (FSM) based test derivation is widely used when deriving conformance tests in many application domains such as sequential circuits, communication protocols, web-services, etc. There are many approaches for FSMbased test derivation that are summarized in many surveys such as [START_REF] Bochmann | Protocol testing: Review of methods and relevance for software testing[END_REF] [4] [20] [START_REF] Simao | Comparing finite state machine test[END_REF]. In many approaches, such as in the W-method [START_REF] Chow | Testing software design modelled by finite state machines[END_REF] and its many derivatives, both the specification and implementation FSMs are assumed to be initialized and thus, tests (input sequences or traces) are derived from a given initialized specification FSM; these tests are concatenated by a reliable reset that brings the machine to the initial state. Many other approaches do not rely on the existence of such possibly expensive resets and derive so-called checking sequences consisting of one test without resets. The reader may refer to [START_REF] Gonenc | A method for the design of fault detection experiments[END_REF][START_REF] Güniçen | Using multiple adaptive distinguishing sequences for checking sequence generation[END_REF][START_REF] Güniçen | The relation between preset distinguishing sequences and synchronizing sequences[END_REF][START_REF] Hennie | Fault-Detecting experiments for sequential circuits[END_REF][START_REF] Hierons | Reduced length checking sequences[END_REF][START_REF] Hierons | Optimizing the length of checking sequences[END_REF][START_REF] Kohavi | Switching and Finite Automata Theory[END_REF] for some approaches and summary of existing work on deriving and reducing length of checking sequences for deterministic FSMs. In general, while constructing a checking sequence for deterministic FSMs, as there are no resets, one may rely on the so-called synchronizing (or homing) sequence that takes the FSM from any state to the known state in addition to an input sequence that can distinguish two different states of the machine. Nowadays, design and analysis of non-deterministic systems is capturing a lot of attention. Nondeterminism can occur due to several reasons, such as limited observability, abstraction, etc. Accordingly, in this paper, we consider the derivation of checking sequences for observable nondeterministic FSMs. A nondeterministic machine is observable if for each state and input the machine can have many outgoing transitions under the input as long as different outputs are produced at these transitions. Otherwise, the machine is non-observable. We consider observable machines as it is known that any non-observable specification machine can be transformed into an observable one with the same behavior.

Petrenko et al. [START_REF] Petrenko | Generating checking sequences for nondeterministic finite state machines[END_REF] proposed a method for deriving a checking sequence for a complete nondeterministic FSM with respect to the equivalence relation under appropriate assumptions about the specification FSM and the fault domain. The specification FSM has to have a distinguishing input sequence for which the sets of output responses at any two different states do not coincide. Since an implementation under test (IUT) can be nondeterministic, the authors also rely on the all-weather conditions assumption. In [START_REF] Petrenko | Generalizing the DS-Methods for testing non-deterministic FSMs[END_REF] the authors extended the work considering the derivation of a checking sequence with respect to the reduction relation. Resetting is still used yet only in one phase of the construction approach. Ermakov [START_REF] Ermakov | Deriving checking sequences for nondeterministic FSMs[END_REF] presented a method for deriving an adaptive checking sequence with respect to the reduction relation under the assumption that the specification has a separating sequence, i.e., an input sequence for which the sets of output responses at any two different states are disjoint. The specification FSM has also to be deterministically connected, i.e., each state is deterministically reachable from any other state while an IUT is a complete deterministic FSM. A checking sequence is adaptive if the selection of the next input to be applied to an IUT depends on the outputs produced by the IUT to previously applied inputs. As in the other above approaches, the approach given in [START_REF] Ermakov | Deriving checking sequences for nondeterministic FSMs[END_REF] also uses resetting. In this paper, we reduce the limitation considered in the above papers about the use of resets. Moreover, differently from [START_REF] Ermakov | Deriving checking sequences for nondeterministic FSMs[END_REF] we show how to effectively use adaptive transfer and distinguishing sequences when deriving an adaptive checking sequence as such adaptive sequences can exist when there are no preset ones; in addition, such adaptive sequences can be shorter [START_REF] Alur | Distinguishing tests for nondeterministic and probabilistic machines[END_REF] [17] [START_REF] Kushik | Reducing the complexity of checking the existence and derivation of adaptive synchronizing experiments for nondeterministic FSMs[END_REF]. More precisely, we construct an adaptive checking sequence from a given non-deterministic observable FSM against a given complete deterministic IUT assuming that the specification FSM has adaptive transfer sequences as well as an adaptive distinguishing sequence (a distinguishing test case) of reasonable length. The existence of an adaptive transfer sequences means that every state of the machine is definitely reachable from any other state. We show that in this case, when testing with respect to the reduction relation, each state of the specification FSM is required to be implemented in an IUT. As usual, we also assume that the behavior of the IUT is not known, we only know that the number of states of the IUT does not exceed that of the specification. Under the above assumptions, an IUT is a reduction of the specification machine if and only if the IUT is isomorphic to a complete submachine of the specification FSM and thus, when testing it is enough to establish the one-to-one correspondence between states and transitions of the IUT and states and transitions of an appropriate submachine in the specification FSM. In other words, each transition of the IUT has to be traversed and an adaptive distinguishing sequence has to be applied for verifying the final state of the transition. This approach allows us to derive checking sequences of reasonable length when an adaptive distinguishing sequence has polynomial length with respect to the number of states of the specification FSM.

This paper is organized as followed. Section 2 includes preliminaries with related definitions. Section 3 includes the considered fault model and Section 4 includes the checking sequence construction method with related propositions and a simple application example. Section 5 concludes the paper.

Preliminaries

A finite state machine (FSM), or simply a machine, is a 4-tuple S = S, I, O, h S , where S is a finite nonempty set of states, I and O are finite input and output alphabets, and h S  S  I  O  S is a (behavior) transition relation. FSM S is nondeterministic if for some pair (s, i)  S  I there can exist several pairs (o, s)  O  S such that (s, i, o, s)  h S . FSM S is complete if for each pair (s, i)  S  I there exists (o, s)  O  S such that (s, i, o, s)  h S . FSM S is observable if for each two transitions (s, i, o, s 1 ), (s, i, o, s 2 )  h S it holds that s 1 = s 2 . FSM S is initialized if it has the designated initial state s 1 , written S/s 1 . Thus, an initialized FSM is a 5-tuple S, I, O, h, s 1 . In the following, we consider observable and complete FSMs if the contrary is not explicitly stated.

A trace of S at state s is a sequence of input/output pairs of consecutive transitions starting from state s. Given a trace i 1 o 1 … i k o k at state s, the input projection i 1 … i k of the trace is a defined input sequence at state s. For an observable nondeterministic FSM, if  = i 1 o 1 … i k o k is a trace at a state s, then there exists a unique sequence of consecutive transitions (s,

i 1 , o 1 , s 1 )(s 1 , i 2 , o 2 , s 2 )…(s k-1 , i k , o k , s k ).
As usual, for state s and a sequence   (IO)* of input/output pairs, the -successor of state s is the set of all states that are reached from s by trace . If  is not a trace at state s then the successor of state s is empty or we simply say that the -successor of state s does not exist. For an observable FSM S, for any string   (IO)*, the cardinality of the successor of state s is at most one. Given a subset S of states, the -successor of S is the union of -successors over all states of the set S.

FSM S is single-input if at each state there is at most one defined input at the state, i.e., for each two transitions (s, i 1 , o 1 , s 1 ), (s, i 2 , o 2 , s 2 )  h S it holds that i 1 = i 2 , and S is output-complete if for each pair (s, i )  S  I such that the input i is defined at state s, there exists a transition from s with i for every output in O. An initialized FSM S is acyclic if the FSM transition diagram has no cycles. An initialized FSM S is (initially) connected if each state is reachable from the initial state. Given an input alphabet I and an output alphabet O, a test case TC(I, O) is an initially connected single-input output-complete observable initialized FSM T = (T, I, O, h T , t 1 ) with an acyclic transition graph [START_REF] Petrenko | Conformance tests as checking experiments for partial nondeterministic FSM[END_REF]. Given a complete FSM S over alphabets I and O, a test case TC(I, O) represents an adaptive experiment with the FSM S [START_REF] Kushik | Methods for deriving homing and distinguishing experiments for nondeterministic FSMs[END_REF].

If | I | > 1 then a test case is a partial FSM. A state t  T is a deadlock state of the FSM T if there are no defined inputs at this state. In general, given a test case T, the length (height) of the test case T is defined as the length of a longest trace from the initial state to a deadlock state of T and it specifies the length of the longest input sequence that can be applied to an FSM S during the experiment. A trace from the initial state to a deadlock state is a complete trace of a test case [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF]. As usual, for complexity reasons, one is interested in deriving a test case with minimal length. A test case T is a distinguishing test case (DTC) for an FSM S if for every trace  of T from the initial state to a deadlock state,  is trace at most at one state of S. Sometimes, a distinguishing test case is called an adaptive distinguishing sequence.

Consider FSM S in Fig. 1.a. Using the approach proposed in [START_REF] Yevtushenko | On adaptive experiments for nondeterministic finite state machines[END_REF] a (adaptive) distinguishing test case can be constructed for FSM S (Fig. 2).

{1,3} {1,2} b/0 b/1 b/0 b/1 a/0 a/1 b/0 b/1 {3} {2} {3} {1} {2} {1 , 2 , 3 , 4 } { 2 , 3 } { 1 , 3 } { 1 , 2 } b/0 b/1 b/0 b/1 a/0 a/1 b/0 b/1 {3} {2} {3} {1} {2}
a/0 a/0 1 2 4 c/1 a/1 a,c/1 a,c/0 c/1 c/1 a/1 b/1 a/0 3 b/0 b/1 b/0 A B D c/1 a/1 c/1 c/1 b/0 c/1 a/1 a/0 C b/0 b/1 b/1
Given a complete observable FSM S = (S, I, O, h S ), state s  S is definitelyreachable (def-reachable) from state s  S if there exists a test case T s,s over I and O, initialized with the singleton {s}, and for every trace  of T s,s from the initial state to a deadlock state, the -successor of state s is either the empty set or {s}.

We hereafter refer to such a test case T s,s as a def-transfer test case from state s to state s or as an adaptive def-transfer sequence.

In fact, a def-transfer test case is defined in [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF] as an extension of a deterministic (d-)transfer sequence for states s and s. All the traces of T s,s take the FSM S from state s to state s. When testing with respect to the reduction relation not each state of the specification FSM, except for the initial state, is required to be implemented in an implementation FSM P. However, if there exists a def-transfer test case T s,s and state s is implemented in the reduction P of S then according to [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF], state s must be implemented in P.

In [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF], necessary and sufficient conditions were established to check if state s  S is definitely reachable from the initial state of the initialized FSM. Accordingly, when checking whether state s is definitely reachable form state s, the initialized FSM S/s can be considered. Moreover, in [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF] it is shown how a def-transfer test case T s,s can be derived such that the length of T s,s (if it exists) does not exceed the number of states of FSM S. By direct inspection, one can assure that for every two different states s, s of FSM S (Fig. 1.a) there exists a def-transfer test case T s, s . As an example, consider T 1,2 in Fig. 3. If an IUT replies with 1 to the applied input a at state 1 then we know that the next state of the specification is state 2. If the output 0 is produced by the IUT then the specification reaches state 3 and we apply the input a again. If the IUT replies with 0 to the applied input a then we know that the next state of the specification is state 2. If the output 1 is produced by the IUT then the specification reaches state 4 and we apply an input b in order to reach state 2.

Consider the FSM in Fig. 1.a. For states 2 and 1, 3 and 1, and 4 and 1, there exist deterministic transfer sequences, namely, state 1 is d-reachable from 2 by input sequence a, By direct inspection, one can assure that T 1,3 and T 1,4 can be easily derived from the machine in Fig. 3 as states 3 and 4 are deterministically reachable from state 2.

In order to check if there exists a distinguishing test case for the specification FSM S, we can use the procedures proposed in [START_REF] Yevtushenko | Decreasing the length of adaptive distinguishing experiments for nondeterministic merging-free finite state machines[END_REF][START_REF] Kushik | Adaptive homing and distinguishing experiments for nondeterministic finite state machines[END_REF]. If a general procedure is used then the complexity can become exponential w.r.t. the number of FSM states [START_REF] El-Fakih | On the reachability of the exponential upper bound of adaptive experiments for nondeterministic finite state machines[END_REF]. The complexity of the procedure proposed in [START_REF] Yevtushenko | Decreasing the length of adaptive distinguishing experiments for nondeterministic merging-free finite state machines[END_REF] is polynomial but it can be applied only for so-called merging free FSMs. A complete observable FSM is merging free if for each two different states s 1 and s 2 , every input i and every output o, the non-empty i/o successors of s 1 and s 2 do not coincide. For a merging free FSM, a distinguishing test case exists if and only if a distinguishing test case exists for each pair of different state of the FSM; the latter can be checked in polynomial time and the length of such test case is at most n(n -1)/2 if the FSM has n states. Then a distinguishing test case for the FSM is derived step by step starting from a single pair and adding a new state for the set of initial states at each step. In [START_REF] Yevtushenko | Decreasing the length of adaptive distinguishing experiments for nondeterministic merging-free finite state machines[END_REF], it is shown that the length of such test case is O(n 3 ). The class of merging-free FSMs is big enough; at least it contains many deterministic FSMs which are used in practical applications [START_REF] Güniçen | The relation between preset distinguishing sequences and synchronizing sequences[END_REF].

Hereafter we use S to denote a complete observable nondeterministic specification machine while P denotes a complete deterministic IUT.

Given complete FSMs S and P, state p of the FSM P is a reduction of state s of the FSM S, written p  s, if the set of traces of P at state p is a subset of that of S at state s; otherwise, p is not a reduction of state s, written p ≰ s. FSM P is a reduction of FSM S if for each state p there exists state s such that p  s.

Given complete FSM S, two different states s 1 and s 2 and an input sequence ,  is a separating sequence of states s 1 and s 2 if the sets out(s 1 , ) and out(s 2 , ) are disjoint. If  separates each pair of different states then  is a separating sequence for FSM S. For non-deterministic observable machines the tight upper bound on the length of a separating sequence of two states is known to be exponential with respect to number of FSM states [START_REF] Spitsyna | Studying the separability relation between finite state machines[END_REF] while for deterministic FSMs the length of an adaptive distinguishing sequence (a distinguishing test case) is polynomial [START_REF] Lee | Testing finite-state machines: state identification and verification[END_REF]. Moreover, if there exists a separating sequence then there exists a distinguishing test case but the opposite is not necessarily true. When an implementation is deterministic then the observation of n different replies to a separating sequence immediately means that the IUT has at least n states. For recognizing states of an implementation, a separating sequence sometimes can be replaced by state identifiers. An input sequence  is a state identifier of state s of FSM S if  is a separating sequence for each pair (s, s), s  s. As an example, the b b is a state identifier for states 3 and 4 of the FSM in Fig. 1.a and b a b is a state identifier for states 1 and 2.

Given a test case TC of a complete observable specification S, a trace that takes TC from the initial state to a deadlock state is a complete trace; the set Complete-Traces(TC) is the set of all complete traces of TC. If there exists a distinguishing test case then any two different states s 1 and s 2 of FSM S are r-distinguishable and thus, any state of any complete FSM over alphabets I and O is not a reduction of two different states of FSM S [START_REF] Petrenko | Conformance tests as checking experiments for partial nondeterministic FSM[END_REF]. The set of input projections of all complete traces of a distinguishing test case sometimes is called a distinguishing set. In [START_REF] Petrenko | Conformance tests as checking experiments for partial nondeterministic FSM[END_REF], it is shown, that given a state p of a complete FSM over alphabets I and O, for any two states s 1 and s 2 of FSM S there always exists an input sequence of the distinguishing set such that the set of output responses of P at state p is not a subset of that at both states s 1 and s 2 . Moreover, given a reduction P of FSM S, not each state of S has to be implemented in P. However, according to Proposition 1, if S has both a distinguishing test case and a def-transfer test case for each pair of different states then each state of S has to be implemented in P and there is the one-to-one correspondence between states and transitions of P and the corresponding states and transitions of an appropriate submachine of S. The latter allows the construction of shorter tests and reduces the efforts of checking if a given FSM P is a reduction of such specification FSM.

Two FSMs over the same input and output alphabets are isomorphic if there exists one-to-one correspondence between their states and transitions, i.e., if there exists one-to-one mapping f : S  P such that for any input i and any state s the 4-tuple (s, i, o, s)  h s if and only if ( f (s), i, o, f (s) )  h P .

Proposition 1. Given a complete observable FSM S with n states, let S have a distinguishing test case and each pair of different states s and s of S have a def-transfer test case T s, s . A complete observable FSM P that has at most n states is a reduction of S if and only if P is isomorphic to a submachine of S.

Proof. If P is isomorphic to a submachine of S then P is a reduction of S. Let now P be a reduction of S, i.e., for each state p of P there exists state s of S such that p  s. When there exists a distinguishing test case DTC for S, states of the FSM S are r-distinguishable and thus, any state of any complete FSM over alphabets I and O is not a reduction of two different states of FSM S [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF]. Moreover, if p  s then a distinguishing test case DTC has a trace at state p of P that is not a trace at any other state of S. On the other hand, let state s of FSM S be implemented in P as state p  s. Any state s is def-reachable from s and thus also is implemented in P as p  s. Therefore, each state of S is implemented in P and since P has at most n states, each state of S is implemented as a unique P state. Correspondingly, we can establish oneto-one correspondence F DTC : S  P between states of FSMs S and P according to the given distinguishing test case.

Moreover, since P is a reduction of S the following holds. If there is a transition p i/o -p where p = F DTC (s) and p = F DTC (s) then S has a transition si/o -s.  Let S have a distinguishing test case DTC, each pair of different states s and s of S have a def-transfer test case T s, s and the number of states of FSM P does not exceed that of S. FSM P is DTC-compatible with S if there exists one-to-one correspondence F: S  P such that for each state s  S it holds that the intersection of Tr(S/s)  Tr(P/p)  CompleteTraces(DTC) is not empty if and only if p = F(s). Proposition 2. Given the specification FSM S that has a distinguishing test case DTC, let a deterministic complete FSM P be DTC-compatible with S, each pair of different states s and s of S have a def-transfer test case T s, s and the number of states of FSM P does not exceed that of S. For each state p of P, the distinguishing test case DTC has a complete trace / that is a trace at state p; moreover,  is a state identifier of state p in P.

Proof. In fact, if there exists one-to-one correspondence between states of S and P according to the distinguishing test case DTC, then for each two states s and s, s  s, there exists a prefix of an input sequence of some complete trace / of DTC such that output responses at corresponding states p = F(s) and p = F(s) are different. As DTC is a distinguishing test case of S and FSM P is complete and deterministic, the latter means that a corresponding input projection of trace / is a state identifier of state p.



Fault Model for Deriving an Adaptive Checking Sequence

In FSM-based testing, it is assumed that the specification FSM describes the reference behavior while the fault domain FD contains each possible implementation FSM of the specification. In our case, the specification FSM S is complete and observable, moreover, S has a distinguishing test case and there exists a def-transfer test case for each pair of different states of S. The conformance relation is the reduction relation while any IUT of the FD is complete and deterministic and the number of its states does not exceed that of the specification FSM. In other words, we implicitly assume that the nondeterminism of the specification is implied by the optionality where a designer selects a better option according to some criteria. We do not rely on machines for having a reset; moreover, if the machines have a reset we still check if it is implemented correctly.

An implementation P conforms to the specification S if P is a reduction of S; otherwise, P is a nonconforming implementation. According to Proposition 1 the former means that P is isomorphic to some complete submachine of S.

An adaptive sequence is an input sequence when the next input of the sequence is selected based on the output of the IUT to the previous inputs. In fact, an adaptive checking sequence is a test case; however, the total length of this test case is big enough and for this reason, we do not talk about the complete test case and usually consider only a part of it that is appropriate for the implementation at hand. Correspondingly, similar to [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF], we propose a technique for testing an IUT P on-the-fly but with a single input sequence; the algorithm yields the verdict pass if P is a reduction of a given specification FSM S and the verdict fail if P is not a reduction of S. Our proposed technique has two procedures. The former checks if P has the same number of states as S and establishes, based on a distinguishing test case, the one-toone correspondence between the states of P and S if such a correspondence exists. We underline that when such correspondence can be established then an appropriate trace of the distinguishing test case is identified as a state identifier of the corresponding state in P (Proposition 2). The second procedure checks that there is one-to-one correspondence between the transitions of P and an appropriate submachine of S.

Deriving an Adaptive Checking Sequence

This section includes two procedures for on-the-fly constructing a checking sequence for a given IUT P from the specification FSM S with respect to the reduction relation. Given a distinguishing case DTC for the FSM S, Procedure 1 returns the verdict fail if P is not DTC-compatible with S; otherwise, it computes the set "state_identifier". For each state s of S, this set includes the trace of DTC executed by the IUT at the state of P corresponding to s and it also includes the state of S reached after this trace. Then Procedure 2 starting from information obtained from Procedure 1 continues deriving the checking sequence where it focuses on checking the one-toone correspondence between transitions of P and some submachine of S.

As an application example of Procedure 1, consider the implementation FSM P in Fig. 1.b and assume that at the beginning of testing P is at state C. After applying DTC (in Fig. 2 Then, at Step 2, s new = s = 1, after applying T 2,1 (input sequence a) we observe 0 and then after applying again the input sequences b a followed by b b of DTC the traces b a/ 1 1 followed by b b / 1 1 are observed and accordingly the tuple < 1, b a / 1 1, 2 > is added to "state_identifier". We stop as the set "state_identifier" is complete and the specification FSM reaches state 2 after the observed trace. Proof. If FSM P passes Procedure 1 then P is strongly connected, since each state of P is traversed when executing Procedure 1. For this reason, if at Step 1, the reached state has no unchecked transitions then at Step 2, in the set "Transitions" that has only already checked transitions, there is a path to a state with an unchecked transition. Procedure 2 establishes the one-to-one correspondence between transitions of FSM P and an appropriate submachine of S, since all P transitions are executed and checked for a conforming output and corresponding final state (according to DTC). Therefore, FSM P passes Procedure 2 if and only if P is isomorphic to some submachine of S and the proposition holds according to Proposition 1.

1 (A) b a 1 1 2 (B) 2 (B) b a b 1 0 1 1 (A) 3 (C) b b 0 0 3 (C) 4 (D) b b 0 1 2 (B)



As an application example, consider the FSM in Fig. 1.a, after applying Procedure 1, we obtain s 1 = 3, the trace , and state s 2 = 2 (reached after applying ); in addition, the set "state_identifier" = { < 1, b a / 1 1, 2 >, < 2, b a b / 1 0, 1 >, < 3, b b / 0 0, 3 >, < 4, b b / 0 1, 2 >}. As s = s 2 = 2 and the set "Transitions" is empty, at Step 1, apply the input b at s 2 followed by b a b of DTC and observe the trace b b a b / 1 1 0 1 that reaches state 1 of the FSM S. Add (2, b, 1, 2) to "Transitions",  becomes that of Procedure 1 concatenated with the trace b b a b / 1 1 0 1, and the reached state s 2 = 1 according to the tuple < 2, b a b / 1 0 1, 1 > of the "state_identifier". We goback to Step 1, apply the input a followed by b a b of DTC and observe 1 1 0 1, reach state s 2 = 1, add (1, a, 1, 2) to "Transitions", append  as usual, and proceed again to Step 1. At s 2 = 1 apply b, then apply b a of DTC and observe 1 1 1; add (1, b, 1, 1) to "Transitions" and reach state s 2 = 2. Again at Step 1, apply a followed by b a and observe 0 1 1, add (2, a, 0, 1) to "Transitions". Then at the reached state s 2 = 2, apply c followed by b b of DTC, observe 1 0 1, add (2, c, 1, 4) to "Transitions" and reach state s 2 = 2. Now, as all (2, b, 1, 2), (2, a, 0, 1), (2, c, 1, 4) are in the set "Transitions", at Step 2, we consider s = 4 such that from the reached state s 2 = 2 there is the checked trace  = c /1 from 2 to 4 and for some input i there is no transition (4, i, o, s) in the set "Transitions". We transfer to state 4 from state 2 by applying the input c, now s 2 becomes the reached state 4. We go-back to Step 1 where we select to apply the input a followed by applying the sequence b b of DTC, observe 1 0 0, add (4, a, 1, 3) to "Transitions" and reach state s 2 = 3. We proceed as above till the set "Transi-tions" is full. The verdict pass is produced after completing the set "Transitions" and thus, FSM P is a reduction of the specification FSM S.

As the length of a transfer sequence when checking a new input is less than the number n of states of the FSM S, the length of a checking sequence returned by Procedure 2 is proportional to the length of a distinguishing test case. If this length is polynomial with respect to the number of S states as it happens for merging-free FSMs then the length of an adaptive checking sequence is O(n 3 ), i.e., the length evaluation is almost similar to that for deterministic FSMs [START_REF] Hennie | Fault-Detecting experiments for sequential circuits[END_REF].

Conclusion

In this paper, we have proposed an adaptive strategy for testing a deterministic implementation FSM against nondeterministic observable specification FSM with respect to the reduction relation. Similar to deterministic FSMs, the strategy can be applied under appropriate restrictions upon the specification FSM and fault domain. However, we show that the requirement of the existence of a separating sequence can be replaced by the requirement of the existence of a distinguishing test case. This is useful as the existence of a distinguishing test case is more likely than that of a separating sequence and generally, the length of a distinguishing test case is less than that of a separating sequence (when both exist). In addition, the construction uses adaptive transfer sequences that reduce the length of an applied input sequence. We note that in this paper, we do not discuss any optimization procedure for deriving adaptive checking sequences; this is left for the future work. Another possible direction of a future work is the extension of the proposed work for testing nondeterministic noninitialized implementations. It could be also interesting to apply a proposed approach for deriving checking sequences for I/O automata, for example, with respect to the widely used ioco conformance relation that is very close to the reduction relation between FSMs.

6

Fig. 1 .

 1 Fig. 1. (a) Specification FSM S (b) Implementation FSM P

Fig. 2 .

 2 Fig. 2. (a) The distinguishing test case (b) The test case for (a) where source states are indicated

Fig. 3 .

 3 Fig. 3. A def-transfer test case for states 1 and 2 of the FSM in Fig. 1.a

  state 3 is d-reachable from 1 by input sequence c b a and state 4 is dreachable from 1 by input sequence b a. State 2 is d-reachable from 3 and 4 by input sequences c b and b correspondingly, state 3 is d-reachable from 2 and 4 by input sequences b a and a, while state 4 is d-reachable from 2 and 3 by input sequence b.

  .a) we observe a trace b b / 0 0 which is a trace of state 3 of S. Accordingly, s = s 1 = 3,  = . After applying DTC again (at Step 1), we observe  = b b / 0 0 which is a trace of state C of P. Thus,  becomes b b b b / 0 0 0 0 , s 2 = 3, s = 3 as the starting state of S where  is a trace of DTC, and the tuple < 3, b b /0 0, 3 > is added to the (initially empty) set "state_identifier", s = 3,  =  = b b / 0 0, and then we go to Step 2 as the tuple < 3, b b / 0 0, 3 > is in "state_identifier". Let s new = 4, then s = 4, we then apply the transfer sequence c, observe 1, and thus have  = c / 1. Then after applying the b b of DTC to P, we observe b b / 0 1. As  = b b b b c b b / 0 0 0 0 1 0 1 is a trace at s 1 , then we go back to Step 1 where we apply b a of DTC and observe 1 0, then s 2 becomes 1, s = 2, and we add the tuple < 4, b b / 0 1, 2 > to "state_identifier". Similarly, afterwards, s= s= 2,  : =  = b a, at Step 1, we apply b a b of DTC, the trace b a b / 1 1 1 is observed and the tuple < 2, b a b / 1 0 1, 1 > is added to the set "state_identifier".

Table 1

 1

	rep-

Table 1 .

 1 The set "state_identifier" for the FSM in Fig.1.b according to the distinguishing test case in Fig.2.

	Current state of S	State	Output	Next state of S
	(corresponding state in IUT)	identifier	response	(corresponding state in IUT)

Procedure 1: Checking the DTC-compatibility between a deterministic IUT P and the specification S Input:

  The complete and observable specification FSM S with n states that has a distinguishing test case DTC and a def-transfer test case T s,s for each pair of different states s and s; a complete deterministic FSM IUT P with at most n states. Output: Verdict fail if P is not DTC-compatible with S or state s 2 , trace , the set "state_identifier". The set "state_identifier" is the empty set;  is the empty trace; Apply DTC to P and observe a complete trace  ;If  is not a trace at any state of S then Return the verdict fail ;

	Else
	Determine state s 1 of S with the trace  ;
	 : =  ;
	s : = s 1 ;
	Step 1.
	Apply DTC to P and observe a complete trace  ;
	 : =   ;
	If  is not a trace at state s 1 of S then
	Return the verdict fail ;
	Else
	Determine state s 2 where  takes the FSM S from state s 1 ;
	Determine state s of S with the trace ;
	Add the tuple < s, , s > to the set "state_identifier" ;
	If the set "state_identifier" has n tuples then
	End Procedure 1
	Else
	s : = s ;
	 : =  ;
	If the set "state_identifier" has a tuple < s, , s 2 >

then Go-to Step 2 ; Else Go-back to Step 1 ; Step 2.

  Let s new be the state of S such that "state_identifier" has no tuple with the first item s new ; s : = s new ; Apply T s2, s and observe a complete trace  ; Apply DTC to P and observe a complete trace  ; According to Proposition 1, if P is a reduction of S then each state p of P has to have a corresponding state s in S such that the set of complete traces of DTC executed at state s has a trace executed at state p, i.e., the following proposition holds. If a trace  observed when executing Procedure 1 is a trace of the specification FSM S, i.e., Procedure 1 does not return the verdict fail, then the IUT P is DTC-compatible with S.If the verdict fail is produced by Procedure 1 then the IUT P is not a reduction of S. Otherwise, P is DTC-compatible with S and for each state s of S the set "state_identifier" includes the trace of DTC executed by the IUT at the state corresponding to s and it also includes the state of S reached after this trace.Moreover, if P is DTC-compatible with S, then due to Proposition 2, the input projection of a trace observed at state p of P is a state identifier of this state. Let the IUT P be DTC-compatible with S, i.e., there exists one-toone correspondence F: S  P such that for each state s  S it holds that the intersection of Tr(S/s)  Tr(P/p)  CompleteTraces(TC) is not empty if and only if p = F(s). Given a tuple < s, , s > of the set "state_identifier", the input projection of trace  is a state identifier of state F(s) while s is the state of S reached by .

	Proposition 3. 
	Proposition 4.
	 : =    ;
	If  is not a trace at state s 1 of S then
	Return the verdict fail;
	Else
	Go-back to Step 1;	



Procedure

2: Adaptive testing of a deterministic implementation FSM Input:

  The complete and observable specification FSM S with n states that has a distinguishing test case DTC and a def-transfer test case T s,s for each pair of different states; a complete deterministic FSM P that has at most n states, initial state s 1 , already observed trace  and the set "state_identifier" returned by Procedure 1 and state s 2 reached after executing Procedure 1. Output: Verdict pass if and only if P a reduction of S. The set "Transitions" is the empty set; s = s 2 ;

Step 1. If there

  exists input i such that there is no 4-tuple (s 2 , i, o, s 2 ) with the pair (s 2 , i) in the set "Transitions" then Apply i followed by DTC and observe a trace  ; If  is not a trace at state s 2 then Return the verdict fail ; Else Add the transition (s 2 , i, o, s) to the set "Transitions" where o is the observed output to i while s is the current state according to the set The verdict pass is produced by Procedure 2 if and only if the IUT P is a reduction of S.

	Step 2.
	If the set "Transitions" is full, i.e., the set includes an item (s, i, o, s) for every pair
	(s, i) then
	Return the verdict pass ;
	Else
	Using transitions of the set "Transitions" determine a trace  from s 2 to state s
	such that for some i there is no transition (s, i, o, s) with the pair (s, i) in the
	set "Transitions" ;
	 : =   ;
	s 2 : = s ;
	Go-back to Step 1;
	
	Proposition 5.
	"state_identifier";
	 : =   ;
	s 2 : = s ;
	Go-back to Step 1;
	Else

Acknowledgment

This work was partially supported by the RSF project № 16-49-03012


Krishna Patel
email: krishna.patel@brunel.ac.uk

Robert M Hierons
email: rob.hierons@brunel.ac.uk

Resolving the Equivalent Mutant Problem in the Presence of Non-determinism and Coincidental Correctness

Keywords: Mutation Testing, Coincidental Correctness, Non-determinism, Equivalent Mutant Problem

In this paper, we develop a new mutation testing technique called Interlocutory Mutation Testing (IMT) that mitigates the equivalent mutant problem in the presence of coincidental correctness and non-determinism. The accuracy of IMT was evaluated; it obtained a classification accuracy of 93.33% for non-equivalent mutants and 100% for equivalent mutants in a non-deterministic system with coincidental correctness.

Introduction

Mutation Testing (MT) is a technique for generating artificial faults [START_REF] Offutt | Investigations of the software testing coupling effect[END_REF], which are reasonably accurate simulations of real faults [START_REF] Androutsopoulos | An Analysis of the Relationship Between Conditional Entropy and Failed Error Propagation in Software Testing[END_REF]. MT operates by applying a minor augmentation (referred to as a mutation) to the system under test (SUT) S o to produce a faulty version S m [START_REF] Carver | Mutation-based testing of concurrent programs[END_REF] called a mutant. For example, a statement X < 5 in S o might be transformed into X > 5 in S m .

Unfortunately, a limitation of MT is that it can produce equivalent mutants [START_REF] Gligoric | MuTMuT: Efficient Exploration for Mutation Testing of Multithreaded Code[END_REF] -this is known as the equivalent mutant problem. An equivalent mutant is an augmentation S m that is observationally equivalent to the SUT S o . For example, suppose that M ath.abs [START_REF] Carver | Mutation-based testing of concurrent programs[END_REF] and M ath.abs(-5) appear on Line 1 in S o and S m respectively. S m is an equivalent mutant, because the augmentation is semantically equivalent and doesn't modify the behaviour of S o .

A study conducted by Yao et al. [START_REF] Yao | A study of equivalent and stubborn mutation operators using human analysis of equivalence[END_REF] demonstrated that the equivalent mutant problem is pervasive. Despite the fact that deducing mutant equivalence is undecidable [START_REF] Budd | Two notions of correctness and their relation to testing[END_REF], this has motivated some research into how the problem can be circumvented [START_REF] Jia | An Analysis and Survey of the Development of Mutation Testing[END_REF]. For example, let S o (I) and S m (I) denote the respective outputs of S o and S m for a given input. Many researchers typically expose S o and S m to a test suite to obtain a set of pairs S o (I), S m (I) and assume that S o and S m are equivalent if the following condition holds for each pair: S o (I) = S m (I).

For ease of reference, we refer to this as the Traditional Equivalent Mutant Detection Technique (TEMDT). An example of the use of TEMDT can be found in Sadi et al. [START_REF] Sadi | Verification of phylogenetic inference programs using metamorphic testing[END_REF].

However, this assumption doesn't always hold. For example, non-deterministic behaviours may be responsible for any observed discrepancies, and may be misinterpreted as having originated from the mutation [START_REF] Carver | Mutation-based testing of concurrent programs[END_REF]. Another example includes the presence of coincidental correctness; the SUT can misbehave but still produce the expected output, which can lead to non-equivalent mutants being mistakenly classified as equivalent. Alternative techniques have been proposed to address these problems, but have limitations (see Section 2). Manual inspection is typically used under such circumstances [START_REF] Aichernig | Efficient Refinement Checking for Model-Based Mutation Testing[END_REF].

In our previous work, we developed Interlocutory Testing (IT), a testing technique that suppresses coincidental correctness and can operate effectively in the presence of non-determinism [START_REF] Patel | Interlocutory Testing: Combating Coincidental Correctness in Testing[END_REF]. This paper explores how IT can be used to alleviate the Equivalent Mutant Problem in systems with non-determinism and/or coincidental correctness. We call the approach Interlocutory Mutation Testing (IMT).

The relationship between the input and output of the SUT, in conjunction with one's knowledge/expectations about the SUT, can be used to predict aspects of the execution trace. For example, consider the Bubble Sort algorithm; Input and Output are sequences of integers. If Input = Output, one can predict that the Swap Operator was invoked at least once. The correctness of this prediction is predicated on whether the SUT's behaviour mirrors the tester's expectations. Let f denote a fault in Bubble Sort that overwrites the value of the first element of Input with a random value. f can lead to situations in which Input = Output and the swap operator was not invoked; the failure to satisfy the prediction above in such situations shows that the behaviour of the SUT does not satisfy the tester's expectations 1 . IMT exploits this observation as follows. Let S denote the SUT and M denote a mutated version of S. Suppose that M is executed with an input M Input, and produces an execution trace M ET and output M Output. IMT uses the relationship between M Input and M Output, in conjunction with the tester's knowledge/expectations about S, to predict aspects of M ET . If this prediction is incorrect then this suggests that M is not an equivalent mutant.

This paper makes the following main contributions:

1. A new technique called IMT that can classify mutants as equivalent and nonequivalent in programs with coincidental correctness and/or non-deterministic behaviours.

An evaluation of the accuracy of IMT.

The paper is structured as follows. We begin by presenting related work in Section 2. Section 3 describes our proposed technique and explains how the technique can be applied. Section 4 outlines our experimental set-up. The experiment results are presented and discussed in Section 5, along with threats to validity in Section 6. Conclusions are finally drawn in Section 7.

Related Work

The Equivalent Mutant Problem and Coincidental Correctness

Fault detection requires the execution of a faulty statement, that causes the subsequent infection of a state (to produce a failure), and propagation of an infected state to the output (so an oracle can assess it) [START_REF] Voas | PIE: a dynamic failure-based technique[END_REF]. According to Masri and Assi [START_REF] Masri | Prevalence of coincidental correctness and mitigation of its impact on fault localization[END_REF], strong coincidental correctness occurs when the first two conditions are satisfied, the third is not, and weak coincidental correctness occurs when the first condition is satisfied, but not the third; the second condition may or may not be satisfied. Weak coincidental correctness subsumes strong coincidental correctness. In this paper, "coincidental correctness" refers to weak coincidental correctness.

In the context of mutation testing, coincidental correctness can be described as follows: Let S o be the SUT and S m be a non-equivalent mutant. Also let s m denote the state in S m after the mutated statement executes and s o be the corresponding state in S o . Coincidental correctness occurs if s m and s o map to the same output, despite the differences in code.

Masri and Assi [START_REF] Masri | Cleansing Test Suites from Coincidental Correctness to Enhance Fault-Localization[END_REF] define information flow strength as the percentage of information that propagates between two program points; a higher percentage indicates greater strength. This determines the probability that an infected state will propagate to the output, which is tantamount to the likelihood of observing coincidental correctness. Masri et al. [START_REF] Masri | Prevalence of coincidental correctness and mitigation of its impact on fault localization[END_REF] conducted a series of experiments that suggested that coincidental correctness is widespread. For example, 96.5% and 72% of the systems they investigated had strong and weak coincidental correctness respectively and between 63.76 -97.58% of the weak information flows in six of these systems had a strength of 0.

Despite the prevalence of coincidental correctness, little research has been conducted on determining mutant equivalence in the context of coincidental correctness. To our knowledge, only one approach has been proposed. Offutt and Lee [START_REF] Offutt | How Strong is Weak Mutation?[END_REF] extend TEMDT (see Section 1). They suggest additionally comparing s o and s m . While this can be useful in some situations it's not a universal solution e.g. its effectiveness may be limited in non-deterministic systems.

The Equivalent Mutant Problem and Non-Deterministic Systems

Non-deterministic systems are becoming increasingly prevalent e.g. concurrency can lead to alternative interleavings. For example, consider a variable X that is instantiated with a value of 3. Suppose we have two threads t 1 and t 2 and that t 1 applies the following operation to X: X = X + 1. Further, suppose that t 2 updates the value of X to X = X × 2. The order of the interleavings affects the final state of X i.e. if t 1 executes first, then X = 8 and if t 2 executes first X = 7.

This complicates the mutant classification process. Several proposals have been made to address this. For example, Carver [START_REF] Carver | Mutation-based testing of concurrent programs[END_REF] identifies two methods -Multiple Execution Testing (MET) and Deterministic Execution Testing (DET). In MET, confidence is improved by executing the original S o and mutant S m versions multiple times and observing their output distributions. DET involves forcing the SUT to execute deterministically by manipulating conditions e.g. a Genetic Algorithms Mutation Rate can be set to 100% or 0% to force deterministic execution of the Mutation Operator.

Both strategies are viable, but have limitations. For example, MET is dictated by chance; thus there is scope for misclassification [START_REF] Carver | Mutation-based testing of concurrent programs[END_REF] and non-replicability [START_REF] Carver | Mutation-based testing of concurrent programs[END_REF]. It's also expensive because it uses multiple executions. On the other hand, DET limits test case selection; thus some mutation points may not be reachable with allowable test cases. Carver [START_REF] Carver | Mutation-based testing of concurrent programs[END_REF] attempted to reduce the impact of these weaknesses by combining MET and DET.

Gligoric et al. [START_REF] Gligoric | MuTMuT: Efficient Exploration for Mutation Testing of Multithreaded Code[END_REF] suggest executing S o with a test case t, and then establishing whether the mutant statement in S m could have been reached by this execution. Non-reachability implies equivalence for t. This approach is limited to the identification of equivalent mutants in unexecuted code.

Finally, Papadakis et al. [START_REF] Papadakis | Trivial compiler equivalence: a large scale empirical study of a simple, fast and effective equivalent mutant detection technique[END_REF] propose comparing the S m 's object code to the object code of the S o . If S m 's object code matches S o 's object code, then we can guarantee that S o is equivalent to S m . However, if the comparison reveals that there are discrepancies, S m may either be equivalent or non-equivalent to S o . Although the approach can't correctly classify all mutants, it is inexpensive and so can be a valuable complimentary equivalent mutant classification technique.

Interlocutory Mutation Testing

IMT was developed to enable the classification of equivalent and non-equivalent mutants in programs that are non-deterministic and/or are susceptible to coincidental correctness. Section 3.1 introduces the technique and demonstrates how it can classify mutants despite the presence of coincidental correctness, and Section 3.2 shows how the technique can be extended to cope with non-determinism.

Interlocutory Mutation Testing and Coincidental Correctness

This section draws on the following running example.

The SUT is a Genetic Algorithm, which is a search optimisation technique. The SUT consists of four major components: Initial Population Generator, Crossover, Mutation, and Selection. Let Sys denote the SUT. Consider Sys's selection operator, denoted by Sys so . Sys so 's Input consists of a population size parameter P S, which is the maximum population size, and a P opulation, such that P opulation.size() ≥ P S. Let P opulation SOI be the state of P opulation at this point in the execution trace. Input is processed by the Sys so as follows: random elements of P opulation SOI are iteratively removed until P opulation.size() == P S. Sys so 's resultant Output is a version of the P opulation that has been subjected to this process; P opulation SOO denotes the state of P opulation at this point in the execution.

Suppose that a non-equivalent mutant, denoted by M U T , of the Sys was produced. The delta between M U T and Sys is that M U T performs an additional operation; it adds a random individual to P opulation SOI during Sys so 's initialisation phase. Since Sys so iteratively removes random individuals from P opulation SOO .size() until P opulation SOO .size() == P S, all traces of an additional member being added to P opulation SOI might be lost by the time the execution reaches the P opulation SOO state. Thus, M U T is a coincidentally correct mutant.

Intuition Let's consider how M U T could be correctly classified. Suppose that M U T is executed and produces a log file that details the execution trace M ET . Let M U T so denote M U T 's selection operator. The execution trace of M U T so is a subsequence of M ET . Let M Input and M Output be M U T so 's input and output respectively. Information about M ET can be revealed by assessing the relationship between M Input and M Output. For example, P opulation SOI .size() > P opulation SOO .size() may be one relationship between M Input and M Output, and from this, we can deduce that members of P opulation were removed during the execution.

If we assume that M U T is equivalent to Sys, we can use our knowledge about how Sys behaves in this context to predict aspects of M ET . To illustrate, since we know that the Selection Operator iteratively removes random members of P opulation until P opulation.size() == P S, when P opulation SOI .size() > P opulation SOO .size(), we can deduce that the P opulation must have been expanded by P opulation SOI .size() -P opulation SOO .size() individuals before the Selection Operator was executed. Since we also know that the only function that can add additional members to a P opulation of size P S is the Crossover Operator, the following prediction about M ET can be made: the Crossover Operator generated P opulation SOI .size() -P opulation SOO .size() individuals and added them to P opulation.

Finally, this prediction can be checked against M ET . Let CrossoverN be the total number of members that were actually generated by the Crossover Operator during the execution i.e. as reported in M ET . In continuation of the example above, this involves checking CrossoverN == P opulation SOI .size() -P opulation SOO .size(). Since an additional member is added to P opulation SOI by M U T , this predicate would evaluate to false, which indicates that the prediction was incorrect. The behaviour of M U T deviated from how Sys would have behaved; thus we can conclude that M U T is not equivalent to Sys.

Had M U T been equivalent to Sys (i.e. had the additional member not been added to P opulation during the initialisation of the Selection Operator), the prediction would have been correct.

The example above demonstrates that one can use the relationship between M Input and M Output to predict properties of M ET . Discrepancies between this prediction and M ET indicate that M U T is not equivalent to Sys. The ex-ample also demonstrates that this approach works in the presence of coincidental correctness. This forms the intuition of our technique -Interlocutory Mutation Testing (IMT).

Technique Description This section outlines how IMT realises the intuition described above. IMT requires that the relationship between an input and output (Input-Output pair) is associated with a prediction about the mutants execution trace M ET . Associating a prediction with every individual Input-Output pair would be impractical. Instead, IMT groups Input-Output pairs together using Input-Output Relationships (IORs). Certain predictions are applicable to all Input-Output pairs in such a group. Consider the earlier example; P opulation SOI .size() > P opulation SOO .size() is an IOR (for ease of reference, we call this IOR 1 ), and it groups Input-Output pairs where the prediction is that the Crossover Operator produced P opulation SOI .size()-P opulation SOO .size() members and added them to the P opulation.

The prediction that is associated with an IOR is referred to as an "Interlocutory Decision" (ID). An ID can be expressed using any method, on the proviso that it can unambiguously describe one's prediction about M ET and be automatically compared with the execution trace M ET . For example, as demonstrated above, IDs can be expressed as predicates e.g. CrossoverN == P opulation SOI .size()-P opulation SOO .size() (this ID is associated with IOR 1 ). Alternative methods of expressing IDs are discussed in our previous work [START_REF] Patel | Interlocutory Testing: Combating Coincidental Correctness in Testing[END_REF].

In IMT, the mutant is executed, which results in an execution trace M ET . IMT checks whether an IOR is satisfied by an input M Input and output M Output, which are extracted from M ET . In continuation of the example above, M Input = P opulation SOI and M Output = P opulation SOO . If M Input.size() > M Output.size(), then IOR 1 is satisfied. If the IOR is satisfied, then IMT checks that M ET satisfies the IOR's associated IDs (e.g. in the case of IOR 1 , this would involve checking CrossoverN == P opulation SOI .size()-P opulation SOO .size()). Finally, if the prediction is correct (e.g. if CrossoverN == P opulation SOI .size()-P opulation SOO .size()), then IMT reports that the mutant is possibly equivalent, otherwise it reports that the mutant is non-equivalent.

An Input-Output pair I/O is said to be valid if the SUT can produce output O in response to input I. IOR 1 doesn't cater for all valid Input-Output pairs -it's possible to observe P opulation SOI .size()==P opulation SOO .size() in Sys. IOR 1 must report that its classification was inconclusive in such cases. This can be remedied by creating more IORs that cover such pairs. For example, P opulation SOI .size() == P opulation SOO .size() can be IOR 2 and CrossoverExecuted == f alse can be its ID.

Interlocutory Relations (IRs) are the final construct used by IMT. An IR groups multiple IORs together to enable the definition of potentially complex relationships between IORs. Such relationships can enhance their classification accuracy. To illustrate, since all valid Input-Output pairs in Sys are collectively covered by IOR 1 and IOR 2 , if a situation arises where neither IOR 1 nor IOR 2 is satisfied i.e. if P opulation SOI .size() < P opulation SOO .size(), then the IR can guarantee that the Input-Output pair under consideration can not have been observed in Sys, and thus reports that the mutant is non-equivalent. We refer to this grouping of IOR 1 and IOR 2 as IR 1 . Thus, an IR operates as follows: Each IOR that is associated with the IR is evaluated as described above to obtain a set of Possibly Equivalent/Non-Equivalent/Inconclusive classifications. These classifications are analysed by the IR to arrive at a final conclusion. If at least one classification is possibly equivalent and none are non-equivalent, then the final conclusion is that the mutant is equivalent, and if at least one is nonequivalent, then the final conclusion is non-equivalent. Assuming that the IR has IORs that collectively cover all valid Input-Output Pairs, the final conclusion can be non-equivalent if all classifications are inconclusive (as is the case for IR 1 ).

Interlocutory Mutation Testing and Non-determinism

Intuition Consider the Tournament Selection Operator (TSO) of a Genetic Algorithm. In particular, consider the logic that determines the winner of a tournament. A tournament consists of a set of competitors tournament = {Competitor 1 , Competitor 2 , ..., Competitor n }, each of which is associated with a fitness value. One Competitor i ∈ tournament is randomly selected to be the winner of the tournament. A competitor's chance of winning is based to their fitness value, relative to the combined fitness values of all other competitors in the tournament. Thus, even though any competitor could win, the competitor with the highest fitness will have the greatest chance of being selected as the winner. Let winner denote the selected competitor. On invocation of TSO, multiple tournaments are performed tournaments={ tournament 1 , winner 1 , tournament 2 , winner 2 , tournament 3 , winner 3 , ...}.

An IR, which we will refer to as TournamentPIR, may be constructed for TSO. TournamentPIR may be associated with one IOR IOR T P IR that is only satisfied under the following condition: For each tournament i , winner i in tournaments, tournament i contains at least two competitors Competitor j and Competitor k , such that Competitor j .getF itnessV alue() = Competitor k .getF itnessV alue().

Let tournaments strong be a subset of tournaments, such that for each tournament i , winner i ∈ tournaments strong , winner i was a solution with the highest fitness in tournament i . Conversely, let tournaments weak be a subset of tournaments, where in each tournament i , winner i ∈ tournaments weak , winner i was a solution with the lowest fitness. IOR T P IR may be associated with an ID that predicts that tournaments strong contains more members than tournaments weak .

In summary, TournamentPIR predicts that tournament strong will contain more members than tournaments weak (this is the ID), when every tournament in tournaments contains at least two competitors with different fitness values (this is the IOR). Although it's unlikely, it's possible that tournament strong may validly contains fewer members than tournaments weak . This means that Tour-namentPIR can misclassify an equivalent mutant as a non-equivalent mutant. We refer to such a misclassification error as a false positive.

This demonstrates that a revised evaluation method is necessary for IRs that deal with probabilistic behaviours, to reduce the incidence of false positives. We refer to IRs that use the revised evaluation method as Probabilistic IRs (PIRs). For the sake of clarity, we refer to IRs that use the evaluation method detailed above as Deterministic IRs.

The intuition behind the new evaluation method is as follows. As discussed above, certain behaviours can cause PIRs to report false positives e.g. when tournament strong contains fewer members than tournament weak . The randomised properties of a system determine how frequently certain behaviours are observed. This means that all behaviours, including those that can lead to false positives will have a typical rate of occurrence. In other words, a PIR has a typical false positive rate. The proposed evaluation method is to use statistical techniques to compare a PIR's typical false positive rate to the proportion of non-equivalent classifications made by that PIR; if the proportion of non-equivalent mutant classifications is significantly higher than the false positive rate, then it's likely that the mutant is non-equivalent, otherwise, it's possible that the mutant is equivalent.

Technique Description This section introduces the evaluation method used by PIRs to reduce the impact of false positives.

The PIR evaluation method is two-fold. The first part of the evaluation method attempts to reduce the impact of false positives for a single test case tc. Let P IR be a PIR e.g. TournamentPIR and suppose that P IR has a typical false positive rate F P R tc of 30%. F P R tc can be determined by analysing the randomised properties of the SUT, extrapolated from empirical test data, or be based on the tester's expertise. P IR may be evaluated multiple times during an execution of tc. For example, TournamentPIR is evaluated each time TSO is executed, and TSO can execute multiple times if the Genetic Algorithm has been configured to perform more than one generation. Each evaluation of P IR will either yield an equivalent or non-equivalent classification. Let R tc = count(N on Equivalent tc ) ÷ (count(N on Equivalent tc ) + count(Equivalent tc )), where count( N on Equivalent tc ) and count(Equivalent tc ) represent the number of times the mutant was classified as Non-Equivalent and Equivalent respectively. Thus, R tc represents the proportion of times that P IR classified the mutant as Non-Equivalent in tc. In the first part of the evaluation method, R tc is compared with F P R tc using Pearsons χ 2 . P IR's classification of the mutant based on tc is Non-equivalent if R tc > F P R tc and the difference is statistically significant, otherwise the classification is equivalent. P IR C (tc) denotes this classification. To illustrate, suppose that R tc = 70% and P IR was evaluated 100 times; since 70% > 30% and the difference between R tc and F P R tc is significant, P IR C (tc) would be Non-Equivalent. Conversely, if R tc = 33%, the difference between R tc and F P R tc would not be statistically significant and P IR C (tc) would Equivalent.

As discussed above, the first part of the PIR evaluation method alleviates the impact of false positives for a single test case execution. However, because of non-determinism, it's also possible for P IR C (tc) to be a false positive. Typically, one has access to a test suite ts = {tc 1 , tc 2 , ...}. Each test case tc i ∈ ts would have been subjected to the first part of the PIR evaluation method to obtain an Equivalent or Non-Equivalent classification T CClassif ications = {P IR C (tc 1 ), P IR C (tc 2 ), ...}. The second part of the PIR evaluation method compares the proportion of Non-Equivalent to Equivalent classifications in T CClassif ications to a known false positive rate for T CClassif ications for the P IR under consideration using Pearsons χ 2 . This "known false positive rate" can be determined using the same methods as above. The results of this comparison is interpreted in the same way as in the first part of the evaluation method; the resulting classification is the P IR's final classification for the mutant.

Applying IMT

Multiple IRs In practice, one would typically leverage multiple IRs. Each IR may classify the mutant differently. This should be interpreted as follows: The mutant should be assumed to be non-equivalent if at least one IR classifies the mutant as non-equivalent, and should be considered to be equivalent if all IRs classify the mutant as equivalent.

Assumptions IMT assumes that an IR is encoded with accurate information about how Sys works. Unfortunately, this assumption may not hold if a real fault is in the system or IRs. To reduce the impact of this assumption, we recommend applying the IRs to Sys with a test suite. If any of the IRs indicate that the Sys is non-equivalent, then the assumption doesn't hold. In such cases, one can either modify the system and/or IRs, or remove IRs until all IRs report that Sys is equivalent. The same test suite should then be used for conducting IMT.

Constructing IRs s i and s o denote the program's input and output respectively. One must use one's domain knowledge to develop an intuition into how s i and s o are related. s i , s o and this intuition form an IOR. Tools that partially automate the exploration of relationships between inputs and outputs may simplify this task [START_REF] Chen | METRIC: METamorphic relation identification based on the category-choice framework[END_REF]. One must then leverage one's knowledge about the SUT's implementation details to identify execution trace behaviours that should manifest in executions in which this IOR is satisfied.

UCov is a test case coverage adequacy assessment tool for regression testing [START_REF] Assi | UCov: a user-defined coverage criterion for test case intent verification[END_REF]. Like IMT, UCov leverages execution trace behaviours to achieve its objective. However, these execution trace behaviours are used to assess the intent of a test case i.e. program behaviours that should be executed by the test case, whilst such behaviours are used by IMT to assess the intent of the SUT i.e. program behaviours that should manifest if the SUT has not been adversely affected by the mutation. Given their similarities, some of UCov's findings are relevant for IMT. For example, the aforementioned knowledge has been found to be available in the SUT's documentation [START_REF] Assi | UCov: a user-defined coverage criterion for test case intent verification[END_REF].

Automated program analytic tools like Program Slicing [START_REF] Harman | An overview of program slicing[END_REF] and Invariant Detection e.g. Daikon [START_REF] Harman | A comprehensive survey of trends in oracles for software testing[END_REF] can assist one in identifying useful execution trace behaviours. These behaviours are the IDs of IOR. This process is repeated to obtain multiple pairs IOR i , IDs i , where IOR i is an IOR and IDs i is a set of IDs that are associated with IOR i . Finally, one can group multiple pairs together, such that the IORs in these pairs have relationships. Identifying IORs that are amenable to such a grouping can be a natural task, because such IORs are typically highly related.

Experimental Set-up

Subject Program

The subject program is a Genetic Algorithm for the Bin Packing Problem that was developed by the author based on the design of Mladen Jankovic [START_REF] Jankovic | Genetic Algorithm for Bin Packing Problem[END_REF] with the JAGA Genetic Algorithm API toolbox [START_REF] Paperin | JAGA -Java API for Genetic Algorithms[END_REF]. The subject program consists of 1606 source lines of code (SLOC)2 , 29 classes and 244 methods (average 8 per class). The subject was partly selected to enhance the representativeness of the experiment and also minimise experimental bias. The former is achieved because it is non-deterministic and has weak information flow strength [START_REF] Masri | Prevalence of coincidental correctness and mitigation of its impact on fault localization[END_REF] and is thus susceptible to coincidental correctness. With regards to the latter, the implementation involves multiple developers, most of which were not aware of this research.

Interlocutory Relations

We used the same 48 IRs that were used in our previous work [START_REF] Patel | Interlocutory Testing: Combating Coincidental Correctness in Testing[END_REF]. For a comprehensive list of these IRs, please see [START_REF] Patel | Interlocutory Testing: Combating Coincidental Correctness in Testing[END_REF]. A real fault was present in the system, so we tested the assumption outlined in Section 3.3. We found that the assumption holds i.e. these IRs were not sensitive to the real fault. 42 IRs are Deterministic and 6 are Probabilistic.

Mutants

MuJava [START_REF] Ma | Mujava[END_REF] was used to generate 30 non-equivalent mutants. It was applied to all classes that significantly contributed to the SUT's core functionality. 11 interface classes (MuJava couldn't produce mutants for these), 2 unused classes and the test case input class were excluded. We also excluded 3 simple data classes and 2 abstract classes that stored a single object and only implemented getter/setter methods and/or just exposed methods that this object already has. For example, the simple data class may have an ArrayList ArrayObj and a method remove(i), which simply calls ArrayObj.remove(i). Finally, a comparator class was also excluded. Equivalent mutants and obvious mutants (i.e. mutants that resulted in system crashes or infinite loops) were also removed. We also rejected mutations of faulty code. These mutants were classified as either coincidentally correct or standard faults. Let S denote the system and M be a mutant of S. ORACLE is an oracle that checks all of S's output properties (listed below). This was achieved by using ORACLE on M 's output. If ORACLE fails, then the infected state didn't propagate to the output; thus M is coincidentally correct. We found that 15 were coincidentally correct and 15 were standard.

-Let DataSet be the set of items to be sorted into bins. The output O should be a permutation of DataSet. -O should contain at least one bin.

-O should not contain empty bins.

-O should not contain a bin that has more items than its capacity.

-O should not have a fitness that is greater than the maximum obtainable fitness (Fitness Function Constant).

Refactoring augments source code structure, while retaining behaviour; thus refactorings are effectively equivalent mutants. AutoRefactor [START_REF] Rouvignac | AutoRefactor[END_REF] was used to generate 30 equivalent mutants.

In summary, this experiment leverages 60 mutants in total, 30 non-equivalent and 30 equivalent.

Test Cases

We use the same test suite that was used in our previous work [START_REF] Patel | Interlocutory Testing: Combating Coincidental Correctness in Testing[END_REF]. The test suite consists of 100 test cases that were generated by Random Testing.

Results and Discussion

This section reports an empirical study that measures the accuracy of IMT for non-equivalent and equivalent mutants.

Non-Equivalent Mutants

IMT correctly classified 28/30 non-equivalent mutants. This suggests that IMT's classification accuracy can be high for non-equivalent mutants. Since the SUT is non-deterministic, this also demonstrates that the technique's classification accuracy for these mutants was not hampered by non-determinism. Specifically, 15/15 and 13/15 standard and coincidentally correct mutants were correctly classified. The difference in performance for these mutant types is not significant (Fisher's Exact Test: p > 0.05). This indicates that IMT can be effective for standard and coincidentally correct faults.

Recall that there are two types of IRs -Deterministic and Probabilistic IRs. These IRs are distinguished by the types of logic they are applied to -deterministic IRs are applied to aspects of the system that behave deterministically, whilst probabilistic IRs are applied to non-deterministic aspects of the system. To that end, each approach has different evaluation methods; the difference being, Probabilistic IRs leverage statistical techniques to factor out the effect of false positives that arise due to non-determinism. We therefore decided to further break down the analysis by these IR types. The difference in the Deterministic IR's performance for standard and coincidentally correct mutants is not statistically significant (Fisher's Exact Test: p > 0.05). This demonstrates that one can leverage these IRs in contexts where coincidental correctness is present, or absent. Each bar in Figure 1 represents a Deterministic IR that correctly classified a mutant. The height of the bar denotes the number of correctly classified non-equivalent mutants. Each bar also represents the proportion of mutants that were standard or coincidentally correct. Figure 1 demonstrates that some IRs are more accurate than others for different mutants. For example, the IR represented by the third bar correctly classifies standard mutants, but not coincidentally correct mutants, and the converse is true for the IR represented by the second bar.

19/30 (14/15 standard and 5/15 coincidentally correct) non-equivalent mutants were correctly classified by Probabilistic IRs. A comparison of the performance of Deterministic and Probabilistic IRs for standard faults revealed that the difference was not statistically significant (Fisher's Exact Test: p > 0.05), but was for coincidentally correct faults (Fisher's Exact Test: p < 0.05). This suggests that Probabilistic IRs may be less effective in situations where coincidental correctness is present. However, we observed that 3 of the coincidentally Fig. 2: Number of mutants that were correctly classified by Probabilistic IRs, broken down by mutant type correct faults found by IMT were uniquely identified by Probabilistic IRs, which means that they can add value in situations where coincidental correctness is present. Figure 2 presents the same information as in Figure 1, but for Probabilistic IRs; it shows the breakdown of the results; similar observations can be made to those in Figure 1.

As discussed above, all of the IRs collectively, correctly classified 28/30 nonequivalent mutants. Deterministic IRs and Probabilistic IRs correctly classified 23 and 19 mutants respectively, which means that neither IR type correctly classified all of the mutants on their own. This demonstrates that both IR types can add value.

Interestingly, these results also suggest that there was a substantial degree of overlap in terms of the number of mutants that were correctly classified by the IRs. We therefore decided to perform a subsumption analysis to determine the smallest number of IRs that would be required to obtain the same results. We found that only 12 were necessary: AverageFitnessGeneration, ChoosingPairsOfParentsComposition, CreateRandomIndividualNewBins, CrossoverRate, DecidingWhoShouldMutateFineGrained, GAController, Mutate-Individual, PartitionChild, ReplacementOperationIntegrity, ShouldUseNewIndividual, TerminateGA, TournamentComposition. This shows that the technique can be effective with relatively few IRs.

Equivalent Mutants

Promisingly, IMT correctly classified 30/30 equivalent mutants. Since Deterministic IRs don't check non-deterministic aspects of the system, they aren't susceptible to false positives, assuming that the assumption detailed in Section 3.3 holds. It's therefore not surprising that they did not misclassify any equivalent mutants. Since Probabilistic IRs do check such behaviours, false positives may be possible. To that end, we extended the evaluation method used by Probabilistic IRs, as described in Section 3.2, to curtail the incidence of false positives.

These results illustrate that this evaluation method was successful in achieving this goal.

Threats to Validity

There are several threats to validity. We attempted to address these where possible e.g. randomisation was used throughout the experiment to reduce experimental bias.

Firstly, the presence of real faults may confound the results i.e. an IR may assume that misbehaviour emanating from a real fault actually originated from the mutant process. To mitigated the impact of real faults on the experiment, we only used IRs that were not sensitive to the real fault and excluded mutations of the real fault.

Each IR is associated with a logging function. These logging functions capture data about the execution trace, during the execution of the SUT. Some mutants can alter the SUT's control flow. These alterations can cause the logging functions to crash. In such situations, the IR has effectively recognised that the SUT's control flow is incorrect and has thus correctly classified the nonequivalent mutant. Our experiment did not distinguish between these crashes and system crashes, and so they were conservatively removed. Therefore, the experimental results presented in this paper for non-equivalent mutants underestimate the technique's effectiveness. However, we do not believe that this had a significant impact on the results, since the technique already correctly classifies most of the mutants.

There is also a threat to generalisability; we only used one subject program. However, the subject program had the operating environment that we were studying i.e. non-determinism and a high propensity for coincidental correctness, and was therefore suitable for assessing our research objectives. As a part of ongoing research, we are currently applying IMT to four other subject programs; the preliminary results are promising, see Section 7.

Finally, the results demonstrated that different IRs obtained different levels of effectiveness. Thus, the effectiveness of the technique may vary considerably, depending on one's choice of IRs. This may be a threat to repeatability.

Conclusion

In this paper, we proposed Interlocutory Mutation Testing, the first mutant classification technique that can be applied in the presence of coincidental correctness and/or non-determinism. The technique correctly classified 93.33% of the non-equivalent mutants and 100% of the equivalent mutants, which suggests that the technique is capable of producing highly accurate results. We also observed that different IRs are more effective than others for classifying different faults, which suggests that using a diverse range of IRs can be valuable.

As mentioned in Section 6, one of the limitations of our study is that we only considered one subject program. As a part of on going research, we are currently conducting IMT on four other subject programs. A brief summary of the preliminary results are as follows. We applied IMT to Dijkstra's Algorithm. IMT obtained a non-equivalent mutant classification accuracy of 93.33%, and 100% mutant classification accuracy for equivalent mutants; 30 non-equivalent and 30 equivalent mutants were used. 34 mutants, which include a mixture of equivalent and non-equivalent mutants, were also generated across Bubble Sort, Binary Search and Knuth-Morris-Pratt. All of these mutants were correctly classified. It is our hope that these experiments will reduce the impact of this limitation.

Another limitation of our work is the effort required to apply the technique. Our experiment leveraged 48 IRs, which may be unacceptable in some cases. In Section 5.1, we observed that a small proportion (12) of the IRs subsumed all of the other IRs. This demonstrates that the technique can be applied with relatively few IRs, which may be more acceptable in the aforementioned cases, if one restricts their development efforts to such IRs. Unfortunately, the results did not indicate how one might do this. We would therefore like to investigate this in future work.

In Section 3.3, we detailed the partially automated process that is used to develop IRs. Increasing the degrees of automation further will also reduce the effort required to use the technique and so can reduce the impact of the limitation above. Thus, for future work, we would like to explore methods of automating the development of IRs further.

In the future, we would also like to assess the impact that IMT has on one's mutant classification productivity. This would involve determining the costs that are associated with developing IRs, and the cost savings that can be obtained from leveraging the technique. As a part of ongoing work, we are currently investigating the latter.

Fig. 1 :

 1 Fig. 1: Number of mutants that were correctly classified by Deterministic IRs, broken down by mutant type

Later we will see more complicated examples in which this process can help to overcome coincidental correctness.

We used the "Code Lines" metric in the Understand program[START_REF]Scitools: Understand static code analysis tool[END_REF] to compute SLOC. This metric ignores blank and comment lines.


Antti Jääskeläinen
email: antti.m.jaaskelainen@tut.fi

Towards Model Construction Based on Test Cases and GUI Extraction

Keywords: model extraction, model-based testing, software testing

The adoption of model-based testing techniques is hindered by the difficulty of creating a test model. Various techniques to automate the modelling process have been proposed, based on software process artefacts or an existing product. This paper outlines a hybrid approach to model construction, based on two previously proposed methods. The presented approach combines information in pre-existing test cases with a model extracted from the graphical user interface of the product.

Introduction

Model-based testing is a testing methodology that automates the generation of tests as well as their execution. In a typical approach, the tester first creates a formal model (such as a state machine) that depicts the behaviour of the system under test (SUT). The model is then explored by an automated tool in order to generate a sequence of actions to be used as a test. Models can also be used to otherwise support the testing process, such as in inspections.

A significant drawback of model-based testing is the skill and effort required in modelling. Creating a model that covers all the relevant aspects of the SUT, does so correctly, and is otherwise suitable for test generation, is no small task.

Various methods for easing or partially automating the modelling process have been proposed. Models can be generated from different artefacts of the software process, or the artefacts used directly as test models. Suitable candidates include specifications [START_REF] Ma | WSDL-based automated test data generation for web service[END_REF] and pre-existing test cases [START_REF] Jääskeläinen | Synthesizing test models from test cases[END_REF][START_REF] Xie | Mutually enhancing test generation and specification inference[END_REF]. Alternatively, models can be extracted from an existing product, either the source code [START_REF] Dallmeier | Generating test cases for specification mining[END_REF][START_REF] Silva | The GUISurfer tool: Towards a language independent approach to reverse engineering GUI code[END_REF][START_REF] Yang | A grey-box approach for automated GUI-model generation of mobile applications[END_REF], the structure and functionality of the graphical user interface (GUI) [START_REF] Aho | Industrial adoption of automatically extracted GUI models for testing[END_REF][START_REF] Grilo | Reverse engineering of GUI models for testing[END_REF][START_REF] Memon | GUI ripping: Reverse engineering of graphical user interfaces for testing[END_REF][START_REF] Memon | An event-flow model of GUI-based applications for testing[END_REF], or other known behaviour [START_REF] Hagerer | Model generation by moderated regular extrapolation[END_REF][START_REF] Hungar | Test-based model generation for legacy systems[END_REF]. Many of these methods also use the results of the generated tests to further hone the model.

This paper outlines a hybrid model construction method based on test cases and information extracted from the GUI. Information on the correct behaviour of the SUT in specific states is found in the test cases, and the states can be combined based on information gleaned from the GUI. In this way, weaknesses of each method can be compensated for with the strengths of the other. Hopefully, the new method could reduce the effort required to produce a useful test model.

The rest of the paper is structured as follows: Section 2 presents the two model construction methods that act as the basis for the new approach, which is outlined in Section 3. Section 4 considers the potential benefits of the approach. Finally, Section 5 concludes the paper with a more general discussion.

Automated Model Construction

The approach of this paper builds on two previously presented methods for constructing models to describe the SUT. The first is based on combining test cases into a model, the second on examining the GUI of the system.

Synthesis from Test Cases

The model synthesis process proposed in [START_REF] Jääskeläinen | Synthesizing test models from test cases[END_REF] is based on pre-existing test cases that are linear sequences of automatically executable steps (keywords), and consists of five phases: First, keywords used in test cases are identified and classified. Second, part of the information in the test cases (such as input data) is separated into variables. Third, an initialization sequence for the test model is prepared. Fourth, important states in the test cases are identified manually. Finally, the actual merging of the test cases takes place.

In the merging phase, the linear state sequences of the test cases are combined into a more complex model by merging some of the states with each other. The previously identified common states in the test cases are trivially merged. However, states in different test cases may also be combined if they are reached by the same sequence of keywords, which suggests that the cases are in fact handling the same part of the SUT. Separating input data into variables allows states to be combined even if the stored inputs would actually leave the system in different states, as the data can be combined back into the model afterward.

Although this method works, it relies on a significant amount of manual effort. In particular, the separation of variables requires significant work and skill [START_REF] Jääskeläinen | Synthesizing test models from test cases[END_REF]. Also, the tester has to confirm the merges between the test cases manually, as the state sequence method may generate false positives [START_REF] Jääskeläinen | Synthesizing test models from test cases[END_REF]. Thus, the practicality of the method as presented is questionable.

Extraction from GUI

As an example of methods that extract a model out of a GUI we consider Murphy, a tool that examines the GUI of an application, tries out different functions, and builds a model to describe its observations [START_REF] Aho | Industrial adoption of automatically extracted GUI models for testing[END_REF]. It can use various methods to access the GUI, or crawl through it. The publicly available version [START_REF]GitHub -F-Secure/murphy[END_REF] provides crawlers that use Windows APIs or cycle through GUI controls with the tabulator key. The constructed model is a graph with a node for each observable state of the application.

Murphy starts out at desktop, and launches the application with a predefined command. These two application states, not running and just launched, form the two first nodes in the constructed graph. In each GUI state, Murphy maps out the controls found in it. Then it proceeds to try out a control, such as clicking a button, and considers the resulting state of the GUI. A given state of the application is identified by the controls that can be found in its GUI, while ignoring the data such as the contents of text labels. Based on these, Murphy will either create a transition to an existing node or add a new node to the graph. Extraction can be performed in multiple runs starting from the desktop, with the results combined into a single graph.

Visual inspection of the extracted models can be very helpful in finding errors, and the models can support manual testing of the application [START_REF] Aho | Murphy tools: Utilizing extracted GUI models for industrial software testing[END_REF]. They can also be used for automated regression testing by comparing the extracted models between different versions of the application or using an extracted sequence as a smoke test for the next version [START_REF] Aho | Murphy tools: Utilizing extracted GUI models for industrial software testing[END_REF]. That said, their usefulness for test generation is limited: they can make no difference between an erroneous feature and a correct one, and contain no verifications of the system state beyond finding the expected controls in the GUI. Also, specific input data has to be added into the extraction script manually, as it cannot be inferred from the GUI.

Combined Methodology

Both approaches described above have their drawbacks. In the test case synthesis method, the test cases provide detailed information of what can and should happen in different situations, but constructing a model out of them is difficult.

In the GUI extraction method, a graph to describe the SUT can be constructed with little manual effort, but its understanding of the SUT is limited. But what if the two were combined?

If we have a ready set of test cases when we begin the extraction process, then we can track the actions taken in the GUI within the cases. For each node of the constructed graph, we will have a set of test cases that reach the corresponding SUT state at a specific point of their execution. Then, we can examine the next steps in those cases for information on the current state of the SUT and the actions available in it. The process could work as follows:

1. Before extraction, establish a correspondence between the keywords within the test cases and actions supported by the extraction crawler. This is trivial if the two use the same mechanism for accessing the GUI, and should be doable with any mechanisms that understand the structure of a GUI. Also, make note of any keywords used to verify the state of the SUT without changing it. 2. At the beginning of an extraction run, start with the full set of test cases at their initial states. When the extractor performs an action, examine the cases to see if they would execute the corresponding keyword next, skipping past any keywords that do not change the state of the SUT. Advance these cases past that keyword, and discard the other cases in the set. Make a note that this node can be reached by the remaining test cases at their current stage.

3. At each node, examine the test cases that can reach it. Any verifications performed by the test cases at this node can be added into the model. Also, the next keywords in the cases should be executable in the GUI, even if the crawler fails to find a corresponding control. In particular, test data in the cases, such as the parameter of a type text keyword, can be used as an input.

This process produces a model that incorporates and combines both the information extractable from the SUT and that present in the test cases. It may even contain functionality present in neither, if the test cases provide the crawler access to a part of the GUI it could not reach on its own.

Potential Applications

Combining the test case synthesis and GUI extraction methods as described above offers several potential benefits. Either of the test cases or the extracted model can be used to support a testing approach based on the other. The resulting model can also act as a basis for a manually maintained test model.

If the testing process is based on test cases, their coverage can be increased with the information extracted from the GUI. With the extracted information, it is possible to tell when two test cases reach the same SUT state, or when a test case loops back into a state it has already visited. By using the model for test generation, it is possible to reach a state by a keyword sequence taken from one test case and continue with a sequence from another, even if such a combination does not occur in any of the original cases. A model that loops back into itself at several points can be particularly useful in robustness testing: properly directed, a test run can continue indefinitely without simply repeating a single sequence of keywords over and over.

Conversely, in a testing process based on the extracted model, the test cases can improve the quality of that model. They can improve model coverage by supplying performable actions that cannot be identified in the GUI, and in particular by providing realistic test data. Also, the verifications in the test cases improve the ability of the model to detect errors.

Finally, the constructed model can support a move to proper model-based testing, where the tests are generated from the model. Creating a test model can be a daunting task, especially if a fairly complete product already exists, so that the model cannot be developed incrementally as new features are added. In this situation, a method for automatically constructing a preliminary model can be helpful, even though some augmentation and refactoring is likely to be required. A model extracted purely from the GUI can already be useful here, but the increased coverage and verifications added by the test cases can take this support further.

Discussion

The previous sections have outlined a method for constructing models based on information in test cases and the GUI of the SUT. The resulting models can be used to improve test coverage in a testing approach based on test cases, or to better support static analysis and exploratory techniques. The method is language-independent, and only requires the SUT to have a GUI that can be handled by test automation. Obviously, it assumes the existence of some manually created test cases, and is thus primarily suited for testing approaches that will have those anyway. Practical experience will be required to see whether writing test cases specifically for this method could be worthwhile.

As presented here, the GUI extraction part of the process is based on the Murphy tool. However, there is nothing tool-specific in the approach itself, and other tools can be used, as well. The basic requirement is that the tool can distinguish different GUI events from each other, so that they can be matched with those occurring in the test cases. The test cases must naturally have a similar level of abstraction.

At this point, a prototype tool for the methodology is under development. The prototype can be used to estimate the practicality of the approach, although it will likely be unable to handle complex applications due to the limitations in the crawler component of the freely available version of Murphy [START_REF]GitHub -F-Secure/murphy[END_REF]. For industrial use, integration with a professional quality test execution tool will be required.

There is likely also room for improvement in the methodology presented here. For example, it may be possible to factor out inputs from the test cases so that we could produce separate models for the control graph and saved data. Detecting the input data as identical output later on should be simple, but potential effects of data on the control graph could be more difficult to identify, and modified versions of the data impossible to recognize without domain knowledge. Likewise, it remains to be seen whether the Murphy approach of ignoring data in the GUI when identifying states is the best solution for the new method.

If the test cases have been created using action words and keywords [START_REF] Buwalda | Action figures[END_REF], it might be possible to import these two tiers of abstraction into the constructed model. Presenting the model at a higher level of abstraction could make analysing it significantly easier, and produce a better basis for a full-fledged test model.

Acknowledgements

Funding by Ulla Tuominen Foundation is gratefully acknowledged.