X-Machine Testing

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.

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. 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. 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). The input, memory and output types for the top-level machine are now formalised. Suppose that the memory type of the simple word processor is the type Document defined above. This treats a document as a text string, with two positions marking a possible selection and a flag to indicate modification since the last save-command. A more complex word processor might support undoable editing, with a sequence of document states: Document ::= (Text × Selection)*, which are collapsed to one document every time a save-command is performed. Suppose that the input type for the machine is: In ::= Command × Character × Position. This recognises that every interaction could be a simple character insertion, a menu command or a cursor placement. Any given interaction is a 3-tuple, but some places may be empty. For example, (Insert, 'a', ε) would represent typing the character 'a'; while (Position, ε, 32) would mean placing the cursor between characters 32 and 33; and (Select, ε, 32) would mean selecting the text between the current cursor position and the place between characters 32 and 33. The output type for the machine is designed so that it is possible to determine from the output which processing function was executed, in response to a given input. This relates to the property of output distinguishability, described below. To reach each state expected in Spec, the tester constructs the state cover, C, the smallest set of test sequences that reaches every state. This can be constructed by automatic breadth-first exploration of Spec. The test-set which validates all the states of a minimal Imp is then: C \otimes W , where \otimes denotes the concatenated product of the two sets. For example, if C = , } and W = , }, then C \otimes W = \{\langle ac \rangle, \langle ad \rangle, \langle bc \rangle, \langle bd \rangle \} . The above test-set determines whether a minimal Imp has the same states as Spec. To determine whether a minimal Imp also has the same transition behaviour as Spec, the tester constructs the transition cover, K. This is the smallest set of test sequences that reaches every state and then attempts every possible transition once, from that state. Now, the input alphabet consists of (the labels of) every function φ in Φ. Let us construct a set of length-1 test sequences, consisting of single functions chosen from Φ, and call this Φ 1 . The transition cover is defined as K :=C \cup C \otimes \Phi_{1} . This will attempt every possible transition from every state. For those which succeed, we must validate the destination states. So, the smallest test-set T 1 which completely validates the behaviour of a minimal Imp is given by: T_{1} ::=C \otimes W \cup C \otimes \Phi_{1} \otimes W . This formula can be rearranged as: T_{1} ::=C \otimes\left(\Phi_{0} \cup \Phi_{1}\right) \otimes W , where Φ 0 is the set containing the empty sequence . If Imp has more states than Spec, the above test-set may not be sufficient to guarantee the conformant behaviour of replicated states in Imp. So, sets of longer test sequences are chosen, consisting of all pairs of functions Φ 2 , all triples of functions Φ 3 up to some limit Φ k , when the tester is satisfied that Imp cannot contain chains of duplicated states longer than k-1. The final test formula is given by: T_{\mathrm{k}} ::=C \otimes\left(\Phi_{0} \cup \Phi_{1} \ldots \cup \Phi_{\mathrm{k}}\right) \otimes W . This test-set completely validates the behaviour of a non-minimal Imp in which chains of duplicated states are expected to be no longer than k-1. For most practical purposes, testing up to k=2, or k=3 is quite exhaustive, revealing all state-related faults in really poor implementations.

Text derived from https://en.wikipedia.org/w/index.php?oldid=1322002470 under CC BY-SA 4.0; modifications have been made.