The (Stream) X-Machine Testing Methodology is a complete functional testing approach to software- and hardware testing that exploits the scalability of the Stream X-Machine model of computation. Using this methodology, it is likely to identify a finite test-set that exhaustively determines whether the tested system's implementation matches its specification. This goal is achieved by a divide-and-conquer approach, in which the design is decomposed by refinement into a collection of Stream X-Machines, which are implemented as separate modules, then tested bottom-up. At each integration stage, the testing method guarantees that the tested components are correctly integrated.
The methodology overcomes formal undecidability limitations by requiring that certain design for test principles are followed during specification and implementation. The resulting scalability means that practical software and hardware systems consisting of hundreds of thousands of states and millions of transitions have been tested successfully.
Motivation
Much software testing is merely hopeful, seeking to exercise the software system in various ways to see whether any faults can be detected. Testing may indeed reveal some faults, but can never guarantee that the system is correct, once testing is over. Functional testing methods seek to improve on this situation, by developing a formal specification describing the intended behaviour of the system, against which the implementation is later tested (a kind of conformance testing). The specification can be validated against the user-requirements and later proven to be consistent and complete by mathematical reasoning (eliminating any logical design flaws). Complete functional testing methods exploit the specification systematically, generating test-sets which exercise the implemented software system exhaustively, to determine whether it conforms to the specification. In particular: Full positive testing: confirms that all desired behaviour is present in the system; Full negative testing: confirms that no unintended behaviour is present in the system. This level of testing can be difficult to achieve, since software systems are extremely complex, with hundreds of thousands of states and millions of transitions. What is needed is a way of breaking down the specification and testing problem into parts which can be addressed separately.
Scalable, Abstract Specifications
Mike Holcombe first proposed using Samuel Eilenberg's theoretical X-machine model as the basis for software specification in the late 1980s. This is because the model cleanly separates the control flow of a system from the processing carried out by the system. At a given level of abstraction, the system can be viewed as a simple finite-state machine consisting of a few states and transitions. The more complex processing is delegated to the processing functions on the transitions, which modify the underlying fundamental data type X. Later, each processing function may be separately exposed and characterized by another X-machine, modelling the behaviour of that system operation.
This supports a divide-and-conquer approach, in which the overall system architecture is specified first, then each major system operation is specified next, followed by subroutines, and so forth. At each step, the level of complexity is manageable, because of the independence of each layer. In particular, it is easy for software engineers to validate the simple finite-state machines against user requirements.
Incrementally Testable Specifications
Gilbert Laycock first proposed a particular kind of X-machine, the Stream X-Machine, as the basis for the testing method. The advantage of this variant was the way in which testing could be controlled. In a Stream X-Machine, the fundamental data type has a particular form: X = Out* × Mem × In*, where In* is an input stream, Out* is an output stream, and Mem is the internal memory. The transitions of a Stream X-Machine are labelled with processing functions of the form φ: Mem × In → Out × Mem, that is, they consume one input from the input stream, possibly modify memory, and produce one output on the output stream (see the associated article for more details).