Editing X-machine (section)

== 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 X-Machine|Communicating Stream X-Machines]] and the process calculus WSCSS in the design and testing of ''swarm satellite'' systems.<ref name="HRRT05" />

=== Analog X Machine (AXM) ===
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;<ref
  name="Sta90">M. Stannett (1990) 
  'X-machines and the Halting Problem: Building a super-Turing machine'. 
  ''Formal Aspects of Computing'' '''2''', pp. 331-41.</ref>
it is consequently related to work in [[hypercomputation]] theory.<ref
  name="Cop02">B. J. Copeland (2002) 
  'Hypercomputation'. 
  ''Minds and Machines'' '''12''', pp. 461-502.</ref>

=== Stream X-Machine (SXM) ===
{{main|Stream X-Machine}}
The most commonly encountered X-machine variant is Gilbert Laycock's 1993 ''[[Stream X-Machine]]'' (''[[SXM (computational model)|SXM]]'') model,<ref name="Lay" />
which forms the basis for Mike Holcombe and Florentin Ipate's theory of ''complete'' software testing, which guarantees known correctness properties, once testing is over.<ref name="HI98" /><ref name="IH98">F. Ipate and M. Holcombe (1998) 'A method for refining and testing generalised machine specifications'.
  ''Int. J. Comp. Math.'' '''68''', pp. 197-219.</ref>  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,<ref name="IpaHol97">F. Ipate and M. Holcombe (1997) 'An integration testing method that is proved to find all faults', ''International Journal of Computer Mathematics'' '''63''', pp. 159-178.</ref> 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,<ref
  name="BTWM95">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''</ref><ref
  name="Bar96">J. Barnard (1996)
  ''COMX: A methodology for the formal design of computer systems using Communicating X-machines''. 
  PhD Thesis, Staffordshire University.</ref>
in which machines are connected via named communication channels (known as ''ports''); this model exists in both discrete- and real-timed variants.<ref
  name="AldBarn97">A. Alderson and J. Barnard (1997)
  'On Making a Crossing Safe',
  ''Technical Report SOCTR/97/01'', School of Computing, Staffordshire University.
  [http://citeseer.ist.psu.edu/alderson97making.html (Citeseer)]
</ref>  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.<ref name="KEK00a">E. Kehris, G. Eleftherakis and P. Kefalas (2000) 'Using X-machines to model and test discrete event simulation programs', ''Proc. 4th World Multiconference on Circuits, Systems, Communications and Computers'', Athens.</ref><ref name="KEK00b">P. Kefalas, G. Eleftherakis and E. Kehris (2000) 'Communicating X-machines: a practical approach for modular specification of large systems', ''Technical Report CS-09/00, Department of Computer Science'', City College, Thessaloniki.</ref>  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 [[Communicating X-Machine|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,<ref name="GeoVer00">H. Georgescu and C. Vertan (2000) 'A new approach to communicating stream X-machines', ''Journal of Universal Computer Science'' '''6''' ''(5)'', pp. 490-502.</ref> based on earlier work on communicating automatata by Philip Bird and Anthony Cowling.<ref
  name="BC94">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'', pp. 156-161.
  [http://www.dcs.shef.ac.uk/~ajc/csxms/papers/euromic94.html Abstract]</ref>  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]],<ref name="BCHGGV99">T.Balanescu, A. J. Cowling, H. Georgescu, M. Gheorghe, M. Holcombe and C. Vertan (1999) 'Communicating X-machines systems are no more than X-machines', ''Journal of Universal Computer Science'', '''5''' ''(9)'', pp. 494-507.</ref> so leveraging the earlier testing theory developed by Holcombe and Ipate.

This X-machine variant is discussed [[Communicating X-Machine|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.<ref name="SBH01">A. J. H. Simons, K. E. Bogdanov and W. M. L. Holcombe (2001) 'Complete functional testing using object machines', ''Technical Report CS-01-18, Department of Computer Science'', University of Sheffield</ref>  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.<ref name="Simo06">A. J. H. Simons (2006) 'A theory of regression testing for behaviourally compatible object types', ''Software Testing, Verification and Reliability'', '''16''' ''(3)'', John Wiley, pp. 133-156.</ref>

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<ref
  name="SS02">M. Stannett and A. J. H. Simons (2002)
  'CCS-Augmented X-Machines', 
  ''Technical Report CS-2002-04, Department of Computer Science'', Sheffield University, UK.</ref>  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.