The Stream X-machine (SXM) is a model of computation introduced by Gilbert Laycock in his 1993 PhD thesis, The Theory and Practice of Specification Based Software Testing.[1] Based on Samuel Eilenberg's X-machine, an extended finite-state machine for processing data of the type X,[2] the Stream X-Machine is a kind of X-machine for processing a memory data type Mem with associated input and output streams In* and Out*, that is, where X = Out* × Mem × In*. The transitions of a Stream X-Machine are labelled by functions of the form φ: Mem × In → Out × Mem, that is, which compute an output value and update the memory, from the current memory and an input value.
Although the general X-machine had been identified in the 1980s as a potentially useful formal model for specifying software systems,[3] it was not until the emergence of the Stream X-Machine that this idea could be fully exploited. Florentin Ipate and Mike Holcombe went on to develop a theory of complete functional testing,[4] in which complex software systems with hundreds of thousands of states and millions of transitions could be decomposed into separate SXMs that could be tested exhaustively, with a guaranteed proof of correct integration.[5]
Because of the intuitive interpretation of Stream X-Machines as "processing agents with inputs and outputs", they have attracted increasing interest, because of their utility in modelling real-world phenomena. The SXM model has important applications in fields as diverse as computational biology, software testing and agent-based computational economics.
A Stream X-Machine (SXM) is an extended finite-state machine with auxiliary memory, inputs and outputs. It is a variant of the general X-machine, in which the fundamental data type X = Out* × Mem × In*, that is, a tuple consisting of an output stream, the memory and an input stream. A SXM separates the control flow of a system from the processing carried out by the system. The control is modelled by a finite-state machine (known as the associated automaton) whose transitions are labelled with processing functions chosen from a set Φ (known as the type of the machine), which act upon the fundamental data type.
Each processing function in Φ is a partial function, and can be considered to have the type φ: Mem × In → Out × Mem, where Mem is the memory type, and In and Out are respectively the input and output types. In any given state, a transition is enabled if the domain of the associated function φi includes the next input value and the current memory state. If (at most) one transition is enabled in a given state, the machine is deterministic. Crossing a transition is equivalent to applying the associated function φi, which consumes one input, possibly modifies the memory and produces one output. Each recognised path through the machine therefore generates a list φ1 ... φn of functions, and the SXM composes these functions together to generate a relation on the fundamental data type |φ1 ... φn|: X → X.
The Stream X-Machine is a variant of X-machine in which the fundamental data type X = Out* × Mem × In*. In the original X-machine, the φi are general relations on X. In the Stream X-Machine, these are usually restricted to functions; however the SXM is still only deterministic if (at most) one transition is enabled in each state.
A general X-machine handles input and output using a prior encoding function α: Y → X for input, and a posterior decoding function β: X → Z for output, where Y and Z are respectively the input and output types. In a Stream X-Machine, these types are streams:
Y = In* Z = Out*
and the encoding and decoding functions are defined as:
α(ins) = (<>, mem0, ins) β(outs, memn, <>) = outs
where ins: In*, outs: Out* and memi: Mem. In other words, the machine is initialized with the whole of the input stream; and the decoded result is the whole of the output stream, provided the input stream is eventually consumed (otherwise the result is undefined).
Each processing function in a SXM is given the abbreviated type φSXM: Mem × In → Out × Mem. This can be mapped onto a general X-machine relation of the type φ: X → X if we treat this as computing:
φ(outs, memi, in :: ins) = (outs :: out, memi+1, ins)
where :: denotes concatenation of an element and a sequence. In other words, the relation extracts the head of the input stream, modifies memory and appends a value to the tail of the output stream.
Because of the above equivalence, attention may focus on the way a Stream X-Machine processes inputs into outputs, using an auxiliary memory. Given an initial memory state mem0 and an input stream ins, the machine executes in a step-wise fashion, consuming one input at a time, and generating one output at a time. Provided that (at least) one recognised path path = φ1 ... φn exists leading to a state in which the input has been consumed, the machine yields a final memory state memn and an output stream outs. In general, we can think of this as the relation computed by all recognised paths: | path | : In* → Out*. This is often called the behaviour of the Stream X-Machine.
The behaviour is deterministic, if (at most) one transition is enabled in each state. This property, and the ability to control how the machine behaves in a step-wise fashion in response to inputs and memory, makes it an ideal model for the specification of software systems. If the specification and implementation are both assumed to be Stream X-Machines, then the implementation may be tested for conformance to the specification machine, by observing the inputs and outputs at each step. Laycock first highlighted the utility of single-step processing with observations for testing purposes.
Holcombe and Ipate developed this into a practical theory of software testing which was fully compositional, scaling up to very large systems.[6] A proof of correct integration guarantees that testing each component and each integration layer separately corresponds to testing the whole system. This divide-and-conquer approach makes exhaustive testing feasible for large systems.
The testing method is described in a separate article on the Stream X-Machine testing methodology.