X машинасы: Есептеу моделінің қайнары және қолданыстары

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.

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

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.

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.

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.

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.

M. Stannett and A. J. H. Simons (2002) Complete Behavioural Testing of Object Oriented Systems using CCS Augmented X Machines. Tech Report CS 02 06, Dept of Computer Science, University of Sheffield. Download
J. Aguado and A. J. Cowling (2002) Foundations of the X machine Theory for Testing. Tech Report CS 02 06, Dept of Computer Science, University of Sheffield. Download
J. Aguado and A. J. Cowling (2002) Systems of Communicating X machines for Specifying Distributed Systems. Tech Report CS 02 07, Dept of Computer Science, University of Sheffield. Download
M. Stannett (2005) The Theory of X Machines Part 1. Tech Report CS 05 09, Dept of Computer Science, University of Sheffield. Download