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" [Lay93]. Based on Eilenberg's 1974 X-machine model [Eil74], the SXM has been investigated in detail by Mike Holcombe (Laycock's PhD supervisor, and a key proponent of the X-machine model) and his associates. The SXM model has important applications in fields as diverse as software testing and agent-based computational economics.

The SXM model

An SXM is a "machine for converting inputs into outputs using an auxiliary memory". Suppose that Mem is some datatype, called the memory type, and that Φ is a set of relations φ: In × Mem → Mem × Out, where In and Out are the relevant input and output alphabets. An SXM is a finite state machine whose arrows are labelled by relations in Φ. Each recognised path through the machine generates a list φ₁ ... φ_n of relations, and the SXM chains these relations together to generate a relation |φ₁ ... φ_n|: X → X, where X = Out^* × Mem × In^*.

We will use standard Haskell list notation to represent strings, so that the string hello is written [h, e, l, l, o], and the empty string is written []. The notation x:xs means "add the symbol x to the front of the string xs," and the notation xs++ys means "append the string ys to the end of the string xs." The empty list [] represents the empty string.

For each φ, the relation |φ| is defined by

$(outs+\!+[out],\ mem',\ ins)\in |\phi |(outs,\ mem,\ in:ins)\quad \Leftrightarrow \quad (mem',\ out)\in \phi (in,\ mem)$

and the path relation |φ₁ ... φ_n| is formed by composition, viz. |φ₁ ... φ_n| = |φ₁| o ... o |φ_n|.

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 in the set |p|([], m₀, ins).

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

Applications

See the following articles:

• X-machines, including a simple example.

• 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.

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.

References

1. Samuel Eilenberg (1974) Automata, Languages and Machines, Vol. A. Academic Press, London.
2. Gilbert Laycock (1993) The Theory and Practice of Specification Based Software Testing. PhD Thesis, University of Sheffield, Dept of Computer Science. Abstract