Model-Based Testing with Explicit State Machines

A pure function is tested by input and output. A stateful object is not, because its behaviour depends on the sequence of calls that preceded it, and the interesting defects appear only for particular sequences: a cancel after a partial refund, a retry after a timeout that actually succeeded, a close followed by a read that the interface still permits.

Enumerating sequences by hand is hopeless, since five operations have 5^n sequences of length n, and writing a test per scenario produces a suite that covers the sequences someone imagined. Model-based testing replaces the enumeration with a generator driven by a specification of the states and the legal transitions, and replaces the hand-written expectations with a model that the implementation is compared against after every step.

The two artefacts: model and generator

The model is a second implementation of the system’s semantics, written for clarity rather than performance, usually as an explicit state machine: a set of states, a set of operations, and for each operation a precondition and a transition function. The generator walks the machine, choosing at each step among the operations whose preconditions hold in the current state, and produces a sequence of calls.

Both artefacts are small. A model for a bounded queue has states tracking the elements, an operation that enqueues with the precondition “not full”, an operation that dequeues with the precondition “not empty”. A model for an account has a balance, a status, and operations for deposit, withdraw, freeze, and close, each with its legality conditions. The model’s job is to be obviously correct, which means it should be a fraction of the size of the implementation and should use the simplest possible representation: a list where the implementation uses a ring buffer, an integer where the implementation uses a decimal type.

That size difference is the whole argument. Two implementations of the same semantics that are independent in structure will disagree where either is wrong, and the model, being trivially readable, is the one a reviewer can check. This is differential testing with the reference implementation written for the purpose, and its strength depends on the model not sharing the implementation’s mistakes. A model derived by reading the implementation inherits them and tests nothing.

Executing a sequence and checking after each step

The runner applies operations in order. After each operation it compares the implementation’s observable state to the model’s: the return value, and whatever state the interface exposes — a length, a status, a list of pending items.

Comparing after every step rather than at the end is what makes failures localizable. A sequence of forty operations that ends in a wrong state gives one failure with no indication of which step introduced it; a comparison per step gives the first index at which the two diverged, and that index plus the preceding trace is a complete reproduction.

# The model: a list and a flag. Deliberately the dumbest correct implementation.
class QueueModel:
    def __init__(self, capacity):
        self.items = []
        self.capacity = capacity

    def can_enqueue(self):
        return len(self.items) < self.capacity

    def enqueue(self, x):
        self.items.append(x)

    def can_dequeue(self):
        return len(self.items) > 0

    def dequeue(self):
        return self.items.pop(0)

The runner keeps one model and one real instance, replays the same operation on both, and compares after each. The generated sequence is the test; the trace is the artefact a failure reports.

A failing trace is worth more than a failing input because it is a program. Shrinking applies here too, and applies better: a sequence of forty operations usually reduces to three or four, because most steps are irrelevant to the divergence. The reduction is over the same lazy choice tree described in property-based testing and shrinking, with the additional constraint that removing a step must leave a sequence whose every remaining precondition still holds, which the generator’s structure guarantees if the shrink candidates are generated rather than spliced.

Preconditions, and the sequences that must not be generated

The generator’s most important job is deciding what not to produce. An operation whose precondition is false is not a case to test unless the specification says the implementation must reject it, and generating it produces failures that are about the harness’s assumptions.

Two categories need separate handling. Illegal but reachable operations, such as a dequeue on an empty queue, are worth generating deliberately if the interface promises a specific error, and their expected behaviour belongs in the model as a transition to an error state. Illegal and undefined operations must be excluded from the generator entirely, because the implementation is free to do anything and the model has nothing to compare against.

The generator also needs a fairness policy. Choosing uniformly among legal operations produces sequences dominated by the operations that are almost always legal, and starves the ones with narrow preconditions — the freeze that requires an active account, the close that requires a zero balance. Weighting the selection toward rarely-legal operations, or tracking which operations have been exercised and preferring the unexercised, is what gets the narrow transitions covered. This is the state-machine version of the rare-precondition problem, and it has the same fix: make the generator produce the interesting case rather than filtering for it.

Invariants that hold in every state

Beyond per-step comparison, a model-based run can check invariants: predicates that must hold in every reachable state, independent of the operation that produced it. A queue’s length never exceeds its capacity. An account’s balance and its transaction log agree. A frozen account has no pending withdrawals.

Invariants catch a class of defect the transition comparison misses: a wrong state that the model also produces because the model’s transition is wrong, but that violates a property the model’s author stated separately. They also survive model incompleteness, since an invariant can be asserted even when the model does not implement the operation that would disturb it.

The cost is that an invariant is another claim to maintain, and a badly chosen one produces false failures. Invariants that restate the model’s transition functions add nothing; the useful ones are those stated independently, in terms of quantities the model computes differently.

Where the model diverges from reality

Model-based testing has three recurring failure modes, and each produces a suite that looks thorough and checks little.

The model is the implementation, rewritten. If the model was produced by transliterating the implementation, agreement between them is guaranteed by construction and no defect is detectable. The symptom is a model whose structure mirrors the implementation’s: same data structures, same helper methods, same order of checks.

The observable surface is too narrow. A model can only compare what the implementation exposes. A cache whose hit rate is not observable, a connection pool whose idle count is private, a scheduler whose queue depth is internal: the model compares the return values and misses the state that the defects live in. Widening the observable surface, through an accessor for internal state used only by tests or a counter exposed in a diagnostics endpoint, is often necessary, and it is a design change rather than a testing one.

Time and concurrency are absent. A model of a system with timeouts is a model with a clock, and the model’s clock must advance deterministically while the implementation’s does not. A model of a concurrent system has no single sequence to compare against. Both need a virtual clock injected into the implementation under test, and a scheduler the harness controls, the controls described in nondeterministic tests and flaky suites rather than an extension of the sequential runner.

The leverage and the price

The leverage is coverage of sequence space. A hand-written suite for a stateful object covers the scenarios someone wrote down, typically the happy path, one error per operation, and two combinations. A model-based run of a few hundred sequences covers short and long traces, interleavings of every pair of operations, and the rare transitions that the weighting surfaced. The defects found tend to be ordering defects: an operation that leaves state inconsistent for the next one, a cleanup that runs too early, an error path that forgets to restore a flag.

The price is threefold. The model must be written and must be right, which is a real cost for a system whose semantics are complex. The harness must be built: a way to reset the system to a known state between sequences, a way to observe internal state, a way to replay a trace. And the failures require interpretation, because a divergence means the model and the implementation disagree and the model is sometimes the one that is wrong, which is a defect in the specification, and worth knowing about, but not the defect the run was looking for.

The economics improve sharply when the model already exists for another purpose: a protocol state machine from the specification, a statechart from the design, a reference implementation written for a migration. In that case the harness is the only new cost, and the sequences come free.