X-machine

The X-machine (XM) is a theoretical model of computation introduced by Samuel Eilenberg in 1974.

The X in "X-machine" represents the fundamental data type on which the machine operates; for example, a machine that operates on databases (objects of type database) would be a database-machine. The X-machine model is structurally the same as the finite-state machine, except that the symbols used to label the machine's transitions denote relations of type X→X. Crossing a transition is equivalent to applying the relation that labels it (computing a set of changes to the data type X), and traversing a path in the machine corresponds to applying all the associated relations, one after the other.

Original theory

Eilenberg's original X-machine was a completely general theoretical model of computation (subsuming the Turing machine, for example), which admitted deterministic, non-deterministic and non-terminating computations. His seminal work who noticed that the model was ideal for software formal specification purposes, because it cleanly separates control flow from processing. Provided one works at a sufficiently abstract level, the control flows in a computation can usually be represented as a finite-state machine, so to complete the X-machine specification all that remains is to specify the processing associated with each of the machine's transitions. The structural simplicity of the model makes it extremely flexible; other early illustrations of the idea included Holcombe's specification of human-computer interfaces,

his modelling of processes in cell biochemistry,

and Stannett's modelling of decision-making in military command systems.

1990s

X-machines have received renewed attention since the mid-1990s, when Gilbert Laycock's deterministic Stream X-Machine was found to serve as the basis for specifying large software systems that are completely testable. Another variant,

the Communicating Stream X-Machine offers a useful testable model for biological processes

and future swarm-based satellite systems.

2000s

X-machines have been applied to lexical semantics by András Kornai, who models word meaning by `pointed' machines that have one member of the base set X distinguished. Application to other branches of linguistics, in particular to a contemporary reformulation of Pāṇini were pioneered by Gerard Huet and his co-workers

Major variants

The X-machine is rarely encountered in its original form, but underpins several subsequent models of computation. The most influential model on theories of software testing has been the Stream X-Machine. NASA has recently discussed using a combination of Communicating Stream X-Machines and the process calculus WSCSS in the design and testing of swarm satellite systems.

it is consequently related to work in hypercomputation theory.

Stream X-Machine (SXM)

The most commonly encountered X-machine variant is Gilbert Laycock's 1993 Stream X-Machine (SXM) model, The Stream X-Machine differs from Eilenberg's original model, in that the fundamental data type X is of the form Out* × Mem × In*, where In* is an input sequence, Out* is an output sequence, and Mem is the (rest of the) memory.

The advantage of this model is that it allows a system to be driven, one step at a time, through its states and transitions, while observing the outputs at each step. These are witness values, that guarantee that particular functions were executed on each step. As a result, complex software systems may be decomposed into a hierarchy of Stream X-Machines, designed in a top-down way and tested in a bottom-up way. This divide-and-conquer approach to design and testing is backed by Florentin Ipate's proof of correct integration, which proves how testing the layered machines independently is equivalent to testing the composed system.

Communicating X-Machine (CXM)

The earliest proposal for connecting several X-machines in parallel is Judith Barnard's 1995 Communicating X-machine (CXM or COMX) model,

in which machines are connected via named communication channels (known as ports); this model exists in both discrete- and real-timed variants. Earlier versions of this work were not fully formal and did not show full input/output relations.

A similar Communicating X-Machine approach using buffered

channels was developed by Petros Kefalas. The focus of this work was on expressiveness in the composition of components. The ability to reassign channels meant that some of the testing theorems from Stream X-Machines did not carry over.

These variants are discussed in more detail on a separate page.

Communicating Stream X-Machine (CSXM)

The first fully formal model of concurrent X-machine composition was proposed in 1999 by Cristina Vertan and Horia Georgescu, based on earlier work on communicating automatata by Philip Bird and Anthony Cowling. In Vertan's model, the machines communicate indirectly, via a shared communication matrix (essentially an array of pigeonholes), rather than directly via shared channels.

Bălănescu, Cowling, Georgescu, Vertan and others have studied the formal properties of this CSXM model in some detail. Full input/output relations can be shown. The communication matrix establishes a protocol for synchronous communication. The advantage of this is that it decouples each machine's processing from their communication, allowing the separate testing of each behaviour. This compositional model was proven equivalent to a standard Stream X-Machine, so leveraging the earlier testing theory developed by Holcombe and Ipate.

This X-machine variant is discussed in more detail on a separate page.

Object X-Machine (OXM)

Kirill Bogdanov and Anthony Simons developed several variants of the X-machine to model the behaviour of objects in object-oriented systems. This model differs from the Stream X-Machine approach, in that the monolithic data type X is distributed over, and encapsulated by, several objects, which are serially composed; and systems are driven by method invocations and returns, rather than by inputs and outputs.

Further work in this area concerned adapting the formal testing theory in the context of inheritance, which partitions the state-space of the superclass in extended subclass objects.

A "CCS-augmented X-machine" (CCSXM) model was later developed by Simons and Stannett in 2002 to support complete behavioural testing of object-oriented systems, in the presence of asynchronous communication This is expected to bear some similarity with NASA's recent proposal; but no definitive comparison of the two models has as yet been conducted.

External links

http://www.dcs.shef.ac.uk/~ajc/csxms/index.html - Tony Cowling's Communicating SXM Systems pages
http://x-machines.com - Mike Stannett's Theory of X-Machines site