Jump to content

X-machine: Difference between revisions

Edit links
From Wikipedia, the free encyclopedia
Browse history interactively
← Previous editNext edit →
Content deleted Content added
VisualWikitext
m added ref to Holcombe's 1986 tech report (earliest known XM publication after Eilenberg's book)
m Fixed [Hol88b] date and vol number (checked against x-machines.com)
Line 6: Line 6:


While studying the model in the mid-to-late 1980s, Mike Holcombe noticed that the structure of the X-machine model makes it an ideal tool for [[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.<ref
While studying the model in the mid-to-late 1980s, Mike Holcombe noticed that the structure of the X-machine model makes it an ideal tool for [[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.<ref
name="Hol88">M. Holcombe (1988)
name="Hol88a">M. Holcombe (1988)
'X-machines as a basis for dynamic system specification',
'X-machines as a basis for dynamic system specification',
''Software Engineering Journal'' '''3'''(2), pp. 69-76.</ref>
''Software Engineering Journal'' '''3'''(2), pp. 69-76.</ref>
The structural simplicity of the model makes it extremely flexible; other early illustrations of the idea included Holcombe's specification of human-computer interfaces,<ref
The structural simplicity of the model makes it extremely flexible; other early illustrations of the idea included Holcombe's specification of human-computer interfaces,<ref
name="Hol87">M. Holcombe (1987)
name="Hol88b">M. Holcombe (1988)
'Formal methods in the specification of the human-machine interface',
'Formal methods in the specification of the human-machine interface',
''International J. Command and Control, Communications and Info. Systems.'' '''1'''(2), pp. 24-34.</ref>
''International J. Command and Control, Communications and Info. Systems.'' '''2''', pp. 24-34.</ref>
his modelling of processes in cell biochecmistry,<ref
his modelling of processes in cell biochecmistry,<ref
name="Hol86">M. Holcombe (1986)
name="Hol86">M. Holcombe (1986)
Line 20: Line 20:
name="Sta87">M. Stannett (1987)
name="Sta87">M. Stannett (1987)
'An organisational approach to decision-making in command systems.'
'An organisational approach to decision-making in command systems.'
''International J. Command and Control, Communications and Info. Systems.'' '''1'''(3), pp. 23-34.</ref>.
''International J. Command and Control, Communications and Info. Systems.'' '''1''', pp. 23-34.</ref>.


== Formal definitions ==
== Formal definitions ==

Revision as of 00:05, 22 March 2008

The X-machine (XM) is a theoretical model of computation introduced by Samuel Eilenberg in 1974.[1] The X in "X-machine" represents the 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, and traversing a path in the machine corresponds to applying the associated relations, one after the other.

While studying the model in the mid-to-late 1980s, Mike Holcombe noticed that the structure of the X-machine model makes it an ideal tool for 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.[2] The structural simplicity of the model makes it extremely flexible; other early illustrations of the idea included Holcombe's specification of human-computer interfaces,[3] his modelling of processes in cell biochecmistry,[4] and Stannett's modelling of decision-making in military command systems[5].

Formal definitions

An X-machine is essentially a "machine for manipulating objects of type X". Suppose that X is some datatype, called the fundamental datatype, and that Φ is a set of relations φ: X → X. An X-machine is a finite-state machine whose arrows are labelled by relations in Φ. Each recognised path through the machine generates a list φ1 ... φn of relations. We call the composition φ1 o ... o φn of these relations the path relation corresponding to that path. The behaviour of the X-machine is defined to be the union of all its path-behaviours. In other words, an X-machine can perform a manipulation just so long as one of its recognised paths can perform that computation.

Example

A word-processor can be thought of as a Document-machine, where Document is some data type representing documents. Typical processing relations might include A, a function that inserts the letter 'A' at the current cursor position.

Suppose the machine contains a state called Editing, representing the state in which editing of the document is allowed (as opposed to printing, saving, etc). For each of the letters A - Z, the machine will be equipped with an arrow from Editing to itself. That is, we'll have arrows 

 Editing   →A   Editing 
 Editing   →B   Editing 
 Editing   →C   Editing

and so on.

Suppose also that the keyboard has a special key marked Save, and that pressing Save takes the machine from the Editing state to the terminal state Saved. Hitting the Save button has no effect on the document itself - it simply changes machine state. We'd model it as the identity function (id) on documents. Likwise, we can imagine that the machine always starts up in edit-mode, so that Editing is the machine's initial state.

Now imagine that you're using the word processor to edit a document. One particular path from Editing to Saved would be

Editing →H Editing →E Editing →L Editing →L Editing →O Editing →id Saved

This path goes from the initial state Editing to the terminal state Saved, so it is recognised by the finite state machine, and contributes to the behaviour of the X-machine. The path relation computed by this path has the effect of inserting the word "HELLO" into the document.

Variants of the X-machine Model

The X-machine is rarely encountered in its original form, but underpins several subsequent models of computation. The earliest variant, the continuous-time Analog X-Machine (AXM), was introduced by Mike Stannett in 1990 as a potentially "super-Turing" model of computation;[6] it is consequently related to work in hypercomputation theory.[7] However, the most commonly encountered X-machine variant is Gilbert Laycock's 1993 Stream X-Machine (SXM) model,[8] which forms the basis for much work in the development of software that can be guaranteed to be testable.[9][10]

Several X-machine variants have been proposed in the context of concurrent or parallel computing. NASA has recently discussed using a combination of X-machines and the process calculus WSCCS in the development of swarm satellite systems.[11] This model is expected to have features in common with the CCS-XM ("CCS-augmented X-machine") model developed by Simons and Stannett in 2002 to support complete behavioural testing of object-oriented systems,[12] but no definitive comparison of the two models has as yet been conducted. Another related approach (though again, no formal comparison has yet been undertaken) is embodied in Judith Barnard's 1995 Communicating X-machine (CXM) model,[13][14] in which machines are connected via named communication channels; this model exists in both discrete- and real-timed variants.[15] The CSXM (Communicating Stream X-Machine) model was first published in 1994, having been developed by Philip Bird as part of his PhD work, under the supervision of Tony Cowling.[16] Cowling and his associates have continued to study the model, and have developed numerous applications.[17] Despite their superficial similarities, the CSXM model differs from the CXM in several ways; in particular, the machines communicate indirectly via a central nexus (essentially an array of pigeonholes) rather than directly via shared channels.

See Also


Downloadable Technical Reports  

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



References

  1. ^ S. Eilenberg (1974) Automata, Languages and Machines, Vol. A. Academic Press, London.
  2. ^ M. Holcombe (1988) 'X-machines as a basis for dynamic system specification', Software Engineering Journal 3(2), pp. 69-76.
  3. ^ M. Holcombe (1988) 'Formal methods in the specification of the human-machine interface', International J. Command and Control, Communications and Info. Systems. 2, pp. 24-34.
  4. ^ M. Holcombe (1986) 'Mathematical models of cell biochemistry'. Technical Report CS-86-4, Dept of Computer Science, Sheffield University.
  5. ^ M. Stannett (1987) 'An organisational approach to decision-making in command systems.' International J. Command and Control, Communications and Info. Systems. 1, pp. 23-34.
  6. ^ M. Stannett (1990) 'X-machines and the Halting Problem: Building a super-Turing machine'. Formal Aspects of Computing 2, pp. 331-41.
  7. ^ B. J. Copeland (2002) 'Hypercomputation'. Minds and Machines 12, pp. 461-502.
  8. ^ Gilbert Laycock (1993) The Theory and Practice of Specification Based Software Testing. PhD Thesis, University of Sheffield. Abstract
  9. ^ M. Holcombe and F. Ipate (1998) Correct Systems - Building a Business Process Solution. Springer, Applied Computing Series.
  10. ^ F. Ipate and M. Holcombe (1998) 'A method for refining and testing generalised machine specifications'. Int. J. Comp. Math. 68, pp. 197-219.
  11. ^ M. G. Hinchey, C. A. Rouff, J. L. Rash and W. F. Truszkowski (2005) "Requirements of an Integrated Formal Method for Intelligent Swarms", in Proceedings of FMICS'05, September 5–6, 2005, Lisbon, Portugal. Association for Computing Machinery, pp. 125-133.
  12. ^ M. Stannett and A. J. H. Simons (2002) CCS-Augmented X-Machines. Technical Report CS-2002-04, Dept of Computer Science, Sheffield University, UK.
  13. ^ J. Barnard, C. Theaker, J. Whitworth and M. Woodward (1995) "Real-time communicating X-machines for the formal design of real-time systems", in Proceedings of DARTS '95, Universite Libre, Brussels, Belgium, 9-11 November 2005
  14. ^ J. Barnard (1996) COMX: A methodology for the formal design of computer systems using Communicating X-machines. PhD Thesis, Staffordshire University.
  15. ^ A. Alderson and J. Barnard (1997) 'On Making a Crossing Safe'. Technical Report SOCTR/97/01, School of Computing, Staffordshire University. (Citeseer)
  16. ^ P. R. Bird and A. J. Cowling (1994) "Modelling Logic Programming Using a Network of Communicating Machines", in Proc. 2nd Euromicro Workshop on Parallel and Distributed Processing, Malaga, 26-28 January 1994, pages 156 - 161. Abstract
  17. ^ A. J. Cowling (2005) "A Formal Model for Test Frames", in P. McMinn (ed.), Proc. UK Software Testing Conference 2005, Sheffield, 5-6 September 2005, pp. 83-98. (Available online)
Retrieved from "https://en.wikipedia.org/enwiki/w/index.php?title=X-machine&oldid=199954300"