Conformance Testing from a Specification: Distinguishing Sequences

A test suite derived from a specification has a property that hand-written tests lack: a stated relationship between what was tested and what the specification allows. The relationship is not that the suite proves correctness, because no finite suite does. It is that the suite is guaranteed to detect any implementation that differs from the specification within a bounded number of extra states, and the bound is part of the claim.

The construction comes from finite-state machine testing and rests on one primitive: a way to determine which state an implementation is in by observing its responses. Given that primitive, a suite can be built that exercises every state and every transition, and the resulting claim is stronger than coverage in the usual sense, because it can distinguish an implementation with a wrong transition from one with a missing state.

Distinguishing a state requires a sequence, not a probe

A state is not directly observable. What is observable is the output produced by an input. Two states are distinguishable when some input sequence produces different output sequences from them; if no such sequence exists, the states are equivalent and no test can tell them apart.

For a specification with $n$ states and input alphabet of size $m$, the equivalence classes of states under this relation are computable in $O(n^2 m)$ by partition refinement: start with all states in one block, and repeatedly split blocks by the outputs produced on each input. The result is the minimal machine equivalent to the specification. That minimisation matters for testing, because a specification whose states are not pairwise distinguishable cannot be tested for state identity at all, and the unreachable states removed by the same procedure are states no test needs to visit.

A distinguishing sequence for a state is an input sequence whose output from that state differs from its output from every other state. Not every machine has one — some machines have only adaptive distinguishing sequences, where the next input depends on the output so far — and some have neither, in which case state identification requires a set of sequences rather than a single one. This is the practical limit of the method: a specification with a pair of equivalent states can only be tested up to that equivalence, and no test design repairs it.

The W-method and what the bound means

Chow’s method builds a suite from three components. A transition cover $P$ reaches every transition from the initial state, exercising each transition at least once. A state cover $Q$ reaches every state. A characterising set $W$ is a set of input sequences that distinguishes every pair of states — for each state, its response to the sequences in $W$ identifies it uniquely among the specification’s states.

The suite is then the concatenation of each prefix in $P \cup Q$ with each sequence in $W$. If the implementation has at most $n + k$ states, where $n$ is the specification’s state count, the suite extended to length $k$ extra states detects every implementation that is not equivalent to the specification. The extension is the part that makes the claim non-trivial: without it, a faulty implementation with one extra state that behaves correctly on all short sequences passes.

The size follows. With $|P|$ roughly $n \cdot m$, $|Q| = n$, and $|W|$ at most $n$, the suite has on the order of $n^2 m$ sequences, each of length up to $n + k$. For a specification with thirty states and a four-symbol alphabet, that is already thousands of test cases, and the count grows quadratically. This is the honest cost of a completeness claim, and it is why the method is applied to protocol cores and state-heavy subsystems rather than to whole applications.

from itertools import product

def extensions(alphabet, k):
    # All input sequences of length up to k, giving extra states room
    # to reveal a difference.
    for n in range(k + 1):
        for seq in product(alphabet, repeat=n):
            yield list(seq)

def w_method(spec, k):
    cover = transition_cover(spec) | state_cover(spec)
    w = characterising_set(spec)          # distinguishes all state pairs
    suite = []
    for prefix in cover:
        for seq in w:
            for extra in extensions(spec.alphabet, k):
                suite.append(prefix + seq + extra)
    return suite

The nested loop is the whole construction, and each level answers a different question: the prefix reaches the transition, the characterising sequence identifies the state reached, and the extension gives a faulty implementation room to reveal itself.

Assumptions the guarantee rests on

The completeness claim is conditional on four assumptions, and each is a way for a suite to look rigorous and be wrong.

The first is a bound on implementation states. The method’s guarantee is relative to $n + k$; an implementation with more states than that can differ from the specification and still pass. Choosing $k$ is a judgement about how much extra state a plausible implementation might add — a retry counter, a cache flag, a mode not in the specification — and it is a specification parameter, not a tool setting.

The second is determinism and input-enabledness. The construction assumes that from every state, every input produces exactly one output and one successor. A specification with unspecified inputs, or with inputs that can be refused, needs a different formulation: the suite has to allow the implementation to refuse, and the refusal itself becomes an observable that the characterising set can use. Specifications written as transition tables with unmarked cells violate this assumption directly, because an unmarked cell means the behaviour on that input is not specified and cannot be tested against.

The third is a reliable reset. Each test case starts from the initial state, so the harness must be able to return the implementation to it. A reset that is itself a message the implementation can observe changes the state, and a reset that restarts a process discards state the test was about to inspect. Specifications that define a reset input make this explicit; specifications that leave it to the harness make the suite’s guarantee depend on infrastructure outside the model.

The fourth is observability of outputs. The method assumes every transition produces an output that the harness can see. Internal transitions with no observable effect cannot be tested individually — they can only be tested through their consequences, which means the characterising set has to reach a state where the consequence is visible. A specification with many silent transitions yields a suite that is much weaker than its transition count suggests.

From state count to real implementations

The gap between a finite-state model and a running system is where the method’s assumptions strain. A real implementation has data: a queue whose contents are not part of the abstract state, a counter with a range, a timestamp. The abstraction has to treat these as either irrelevant — in which case the tests cannot detect bugs in them — or as part of the state, in which case the state space is no longer finite.

The standard compromise is to test the control structure exhaustively and the data behaviour by sampling, and to state the split. The claim then becomes: the suite is complete for the control-flow model up to $k$ extra states, and it covers a selected set of data partitions. That is a weaker claim than the pure method’s, and it is reviewable, which the alternative is not.

There is a second gap in the direction of time. The method tests sequences of inputs, and a sequence that ends in the right state with the right output may have taken an unbounded time to get there. Timing properties are outside the alphabet unless the model includes a clock, and including a clock turns the finite-state model into a timed automaton whose state space is infinite in general. Liveness and fairness properties are outside the method entirely, since no finite test can distinguish eventual delivery from delivery within a bound.

The method also assumes the model’s transitions are decided by state alone. Where an outcome depends on a combination of input facts rather than on history, the transition relation is a decision table in disguise, and the table’s coverage check answers the same question the characterising set answers: whether every permitted combination has a defined response. Tables are the cheaper notation for that class, since a complete table gives the test suite its cases without a state cover.

What the method does deliver is worth stating plainly, because it is more than testing usually claims: a suite whose relationship to the specification is a theorem, whose cost is computable in advance from the specification’s size, and whose failures are attributable to a specific transition rather than to an anonymous assertion. That attribution is the practical payoff. A failing characterising sequence names the state the implementation actually reached, which is usually enough to identify the wrong transition without debugging. The same attribution logic appears in model checking, where the counterexample names the path, and in both cases the value comes from the specification having a structure that the tool can follow.