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). The benefits for testing are that software systems designed in this way are observable at each step. For each input, the machine takes one step, producing an output, such that input/output pairs may be matched exactly. This contrasts with other approaches in which the system runs to completion (taking multiple steps) before any observation is made. Furthermore, layered Stream X-Machines offer a convenient abstraction. At each level, the tester may forget about the details of the processing functions and consider the (sub-)system just as a simple finite-state machine. Powerful methods exist for testing systems that conform to finite-state specifications, such as Chow's W-method.
Specification Method When following the (Stream) X-Machine methodology, the first stage is to identify the various types of data to be processed. For example, a word processor will use basic types Character (keyboard input), Position (mouse cursor position) and Command (mouse or menu command). There may be other constructed types, such as Text ::= Character* (a sequence of characters), Selection ::= Position × Position (the start and end of the selection) and Document ::= Text × Selection × Boolean (the text, a possible selection, and a flag to signal if the document has been modified).
… excerpt ends here. Continue reading the full article.
