word-parse/words/Bos2017_Chapter_N-CompleteTestSuitesForIOCO.txt

n-Complete Test Suites for IOCO
Petra van den Bos(B) , Ramon Janssen, and Joshua Moerman
Institute for Computing and Information Sciences,
Radboud University, Nijmegen, The Netherlands
{petra,ramonjanssen,joshua.moerman}@cs.ru.nl

Abstract. An n-complete test suite for automata guarantees to detect
all faulty implementations with a bounded number of states. This
principle is well-known when testing FSMs for equivalence, but the problem becomes harder for ioco conformance on labeled transitions systems.
Existing methods restrict the structure of specifications and implementations. We eliminate those restrictions, using only the number of implementation states, and fairness in test execution. We provide a formalization,
a construction and a correctness proof for n-complete test suites for ioco.

1

Introduction

The holy grail of model-based testing is a complete test suite: a test suite that
can detect any possible faulty implementation. For black-box testing, this is
impossible: a tester can only make a finite number of observations, but for an
implementation of unknown size, it is unclear when to stop. Often, a so called
n-complete test suite is used to tackle this problem, meaning it is complete for
all implementations with at most n states.
For specifications modeled as finite state machines (FSMs) (also called Mealy
machines), this has already been investigated extensively. In this paper we
will explore how an n-complete test suite can be constructed for suspension
automata. We use the ioco relation [11] instead of equivalence of FSMs.
An n-complete test suite for FSM equivalence usually provides some way
to reach all states and transitions of the implementation. After reaching some
state, it is tested whether this is the correct state, by observing behavior which
is unique for that state, and hence distinguishing it from all other states.
Unlike FSM equivalence, ioco is not an equivalence relation, meaning that different implementations may conform to the same specification and, conversely,
an implementation may conform to different specifications. In this paper, we
focus on the problem of distinguishing states. For ioco, this cannot be done with
simple identification. If an implementation state conforms to multiple specifications states, those states are defined to be compatible. Incompatible states can
be handled in ways comparable to FSM-methods, but distinguishing compatible
states requires more effort.
P. van den Bos and R. Janssen—Supported by NWO project 13859 (SUMBAT).
c IFIP International Federation for Information Processing 2017

Published by Springer International Publishing AG 2017. All Rights Reserved
N. Yevtushenko et al. (Eds.): ICTSS 2017, LNCS 10533, pp. 91–107, 2017.
DOI: 10.1007/978-3-319-67549-7 6

92

P. van den Bos et al.

In this paper, we give a structured approach for distinguishing incompatible
states. We also propose a strategy to handle compatible states. Obviously, they
cannot be distinguished in the sense of incompatible states. We thus change the
aim of distinguishing: instead of forcing a non-conformance to either specification
state, we may also prove conformance to both. As our only tool in proving this
is by further testing, this is a recursive problem: during complete testing, we are
required to prove conformance to multiple states by testing. We thus introduce a
recursively defined test suite. We give examples where this still gives a finite test
suite, together with a completeness proof for this approach. To show an upper
bound for the required size of a test suite, we also show that an n-complete test
suite with finite size can always be constructed, albeit an inefficient one.
Related Work. Testing methods for Finite State Machines (FSMs) have been
analyzed thoroughly, and n-complete test suites are already known for quite
a while. A survey is given in [3]. Progress has been made on generalizing these
testing methods to nondeterministic FSMs, for example in [6,9]. FSM-based work
that more closely resembles ioco is reduction of non-deterministic FSMs [4].
Complete testing in ioco received less attention than in FSM theory on this
subject. The original test generation method [11] is an approach in which test
cases are generated randomly. The method is complete in the sense that any
fault can be found, but there is no upper bound to the required number and
length of test cases.
In [8], complete test suites are constructed for Mealy-IOTSes. Mealy-IOTSes
are a subclass of suspension automata, but are similar to Mealy machines as
(sequences of) outputs are coupled to inputs. This makes the transition from
FSM testing more straightforward.
The work most similar to ours [10] works on deterministic labeled transition systems, adding quiescence afterwards, as usual for ioco. Non-deterministic
models are thus not considered, and cannot be handled implicitly through determinization, as determinization can only be done after adding quiescence. Some
further restrictions are made on the specification domains. In particular, all
specification states should be reachable without depending on choices for output transitions of the implementation. Furthermore, all states should be mutually incompatible. In this sense, our test suite construction can be applied to
a broader set of systems, but will potentially be much less efficient. Thus, we
prioritize exploring the bounds of n-complete test suites for ioco, whereas [10]
aims at efficient test suites, by restricting the models which can be handled.

2

Preliminaries

The original ioco theory is defined for labeled transition systems, which may
contain internal transitions, be nondeterministic, and may have states without outputs [11]. To every state without outputs, a self-loop with quiescence is
added as an artificial output. The resulting labeled transition system is then
determinized to create a suspension automaton, which is equivalent to the initial

n-Complete Test Suites for IOCO

93

labeled transition system with respect to ioco [13]. In this paper, we will consider a slight generalization of suspension automata, such that our results hold
for ioco in general: quiescent transitions usually have some restrictions, but we
do not require them and we will treat quiescence as any other output. We will
define them in terms of general automata with inputs and outputs.
Definition 1. An I/O-automaton is a tuple (Q, LI , LO , T, q0 ) where
–
–
–
–
–

Q is a finite set of states
LI is a finite set of input labels
LO is a finite set of output labels
T : Q × (LI ∪ LO )  Q is the (partial) transition function
q0 ∈ Q is the initial state

We denote the domain of I/O-automata for LI and LO with A(LI , LO ).
For the remainder of this paper we fix LI and LO as disjoint sets of input and
output labels respectively, with L = LI ∪ LO , and omit them if clear from the
context. Furthermore, we use a, b as input symbols and x, y, z as output symbols.
Definition 2. Let S = (Q, LI , LO , T, q0 ) ∈ A, q ∈ Q, B ⊆ Q, μ ∈ L and
σ ∈ L∗ . Then we define:


∅
if T (q, μ) = ⊥
q after μ =
{T (q, μ)} otherwise
 
q after μ
B after μ =
q  ∈B

q after  = {q}
q after μσ = (q after μ) after σ

B after σ =



q  after σ

q  ∈B

out(B) = {x ∈ LO | B after x = ∅}
in(B) = {a ∈ LI | B after a = ∅}
init(B) = in(B) ∪ out(B)
Straces(B) = {σ  ∈ L∗ | B after σ  = ∅}



S is output-enabled if ∀p ∈ Q : out(p) = ∅ SA = {S ∈ A | S is output-enabled}


S is input-enabled if ∀p ∈ Q : in(p) = LI SAIE = {S ∈ SA | S is input-enabled}

We interchange singleton sets with its element, e.g. we write out(q) instead
of out({q}). Definitions on states will sometimes be used for automata as well,
acting on their initial states. Similarly, definitions on automata will be used for
states, acting on the automaton with that state as its initial state. For example,
for S = (Q, LI , LO , T, q0 ) ∈ A and q ∈ Q, we may write S after μ instead of q0
after μ, and we may write that q is input-enabled if S is input-enabled.
In this paper, specifications are suspension automata in SA, and implementations are input-enabled suspension automata in SAIE . The ioco relation formalizes when implementations conform to specifications. We give a definition
relating suspension automata, following [11], and the coinductive definition [7]
relating states. Both definitions have been proven to coincide.
Definition 3. Let S ∈ SA, and I ∈ SAIE . Then we say that I ioco S if ∀σ ∈
Straces(S) : out(I after σ) ⊆out(S after σ).

94

P. van den Bos et al.

Definition 4. Let S = (Qs , LI , LO , Ts , q0s ) ∈ SA, and I = (Qi , LI , LO , Ti , q0i ) ∈
SAIE . Then for qi ∈ Qi , qs ∈ Qs , we say that qi ioco qs if there exists a
coinductive ioco relation R ⊆ Qi × Qs such that (qi , qs ) ∈ R, and ∀(q, p) ∈ R:
– ∀a ∈ in(p) : (q after a, p after a) ∈ R
– ∀x ∈ out(q) : x ∈ out(p) ∧ (q after x, p after x) ∈ R
In order to define complete test suites, we require execution of tests to be
fair : if a trace σ is performed often enough, then every output x appearing
in the implementation after σ will eventually be observed. Furthermore, the
implementation may give an output after σ before the tester can supply an
input. We then assume that the tester will eventually succeed in performing
this input after σ. This fairness assumption is unavoidable for any notion of
completeness in testing suspension automata: a fault can never be detected if an
implementation always chooses paths that avoid this fault.

3

Distinguishing Experiments

An important part of n-complete test suites for FSM equivalence is the distinguishing sequence, used to identify an implementation state. As ioco is not
an equivalence relation, there does not have to be a one-to-one correspondence
between specification and implementation states.
3.1

Equivalence and Compatibility

We first describe equivalence and compatibility relations between states, in order
to define distinguishing experiments. We consider two specifications to be equivalent, denoted S1 ≈ S2 , if they have the same implementations conforming to
them. Then, for all implementations I, we have I ioco S1 iff I ioco S2 . For two
inequivalent specifications, there is thus an implementation which conforms to
one, but not the other.
Intuitively, equivalence relates states with the same traces. However, implicit
underspecification by absent inputs should be handled equivalently to explicit
underspecification with chaos. This is done by using chaotic completion [11].
This definition of equivalence is inspired by the relation wioco [12], which relates
specifications based on their sets of traces.
Definition 5. Let (Q, LI , LO , T, q0 ) ∈ SA. Define chaos, a specification to
which every implementation conforms, as X = ({χ}, LI , LO , {(χ, x, χ) | x ∈
L}, χ). Let QX = Q ∪ {χ}. The relation ≈ ⊆ QX × QX relates all equivalent
states. It is the largest relation for which it holds that q ≈ q  if:
out(q) = out(q  ) ∧ (∀μ ∈ init(q) ∩ init(q  ) : q after μ ≈ q  after μ)
∧ (∀a ∈ in(q)\in(q  ) : q after a ≈ χ) ∧ (∀a ∈ in(q  )\in(q) : q  after a ≈ χ)

n-Complete Test Suites for IOCO

95

For two inequivalent specifications, there may still exist an implementation
that conforms to the two. In that case, we define the specifications to be compatible, following the terminology introduced in [9,10]. We introduce an explicit
relation for compatibility.
Definition 6. Let (Q, LI , LO , T, q0 ) ∈ SA. The relation ♦ ⊆ Q × Q relates all
compatible states. It is the largest relation for which it holds that q ♦ q  if:
(∀a ∈ in(q) ∩ in(q  ) : q after a ♦ q  after a)
∧ (∃x ∈ out(q) ∩ out(q  ) : q after x ♦ q  after x)
Compatibility is symmetric and reflexive, but not transitive. Conversely, two
specifications are incompatible if there exists no implementation conforming to
both. When q1 ♦ q2 , we can indeed easily make an implementation which conforms to both q1 and q2 : the set of outputs of the implementation state can
simply be out(q1 )∩out(q2 ), which is non-empty by definition of ♦. Upon such
an output transition or any input transition, the two successor states are again
compatible, thus the implementation can keep picking transitions in this manner. For example, in Fig. 1, compatible states 2 and 3 of the specification are
both implemented by state 2 of the implementation.

a

3

a
x

4

y
x
y

x

1

2

x
6

y

a

5

z

(a) Specification S with 2 ♦ 3.

a

3

a
x

4
a

x
y

x

1
a x
6
z

y

2∧3
2

a

5
a

(b) An implementation of S.

a
4∧5

x
6

y
z

(c) The merge of specification states 2 and 3.

Fig. 1. A specification, an implementation, and a merge of two states.

Beneš et al. [1] describe the construction of merging specifications. For specification states qs and qs , their merge is denoted qs ∧ qs . For any implementation
state qi , it holds that qi ioco qs ∧ qi ioco qs ⇐⇒ qi ioco (qs ∧ qs ). Intuitively, a
merge of two states thus only allows behavior allowed by both states. Figure 1c
shows the merge of specification states 2 and 3. The merge of qs and qs can be
implemented if and only if qs ♦ qs : indeed, for incompatible states, the merge
has states without any output transitions, which is denoted invalid in [1].
3.2

Distinguishing Trees

When an implementation is in state qi , two incompatible specification states qs
and qs are distinguished by showing to which of the two qi conforms, assuming
that it conforms to one. Conversely, we can say that we have to show a nonconformance of qi to qs or qs . Generally, a set of states D is distinguished by

96

P. van den Bos et al.

showing non-conformance to all its states, possibly except one. As a base case,
if |D| ≤ 1, then D is already distinguished. We will construct a distinguishing
tree as an input-enabled automaton which distinguishes D after reaching pass.
Definition
7. Let μ be a symbol and D a set of states. Then injective(μ, D) if

μ ∈ {in(q) | q ∈ D} ∪ LO ∧ ∀q, q  ∈ D : q = q  ∧ μ ∈init(q)∩init(q  ) =⇒ q
after μ = q  after μ. This is extended to sets of symbols Σ as injective(Σ, D) if
∀μ ∈ Σ : injective(μ, D).
Definition 8. Let (Q, LI , LO , T, q0 ) ∈ SA(LI , LO ), and D ⊆ Q a set of mutually incompatible states. Then define DT (LI , LO , D) ⊆ A(LO , LI ) inductively
as the domain of input-enabled distinguishing trees for D, such that for every
Y ∈ DT (LI , LO , D) with initial state t0 :
– if |D| ≤ 1, then t0 is the verdict state pass, and
– if |D| > 1, then t0 has either
• a transition for a single input a ∈ LI to a Y  ∈ DT (LI , LO , D after a)
such that injective(a, D), and transitions to a verdict state reset for all
x ∈ LO , or
• a transition for every output x ∈ LO to a Y  ∈ DT (LI , LO , D after x)
such that injective(x, D).
Furthermore, pass or reset is always reached after a finite number of steps,
and these states are sink states, i.e. contain transitions only to itself.
A distinguishing tree can synchronize with an implementation to reach a
verdict state. As an implementation is output-enabled and the distinguishing
tree is input-enabled, this never blocks. If the tree performs an input, the implementation may provide an output first, resulting in reset: another attempt is
needed to perform the input. If no input is performed by the tree, it waits for
any output, after which it can continue. In this way, the tester is guaranteed to
steer the implementation to a pass, where the specification states disagree on
the allowed outputs: the implementation has to choose an output, thus has to
choose which specifications (not) to implement.
For a set D of mutually incompatible states, such a tree may not exist. For
example, consider states 1, 3 and 5 in Fig. 2. States 1 and 3 both lead to the
same state after a, and can therefore not be distinguished. Similarly, states 3
and 5 cannot be distinguished after b. Labels a and b are therefore not injective
according to Definition 7 and should not be used. This concept is similar in FSM
testing [5]. A distinguishing sequence always exists when |D| = 2. When |D| > 2,
we can thus use multiple experiments to separate all states pairwise.
Lemma 9. Let S ∈ SA. Let q and q  be two states of S, such that q ♦ q  . Then
there exists a distinguishing tree for q and q  .
Proof. Since q ♦ q  , we know that:
(∃a ∈ in(q) ∩ in(q  ) : q after a ♦ q  after a)
∨ (∀x ∈ out(q) ∩ out(q  ) : q after x ♦ q  after x)

n-Complete Test Suites for IOCO

97

So we have that some input or all outputs, enabled in both q and q  , lead to
incompatible states, for which this holds again. Hence, we can construct a tree
with nodes that either have a child for an enabled input of both states, or
children for all outputs enabled in the states (children for not enabled outputs
are distinguishing trees for ∅), as in the second case of Definition 8. If this tree
would be infinite, then this tree would describe infinite sequences of labels. Since
S is finite, such a sequence would be a cycle in S. This would mean that q ♦ q  ,
which is not the case. Hence we have that the tree is finite, as required by
Definition 8.


z
5

a
y
b

a
4

b

3
z

a

2

x

z
1

b

Fig. 2. No distinguishing tree exists for {1,3,5}.

3.3

Distinguishing Compatible States

Distinguishing techniques such as described in Sect. 3.2 rely on incompatibility
of two specifications, by steering the implementation to a point where the specifications disagree on the allowed outputs. This technique fails for compatible specifications, as an implementation state may conform to both specifications. Thus,
a tester then cannot steer the implementation to showing a non-conformance to
either.
We thus extend the aim of a distinguishing experiment: instead of showing a
non-conformance to any of two compatible states qs and qs , we may also prove
conformance to both. This can be achieved with an n-complete test suite for
qs ∧ qs ; this will be explained in Sect. 4.1. Note that even for an implementation
which does not conform to one of the specifications, n-complete testing is needed.
Such an implementation may be distinguished, but it is unknown how, due to
compatibility. See for example the specification and implementation of Fig. 1.
State 2 of the implementation can only be distinguished from state 3 by observing
ax, which is non-conforming behavior for state 2. Although y would also be nonconforming for state 2, this behavior is not observed.
In case that a non-conformance to the merged specification is found with an
n-complete test suite, then the outcome is similar to that of a distinguishing tree
for incompatible states: we have disproven conformance to one of the individual
specifications (or to both).

4

Test Suite Definition

The number n of an n-complete test suite T of a specification S tells how many
states an implementation I is allowed to have to give the guarantee that I ioco

98

P. van den Bos et al.

S after passing T (we will define passing a test suite later). To do this, we must
only count the states relevant for conformance.
Definition 10. Let S = (Qs , LI , LO , T, q0s ) ∈ SA, and I = (Qi , LI , LO , Ti , q0i ) ∈
SAIE . Then,
– A state qs ∈ Qs is reachable if ∃σ ∈ L∗ : S after σ = qs .
– A state qi ∈ Qi is specified if ∃σ ∈ Straces(S) : I after σ = qi . A transition
(qi , μ, qi ) ∈ Ti is specified if qi is specified, and if either μ ∈ LO , or μ ∈
LI ∧ ∃σ ∈ L∗ : I after σ = qi ∧ σμ ∈ Straces(S).
– We denote the number of reachable states of S with |S|, and the number of
specified, reachable states of I with |I|.
Definition 11. Let S ∈ SA be a specification. Then a test suite T for S is
n-complete if for each implementation I: I passes T =⇒ (I ioco S ∨ |I| > n).
In particular, |S|-complete means that if an implementation passes the test
suite, then the implementation is correct (w.r.t. ioco) or it has strictly more
states than the specification. Some authors use the convention that n denotes
the number of extra states (so the above would be called 0-completeness).
To define a full complete test suite, we first define sets of distinguishing
experiments.
Definition 12. Let (Q, LI , LO , T, q0 ) ∈ SA. For any state q ∈ Q, we choose a
set W (q) of distinguishing experiments, such that for all q  ∈ Q with q = q  :
– if q ♦ q  , then W (q) contains a distinguishing tree for D ⊆ Q, s.t. q, q  ∈ D.
– if q ♦ q  , then W (q) contains a complete test suite for q ∧ q  .
Moreover, we need sequences to access all specified, reachable implementation
states. After such sequences distinguishing experiments can be executed. We will
defer the explicit construction of the set of access sequences. For now we assume
some set P of access sequences to exist.
Definition 13. Let S ∈ SA and I ∈ SAIE . Let P be a set of access sequences
and let P + = {σ ∈ P ∪ P · L | S after σ = ∅}. Then the distinguishing test suite
is defined as T = {στ | σ ∈ P + , τ ∈ W (q0 after σ)}. An element t ∈ T is a test.
4.1

Distinguishing Experiments for Compatible States

The distinguishing test suite relies on executing distinguishing experiments. If
a specification contains compatible states, the test suite contains distinguishing
experiments which are themselves n-complete test suites. This is thus a recursive
construction: we need to show that such a test suite is finite. For particular
specifications, recursive repetition of the distinguishing test suite as described
above is already finite. For example, specification S in Fig. 1 contains compatible
states, but in the merge of every two compatible states, no further compatible
states remain. A test suite for S needs to distinguish states 2 and 3. For this

n-Complete Test Suites for IOCO

99

purpose, it uses an n-complete test suite for 2 ∧ 3, which contains no compatible
states, and thus terminates by only containing distinguishing trees.
However, the merge of two compatible states may in general again contain
compatible states. In these cases, recursive repetition of distinguishing test suites
may not terminate. An alternative unconditional n-complete test suite may be
constructed using state counting methods [4], as shown in the next section.
Although inefficient, it shows the possibility of unconditional termination. The
recursive strategy thus may serve as a starting point for other, efficient constructions for n-complete test suites.
Unconditional n-complete Test Suites. We introduce Lemma 16 to bound
test suite execution. We first define some auxiliary definitions.
Definition 14. Let S ∈ SA, σ ∈ L∗ , and x ∈ LO . Then σx is an iococounterexample if S after σ = ∅, x ∈out(S after σ).
Naturally, I ioco S if and only if Straces(I) contains no ioco-counterexample.
Definition 15. Let S = (Qs , LI , LO , Ts , qs0 ) ∈ SA and I ∈ SAIE . A trace σ ∈
Straces(S) is short if ∀qs ∈ Qs : |{ρ | ρ is a prefix of σ ∧ qs0 after ρ = qs }| ≤ |I|.
 S, then Straces(I) contains
Lemma 16. Let S ∈ SA and I ∈ SAIE . If I ioco

a short ioco-counterexample.
 S, then Straces(I) must contain an ioco-counterexample σ. If
Proof. If I ioco

σ is short, the proof is trivial, so assume it is not. Hence, there exists a state
qs , with at least |I| + 1 prefixes of σ leading to qs . At least two of those prefixes
ρ and ρ must lead to the same implementation state, i.e. it holds that qi0 after
ρ = qi0 after ρ and qs0 after ρ = qs0 after ρ . Assuming |ρ| < |ρ | without loss
of generality, we can thus create an ioco-counterexample σ  shorter than σ by

replacing ρ by ρ. If σ  is still not short, we can repeat this process until it is. 
We can use Lemma 16 to bound exhaustive testing to obtain n-completeness.
When any specification state is visited |I| + 1 times with any trace, then any
extensions of this trace will not be short, and we do not need to test them.
Fairness allows us to test all short traces which are present in the implementation.
Corollary 17. Given a specification S the set of all traces of length at most
|S| ∗ n is an n-complete test suite.
Example 18. Figure 3 shows an example of a non-conforming implementation
with a counterexample yyxyyxyyxyyx, of maximal length 4 · 3 = 12.
4.2

Execution of Test Suites

A test στ is executed by following σ, and then executing the distinguishing
experiment τ . If the implementation chooses any output deviating from σ, then
the test gives a reset and should be reattempted. Finishing τ may take several

100

P. van den Bos et al.
x
1
y
4

y
y
x

2
y

x
3

(a) Specification S.

x
3

1
y

y
2

(b) Implementation I.

Fig. 3. A specification, and a non-conforming implementation.

executions: a distinguishing tree may give a reset, and an n-complete test suite
to distinguish compatible states may contain multiple tests. Therefore σ needs
to be run multiple times, in order to allow full execution of the distinguishing
experiment. By assuming fairness, every distinguishing experiment is guaranteed
to termininate, and thus also every test.
The verdict of a test suite T for specification S is concluded simply by checking for observed ioco-counterexamples to S during execution. When executing
a distinguishing experiment w as part of T, the verdict of w is ignored when
concluding a verdict for T: we only require w to be fully executed, i.e. be reattempted if it gives a reset, until it gives a pass or fail. For example, if σ leads
to specification state q, and q needs to be distinguished from compatible state
q  , a test suite T for q ∧ q  is needed to distinguished q and q  . If T finds a
non-conformance to either q or q  , it yields fail. Only in the former case, T will
also yield fail, and in the latter case, T will continue with other tests: q and
q  have been successfully distinguished, but no non-conformance to q has been
found. If all tests have been executed in this manner, T will conclude pass.
4.3

Access Sequences

In FSM-based testing, the set P for reaching all implementation states is taken
care of rather efficiently. The set P is constructed by choosing a word σ for
each specification state, such that σ leads to that state (note the FSMs are fully
deterministic). By passing the tests P · W , where W is a set of distinguishing
experiment for every reached state, we know the implementation has at least
some number of states (by observing that many different behaviors). By passing
tests P ·L·W we also verify that every transition has the correct
 destination state.
By extending these tests to P · L≤k+1 · W (where L≤k+1 = m∈{0,··· ,k+1} Lm ),
we can reach all implementation states if the implementation has at most k
more states than the specification. For suspension automata, however, things
are more difficult for two reasons: (1) A specification state may be reachable
only if an implementation chooses to implement a particular, optional output
transition (in which case this state is not certainly reachable [10]), and (2) if
the specification has compatible states, the implementation may implement two
specification states with a single implementation state.
Consider Fig. 4 for an example. An implementation can omit state 2 of the
specification, as shown in Fig. 4b. Now Fig. 4c shows a fault not found by a test

n-Complete Test Suites for IOCO

101

suite P · L≤1 · W : if we take y ∈ P , z ∈ L, and observe z ∈ W (3), we do not
reach the faulty y transition in the implementation. So by leaving out states, we
introduce an opportunity to make a fault without needing more states than the
specification. This means that we may need to increase the size of the test suite
in order to obtain the desired completeness. In this example, however, a test
suite P · L≤2 · W is enough, as the test suite will contain a test with yzz ∈ P · L2
after which the faulty output y ∈ W (3) will be observed.

x
y

2

1

3

(a) Specification S.

z

y

z

y

y

z
(b) Conforming implementation.

z
(c) Non-conforming
implementation.

Fig. 4. A specification with not certainly reachable states 2 and 3.

Clearly, we reach all states in a n-state implementation for any specification
S, by taking P to be all traces in Straces(S) of at most length n. This set P
can be constructed by simple enumeration. We then have that the traces in the
set P will reach all specified, reachable states in all implementations I such that
|I| ≤ n. In particular this will mean that P + reaches all specified transitions.
Although this generates exponentially many sequences, the length is substantially shorter than the sequences obtained by the unconditional n-complete test
suite. We conjecture that a much more efficient construction is possible with a
careful analysis of compatible states and the not certainly reachable states.
4.4

Completeness Proof for Distinguishing Test Suites

We let T be the distinguishing test suite as defined in Definition 13. As discussed
before, if q and q  are compatible, the set W (q) can be defined using another
complete test suite. If the test suite is again a distinguishing test suite, completeness of it is an induction hypothesis. If, on the other hand, the unconditional
n-complete test suite is used, completeness is already guaranteed (Corollary 17).
Theorem 19. Let S = (Qs , LI , LO , Ts , q0s ) ∈ SA be a specification. Let T be a
distinguishing test suite for S. Then T is n-complete.
Proof. We will show that for any implementation of the correct size and which
passes the test suite we can build a coinductive ioco relation which contain the
initial states. As a basis for that relation we take the states which are reached by
the set P . This may not be an ioco relation, but by extending it (in two steps)
we obtain a full ioco relation. Extending the relation is an instance of a so-called
up-to technique, we will use terminology from [2].

102

P. van den Bos et al.

More precisely, Let I = (Qi , LI , LO , Ti , q0i ) ∈ SAIE be an implementation
with |I| ≤ n which passes T. By construction of P , all reachable specified implementation states are reached by P and so all specified transitions are reached
by P + .
The set P defines a subset of Qi × Qs , namely R = {(q0i after σ, q0s
after σ) | σ ∈ P }. We add relations for all equivalent states: R = {(i, s) |
(i, s ) ∈ R, s ∈ Qs , s ≈ s }. Furthermore, let J = {(i, s, s ) | i ∈ Qi , s, s ∈
Qs such that i ioco s ∧ i ioco 
s } and Ri,s,s be the ioco relation for i ioco s ∧


i ioco s , now define R = R ∪ (i,s,s )∈J Ri,s,s . We want to show that R defines
a coinductive ioco relation. We do this by showing that R progresses to R.
Let (i, s) ∈ R. We assume that we have seen all of out(i) and that
out(i) ⊆ out(s) (this is taken care of by the test suite and the fairness assumption). Then, because we use P + , we also reach the transitions after i. We need
to show that the input and output successors are again related.
– Let a ∈ LI . Since I is input-enabled we have a transition for a with i after
a = i2 . Suppose there is a transition for a from s: s after a = s2 (if not, then
we’re done). We have to show that (i2 , s2 ) ∈ R.
– Let x ∈ LO . Suppose there is a transition for x: i after x = i2 Then (since
out(i)⊆out(s)) there is a transition for x from s: s after x = s2 . We have to
show that (i2 , s2 ) ∈ R.
In both cases we have a successor (i2 , s2 ) which we have to prove to be in R. Now
since P reaches all states of I, we know that (i2 , s2 ) ∈ R for some s2 . If s2 ≈ s2
then (i2 , s2 ) ∈ R ⊆ R holds trivially, so suppose that s2 ≈ s2 . Then there exists
a distinguishing experiment w ∈ W (s2 ) ∩ W (s2 ) which has been executed in i2 ,
namely in two tests: a test σw for some σ ∈ P + with S after σ = s2 , and a test
σ  w for some σ  ∈ P with S after σ  . Then there are two cases:
– If s2 ♦ s2 then w is a distinguishing tree separating s2 and s2 . Then there is
a sequence ρ taken in w of the test σw, i.e. w after ρ reaches a pass state
of w, and similarly there is a sequence ρ that is taken in w of the test σ  w.
By construction of distinguishing trees, ρ must be an ioco-counterexample for
either s2 or s2 , but because T passed this must be s2 . Similarly, ρ disproves
s2 . One implementation state can implement at most one of {ρ, ρ }. This
contradicts that the two tests passed, so this case cannot happen.
– If s2 ♦ s2 (but s2 ≈ s2 as assumed above), then w is a test suite itself for
s2 ∧ s2 . If w passed in both tests then i2 ioco s2 and i2 ioco s2 , and hence
(i2 , s2 ) ∈ Ri,s2 ,s2 ⊆ R. If w failed in one of the tests σw or σ  w, then i2 does
not conform to both s2 and s2 , and hence w also fails in the other test. So
again, there is a counterexample ρ for s2 and ρ for s2 . One implementation
state can implement at most one of {ρ, ρ }. This contradicts that the two
tests passed, so this case cannot happen.
We have now seen that R progresses to R. It is clear that R progresses to R
too. Then, since each Ri,s,s is an ioco relation, they progress to Ri,s,s ⊆ R. And
so the union, R, progresses to R, meaning that R is a coinductive ioco relation.


Furthermore, we have (i0 , s0 ) ∈ R (because  ∈ P ), concluding the proof.

n-Complete Test Suites for IOCO

103

We remark that if the specification does not contain any compatible states,
that the proof can be simplified a lot. In particular, we do not need n-complete
test suites for merges of states, and we can use the relation R instead of R.

5

Constructing Distinguishing Trees

Lee and Yannakakis proposed an algorithm for constructing adaptive distinguishing sequences for FSMs [5]. With a partition refinement algorithm, a splitting
tree is build, from which the actual distinguishing sequence is extracted.
A splitting tree is a tree of which each node is identified with a subset of the
states of the specification. The set of states of a child node is a (strict) subset of
the states of its parent node. In contrast to splitting trees for FSMs, siblings may
overlap: the tree does not describe a partition refinement. We define leaves(Y )
as the set of leaves of a tree Y . The algorithm will split the leaf nodes, i.e. assign
children to every leaf node. If all leaves are identified with a singleton set of
states, we can distinguish all states of the root node.
Additionally, every non-leaf node is associated with a set of labels from L. We
denote the labels of node D with labels(D). The distinguishing tree that is going
to be constructed from the splitting tree is built up from these labels. As argued
in Sect. 3.2, we require injective distinguishing trees, thus our splitting trees only
contain injective labels, i.e. injective(labels(D), D) for all non-leaf nodes D.
Below we list three conditions that describe when it is possible to split the
states of a leaf D, i.e. by taking some transition, we are able to distinguish some
states from the other states of D. We will see later how a split is done. If the
first condition is true, at least one state is immediately distinguished from all
other states. The other two conditions describe that a leaf D can be split if after
an input or all outputs some node D is reached that already is split, i.e. D is
a non-leaf node. Consequently, a split for condition 1 should be done whenever
possible, and otherwise a split for condition 2 or 3 can be done. Depending on
the implementation one is testing, one may prefer splitting with either condition
2 or 3, when both conditions are true.
We present each condition by first giving an intuitive description in words,
and then a more formal definition. With Π(A) we denote the set of all non-trivial
partitions of a set of states A.
Definition 20. A leaf D of tree Y can be split if one of the following conditions
hold:
1. All outputs are enabled in some but not in all states.
∀x ∈ out(D) : injective(x, D) ∧ ∃d ∈ D : d after x = ∅
2. Some states reach different leaves than other states for all outputs.
∀x ∈ out(D) : injective(x, D) ∧ ∃P ∈ Π(D), ∀d, d ∈ P :
(d = d =⇒ ∀l ∈ leaves(Y ) : l ∩ d after x = ∅ ∨ l ∩ d after x = ∅)

104

P. van den Bos et al.

3. Some states reach different leaves than other states for some input.
∃a ∈ in(D) : injective(a, D) ∧ ∃P ∈ Π(D), ∀d, d ∈ P :
(d = d =⇒ ∀l ∈ leaves(Y ) : l ∩ d after a = ∅ ∨ l ∩ d after a = ∅)
Algorithm 1 shows how to split a single leaf of the splitting tree (we chose
arbitrarily to give condition 2 a preference over condition 3). A splitting tree is
constructed in the following manner. Initially, a splitting tree is a leaf node of
the state set from the specification. Then, the full splitting tree is constructed by
splitting leaf nodes with Algorithm 1 until no further splits can be made. If all
leaves in the resulting splitting tree are singletons, the splitting tree is complete
and a distinguishing tree can be constructed (described in the next section).
Otherwise, no distinguishing tree exists. Note that the order of the splits is left
unspecified.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

Input: A specification S = (Q, LI , LO , T, q0 ) ∈ SA
Input: The current (unfinished) splitting tree Y
Input: A leaf node D from Y
if Condition 1 holds for D then
P := {D after x | x ∈ out(D)};
labels(D) := out(D);
Add the partition blocks of P as children of D;
else if Condition 2 holds for D then
labels(D) := out(D);
foreach x ∈ out(D) do
P := the finest partition for Condition 2 with D and x;
Add the partition blocks of P as children of D;
end
else if Condition 3 holds for D with input a then
P := the finest partition for Condition 3 with D and a;
labels(D) := {a};
Add the partition blocks of P as children of D;
return Y ;

Algorithm 1. Algorithm for splitting a leaf node of a splitting tree.

Example 21. Let us apply Algorithm 1 on the suspension automaton in Fig. 5a.
Figure 5b shows the resulting splitting tree. We initialize the root node to
{1, 2, 3, 4, 5}. Condition 1 applies, since states 1 and 5 only have output y
enabled, while states 2, 3 and 4 only have outputs x and z enabled. Thus, we
add leaves {1, 5} and {2, 3, 4}.
We can split {1, 5} by taking an output transition for y according to condition
2, as 1 after y = 4 ∈ {2, 3, 4}, while 5 after y = 1 ∈ {1, 5}, i.e. 1 and 5 reach
different leaves. Condition 2 also applies for {2, 3, 4}. We have that {2, 3} after
x = {2, 4} ⊆ {2, 3, 4} while 4 after x = 5 ∈ {5}. Hence we obtain children {4}

n-Complete Test Suites for IOCO

105

{1,2,3,4,5}: x, y, z
y

5

1

a

2

a

y

x

z

4

z
z

x

x

{2,3,4}: x, z

{1,5}: y
a
{1}

3

(a) Example specification with
mutually incompatible states.

{5}

{4} {2,3}: a {2} {3,4}: a
{2} {3}

{3} {4}

(b) Splitting tree of Figure 5a.

Fig. 5. Specification and its splitting tree.

and {2, 3} for output x. For z we have that 2 after z = 1 ∈ {1} while {3, 4}
after z = {3, 4} ⊆ {2, 3, 4}, so we obtain children {2} and {3, 4} for z.
We can split {2,3} by taking input transition a according to condition 3,
since 2 after a = 4 and 3 after a = 2, and no leaf of the splitting tree contains
both state 2 and state 4. Note that we could also have split on output transitions
x and z. Node {3, 4} cannot be split for output transition z, since {3, 4} after
z = {3, 4} which is a leaf, and hence condition 2 does not hold. However node
{3, 4} can be split for input transition a, as 3 after a = 2 and 4 after a = 4.
Now all leaves are singleton, so we can distinguish all states with this tree.
A distinguishing tree Y ∈ DT (LI , LO , D) for D can be constructed from a
splitting tree with singleton leaf nodes. This follows the structure in Definition 8,
and we only need to choose whether to provide an input, or whether to observe
outputs. We look at the lowest node D in the split tree such that D ⊆ D .

x

{1,2,3,4,5}
y

{2,4,5}
x y z

z
{1,3,4}
x y

{1,4}
x y
z

{1} {1,3} {5} {4} {3} {2,5}
{4,5}
y
x
z
x y
z
x y
z
{5} {1} {3} {2} {4} {4}

z

{4}

{3,4}
a

x

y

z

{4} {1} {1} {2,4} reset reset reset
y
x
z
{4,5}
x y
z
{5}

{1} {3}

∅

{1,3}
x y
z
{2}

{4} {4}

Fig. 6. Distinguishing tree of Fig. 5a. The states are named by the sets of states which
they distinguish. Singleton and empty sets are the pass states. Self-loops in verdict
states have been omitted, for brevity.

106

P. van den Bos et al.

If labels(D ) has an input, then Y has a transition for this input, and a transition
to reset for all outputs. If labels(D ) contains outputs, then Y has a transition for
all outputs. In this manner, we recursively construct states of the distinguishing
tree until |D| ≤ 1, in which case we have reached a pass state. Figure 6 shows
the distinguishing tree obtained from the splitting tree in Fig. 5b.

6

Conclusions

We firmly embedded theory on n-complete test suites into ioco theory, without making any restricting assumptions. We have identified several problems
where classical FSM techniques fail for suspension automata, in particular for
compatible states. An extension of the concept of distinguishing states has been
introduced such that compatible states can be handled, by testing the merge
of such states. This requires that the merge itself does not contain compatible
states. Furthermore, upper bounds for several parts of a test suite have been
given, such as reaching all states in the implementation.
These upper bounds are exponential in the number of states, and may limit
practical applicability. Further investigation is needed to efficiently tackle these
parts of the test suite. Alternatively, looser notions for completeness may circumvent these problems. Furthermore, experiments are needed to compare our
testing method and random testing as in [11] quantitatively, in terms of efficiency
of computation and execution time, and the ability to find bugs, preferably on
a real world case study.