Stream X-Machine

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. Based on Samuel Eilenberg's 1974 X-machine model, a general machine for processing data of the type X, the Stream X-Machine is an extended finite state 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, 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 software testing,, 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.

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.

The Stream X-Machine

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 φ: In × Mem → Mem × Out, 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 φ₁ ... φ_n of functions, and the SXM composes these functions together to generate a relation on the fundamental data type |φ₁ ... φ_n|: X → X.

Relationship to X-machines

The Stream X-Machine is a variant of X-machine in which the fundamental data type X = Out* × Mem × In*. In a general 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 mem_i: 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: In × Mem → Mem × Out. 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.

Running an SXM

In order to run an SXM, the user should specify the initial memory state, m₀, and supply the input stream ins upon which the machine is to operate. The output string is initially assumed to be empty. An output string outs is deemed to be computed by the machine provided there is some recognised path p and some memory state m_p such that (outs, m_p, []) is related to the initial configuration ([], m₀, ins) by |p|.

Seen in this way - provided the initial memory state m₀ has been specified - each SXM M computes a relation |M| : In^* → Out^*. This relation is often called the behaviour of the SXM.

Applications

See the following articles:

• The SXM Testing (SXMT) Methodology, a complete functional testing technique. Using this methodology, it is possible to identify a finite set of tests that exhaustively determine whether an implementation matches its specification. The technique overcomes formal undecidability limitations by insisting that users apply carefully specified design for test principles during implementation.

• Communicating Stream X-Machines (CSXMs), a concurrent version of the SXM model, with applications in fields ranging from social insects to economics.

See Also

• X-machines, a general description of the X-machine model, including a simple example.

External Links

• The MOTIVE project, using SXM techniques to generate test sets for object-oriented software.
• The EURACE project, an application of CSXM techniques to agent-based computational economics.
• x-machines.net, a site describing the background to X-machine research.
• Mike (Prof. W.M.L.) Holcombe's web page at Sheffield University.