Theory of X-Machines
HistoryX-machines were introduced in 1974 by Samuel Eilenberg, a prominent American mathematician, computer scientist and art collector, but were largely ignored until 1986, when Mike Holcombe, recently appointed to a Senior Lectureship at Sheffield University, began championing their use for specification purposes (Holcombe 1986a, 1986b, 1988). It is probably fair to say that Mike Holcombe has over the past decade achieved, almost single-handedly, the introduction and expansion of X-machine Theory into a scientific and engineering discipline. X-machines now play a role in subjects as diverse as formal approaches to software testing, the modelling of biological and biomolecular processes, and the formulation of hypercomputational (super-Turing) systems.
In 1986, Mike Stannett completed his PhD on General Topology (very pure mathematics) in the Pure Mathematics Department at Sheffield. He joined Holcombe first as an RA, and a year later as a Lecturer, and began constructing nonstandard variants of the X-machine model (Stannett 1988, 1990, 1991, 1998, 2002). At that time the two Mikes comprised the Formal Methods Group (also known as ThR@Sh, for Theoretical Research at Sheffield) in the fledgeling Computer Science Department at Sheffield University - all subsequent developments in the Theory of X-machines are believed to have a Sheffield connection of one kind or another. Initially, the Group focussed on establishing basic properties of X-machines, and on understanding how X-machines could be used to specify complicated systems. Holcombe was particularly interested in the model's ability to specify biological processes, and one of our favourite exemplars was a schematic of the biochemical Kreb's Cycle, formulated as an ATP-manipulation machine. Stannett, in contrast, concentrated on the development of hypercomputational models (systems whose computational power is provably beyond that of the Turing machine).
In 1992, Stannett migrated to macroeconomic modelling, but continued work on hypercomputation and X-machine variants as and when time permitted. In the mean time, Holcombe's PhD students began making a series of important contributions. The most significant was Gilbert Laycock's development of the Stream X-Machine (Laycock and Stannett 1992, Laycock 1993, Laycock 1995). Laycock was motivated by a strong resemblance between stream X-machines and automata, which suggested that Chow's W-Method (a well-known technique for generating test-sets for automata) might be extensible to systems specified by SXM. This idea was subsequently developed by Tudor Balanescu, Florentin Ipate and Kirill Bogdanov, and has been applied to hardware systems by Salim Vanak. Not all of the Sheffield programs have dealt with testing, however. Alex Bell continued the Group's early fascination with biological systems, and produced X-machine models of immunological pathways.
In 1998, Mike Holcombe and Florentin Ipate published an account (Holcombe and Ipate 1998) of the SXM Testing method (SXMT). This can be seen as the culmination of work that began with Laycock's thesis five years earlier. It describes a set of rules which, if followed, ensures complete functional testability of implementations. In other words, their method gives you a finite set of input strings, and if an implementation behaves appropriately for every string in the list, then you can be absolutely certain that the implementation will behave correctly in all situations. Inevitably, such a powerful technique comes at a cost, because ensuring that arbitrary behaviours are completely testable is well known to be an uncomputable problem — the SXMT method overcomes this particular obstacle by constraining the types of system that can be implemented. In particular, the 'business systems' prescribed by Holcombe and Ipate are inherently procedural, and their construction inherently modular and top-down.
Recent years have seen the emergence of other European centres of X-Machine Theory. Important practical work on the development of support tools has been the subject of extensive work by Kefalas, Eleftherakis & Kehris and their group at City College in Thessaloniki, whose X-Machine Development Language (XMDL) allows users to construct and run X-machine models as prolog programs. In Bucharest, research is under way on the language theoretic properties of X-machine variants. Prior to his move to Sheffield, for example, Marian Gheorghe developed possibly the earliest results concerning the grammar systems associated with stream X-machines. Back in the UK, Hierons and Harman have recently shown that some limitations of the SXMT method can be overcome, insofar as determinism constraints can be loosened. In addition, Liverpool University (and especially the work of Ray Paton) has emerged as an important centre for X-Machine applications to biocomputing.
Although Stannett's 1990 'AXM' (Analog X-Machine) and 1998 'TXM' (Timed, or Temporal, X-Machine) variants assume that processes might evolve concurrently, the theory of Concurrent X-Machines has until recently gone largely uninvestigated. The earliest concerted investigation was probably Judith Barnard's development of the Communicating X-Machine model (COMX) as part of her 1993-1996 PhD research at Staffordshire University. Another Communicating X-Machines model has been studied by members of several of the Groups, and is still the focus of continuing work by Tony Cowling, Joaquin Aguardo, Tudor Balanescu and others. This model is based loosely on the use of pigeonholes for transmitting messages (and has been shown to be coextensive with the standard SXM model).
The question naturally arises whether SXMT techniques can be modified to provide complete testability for other types of implementation — in particular, can a variant of SXMT be developed which ensures complete testability of (suitably constrained) OO systems? The MOTIVE project was established by Tony Simons and Mike Holcombe in 1999 in the hope of answering this question positively. The project, which is supported by the EPSRC under grant number GR/M56777, was awarded funds to appoint a full-time Research Associate, and this position was initially filled by Kirill Bogdanov. Replacing Kirill, following the latter's appointment elsewhere within the department, Mike Stannett returned to the Sheffield Group (now known as the Verification and Testing (VT) Group) in November 2000, thus taking our story full circle.
The MOTIVE project generated new developments in the story of X-machines. It became clear early in the project that X-machines are too procedural to represent objects in their pure form, so a new variant of the model (the Object Machine) was proposed, which would allow the methods of an object to be modelled as relations on the underlying 'class type.' By considering simple examples, we have found that this approach is too simplistic, because it tells us nothing about the interactions between methods. Instead, we have developed a hybrid model, combining the testability of stream X-machines and the expressiveness of algebraic specification. At the same time, earlier attempts to generate a hybrid of X-machines and the concurrent process language CCS (Stannett and Simons 2001) led to the realisation that both SXMT and the method of Chow on which it is based can be construed as instances of a general testability theorem for a new class of computational models, called b-machines.
X-machine Theory, then, has been roughly 20 years in the making. It has generated many useful results, and seems likely to generate many more over the next 20 years. In short, this is a very good time to be an X-machine Theorist.