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) The most commonly encountered X-machine variant is Gilbert Laycock's 1993 Stream X-Machine (SXM) model, 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. 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,<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. (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. 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.