{"history":[],"article":{"id":"b9274003-a440-40c4-829c-78bdf55d9db0","title":"X-machine","slug":"x-machine","content":":::summary\n:::\n\n# \nThe **X-machine** (XM) is a theoretical model of [computation](https://bliptext.com/articles/computation) introduced by [Samuel Eilenberg](https://bliptext.com/articles/samuel-eilenberg) in 1974.S.\nEilenberg (1974)\nAutomata, Languages and Machines, Vol. A.\nAcademic Press, London.\nThe 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.\nThe X-machine model is structurally the same as the [finite-state machine](https://bliptext.com/articles/finite-state-machine), except that the symbols used to label the machine's transitions denote [relations](https://bliptext.com/articles/relation-mathematics) of type X→X.\nCrossing 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.\n\n# Original theory\nEilenberg's original X-machine was a completely general theoretical model of computation (subsuming the [Turing machine](https://bliptext.com/articles/turing-machine), for example), which admitted deterministic, non-deterministic and non-terminating computations.\nHis seminal work published many variants of the basic X-machine model, each of which generalized the [finite-state machine](https://bliptext.com/articles/finite-state-machine) in a slightly different way.\nIn the most general model, an X-machine is essentially a \"machine for manipulating objects of type X\".\nSuppose that X is some [datatype](https://bliptext.com/articles/datatype), called the fundamental [datatype](https://bliptext.com/articles/datatype), and that Φ is a set of (partial) relations φ: X → X. An X-machine is a [finite-state machine](https://bliptext.com/articles/finite-state-machine) whose arrows are labelled by relations in Φ.\nIn any given state, one or more transitions may be enabled if the [domain](https://bliptext.com/articles/domain-of-a-relation) of the associated relation φi accepts (a subset of) the current values stored in X. In each cycle, all enabled transitions are assumed to be taken.\nEach recognised path through the machine generates a list φ1 ... φn of relations.\nWe call the composition φ1 o ... o φn of these relations the path relation corresponding to that path.\nThe behaviour of the X-machine is defined to be the union of all the behaviours computed by its path relations.\nIn general, this is non-deterministic, since applying any relation computes a set of outcomes on X. In the formal model, all possible outcomes are considered together, in parallel.\nFor practical purposes, an X-machine should describe some finite computation.\nAn encoding function α: Y → X converts from some input data type Y into the initial state of X, and a decoding function β: X → Z, converts back from the final state(s) of X into some output data type Z. Once the initial state of X is populated, the X-machine runs to completion, and the outputs are then observed.\nIn general, a machine may deadlock (be blocked), or livelock (never halt), or perform one or more complete computations.\nFor this reason, more recent research has focused on deterministic X-machines, whose behaviour can be controlled and observed more precisely.\n\n## Example\nA compiler with a peep-hole optimizer can be thought of as a machine for optimizing program structure.\nIn this **Optimizer**-machine, the encoding function α takes source code from the input-type Y (the program source) and loads it into the memory-type X (a parse tree).\nSuppose that the machine has several states, called **FindIncrements**, **FindSubExprs** and **Completed**.\nThe machine starts in the initial state **FindIncrements**, which is linked to other states via the transitions:\n****FindIncrements**** →DoIncrement ****FindIncrements****\n**FindIncrements** →SkipIncrement **FindSubExprs**\n****FindSubExprs**** →DoSubExpr ****FindSubExprs****\n**FindSubExprs** →SkipSubExpr **Completed**\nThe relation **DoIncrement** maps a parsed subtree corresponding to \"x := x + 1\" into the optimized subtree \"++x\".\nThe relation **DoSubExpr** maps a parse tree containing multiple occurrences of the same expression \"x + y ... x + y\" into an optimized version with a local variable to store the repeated computation \"z := x + y; ... z ... z\".\nThese relations are only enabled if X contains the domain values (subtrees) on which they operate.\nThe remaining relations **SkipIncrement** and **SkipSubExpr** are nullops (identity relations) enabled in the complementary cases.\nSo, the **Optimizer**-machine will run to completion, first converting trivial additions into in-place increments (while in the **FindIncrements** state), then it will move on to the **FindSubExprs** state and perform a series of common sub-expression removals, after which it will move to the final state **Completed**.\nThe decoding function β will then map from the memory-type X (the optimized parse-tree) into the output-type Z (optimized machine code).\n\n## Convention\nWhen referring to Eilenberg's original model, \"X-machine\" is typically written with a lower-case \"m\", because the sense is \"any machine for processing X\".\nWhen referring to later specific models, the convention is to use a capital \"M\" as part of the proper name of that variant.\n\n# 1980s\nInterest in the X-machine was revived in the late 1980s by Mike Holcombe,M.\nHolcombe (1988)\n'X-machines as a basis for dynamic system specification',\nSoftware Engineering Journal **3**(2), pp. 69-76.\nwho noticed that the model was ideal for software [formal specification](https://bliptext.com/articles/formal-specification) purposes, because it cleanly separates control flow from processing.\nProvided 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.\nThe structural simplicity of the model makes it extremely flexible; other early illustrations of the idea included Holcombe's specification of human-computer interfaces,M.\nHolcombe (1988)\n'Formal methods in the specification of the human-machine interface',\n''International J. Command and Control, Communications and Info.\nSystems.'' **2**, pp. **2**4-34.\nhis modelling of processes in cell biochemistry,M.\nHolcombe (1986)\n'Mathematical models of cell biochemistry'.\nTechnical Report CS-86-4, Dept of Computer Science, Sheffield University.\nand Stannett's modelling of decision-making in military command systems.M.\nStannett (1987)\n'An organisational approach to decision-making in command systems.'\n''International J. Command and Control, Communications and Info.\nSystems.'' **1**, pp. 23-34.\n\n# 1990s\nX-machines have received renewed attention since the mid-1990s, when Gilbert Laycock's deterministic [Stream X-Machine](https://bliptext.com/articles/stream-x-machine) was found to serve as the basis for specifying large software systems that are completely testable.M.\nHolcombe and F. Ipate (1998)\nCorrect Systems - Building a Business Process Solution.\nSpringer, Applied Computing Series.\nAnother variant,\nthe [Communicating Stream X-Machine](https://bliptext.com/articles/communicating-x-machine) offers a useful testable model for biological processes\nand future swarm-based satellite systems.\n\nM. G. Hinchey, C. A. Rouff, J. L. Rash and W. F. Truszkowski (2005)\n'Requirements of an Integrated Formal Method for Intelligent Swarms',\nin Proceedings of FMICS'05, September 5–6, 2005, Lisbon, Portugal.\nAssociation for Computing Machinery, pp. 125-133.\n\n# 2000s\nX-machines have been applied to [lexical semantics](https://bliptext.com/articles/lexical-semantics) by [András Kornai](https://bliptext.com/articles/andr-s-kornai), who models word meaning by `pointed' machines that have one member of the base set X distinguished.\nApplication to other branches of linguistics, in particular to a contemporary reformulation of [Pāṇini](https://bliptext.com/articles/p-ini) were pioneered by [Gerard Huet](https://bliptext.com/articles/gerard-huet) and his co-workers\n\n# Major variants\nThe X-machine is rarely encountered in its original form, but underpins several subsequent models of computation.\nThe most influential model on theories of software testing has been the [Stream X-Machine](https://bliptext.com/articles/stream-x-machine).\n[NASA](https://bliptext.com/articles/nasa) has recently discussed using a combination of [Communicating Stream X-Machines](https://bliptext.com/articles/communicating-x-machine) and the process calculus WSCSS in the design and testing of swarm satellite systems.\n\n## Analog X Machine (AXM)\nThe earliest variant, the continuous-time Analog X-Machine (AXM), was introduced by Mike Stannett in 1990 as a potentially \"super-Turing\" model of computation;M.\nStannett (1990)\n'X-machines and the Halting Problem: Building a super-Turing machine'.\nFormal Aspects of Computing **2**, pp. 331-41.\nit is consequently related to work in [hypercomputation](https://bliptext.com/articles/hypercomputation) theory.B.\nJ. Copeland (2002)\n'Hypercomputation'.\nMinds and Machines **12**, pp. 461-502.\n\n## Stream X-Machine (SXM)\nThe most commonly encountered X-machine variant is Gilbert Laycock's 1993 [Stream X-Machine](https://bliptext.com/articles/stream-x-machine) ([SXM](https://bliptext.com/articles/sxm-computational-model)) model,\nwhich forms the basis for Mike Holcombe and Florentin Ipate's theory of complete software testing, which guarantees known correctness properties, once testing is over.\nThe 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.\nThe 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.\nThese are witness values, that guarantee that particular functions were executed on each step.\nAs 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.\nThis 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.\n\n## Communicating X-Machine (CXM)\nThe earliest proposal for connecting several X-machines in parallel is Judith Barnard's 1995 Communicating X-machine (CXM or COMX) model,J.\nBarnard, 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 J.\nBarnard (1996)\nCOMX: A methodology for the formal design of computer systems using Communicating X-machines.\nPhD Thesis, Staffordshire University.\nin which machines are connected via named communication channels (known as ports); this model exists in both discrete- and real-timed variants.A.\nAlderson and J. Barnard (1997)\n'On Making a Crossing Safe',\nTechnical Report SOCTR/97/01, School of Computing, Staffordshire University.\n[(Citeseer)](https://bliptext.com/articles/undefined)\nEarlier versions of this work were not fully formal and did not show full input/output relations.\nA similar Communicating X-Machine approach using buffered\nchannels was developed by Petros Kefalas.\nThe focus of this work was on expressiveness in the composition of components.\nThe ability to reassign channels meant that some of the testing theorems from Stream X-Machines did not carry over.\nThese variants are discussed [in more detail](https://bliptext.com/articles/communicating-x-machine) on a separate page.\n\n## Communicating Stream X-Machine (CSXM)\nThe 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.P.\nR. Bird and A. J. Cowling (1994)\n'Modelling logic programming using a network of communicating machines', in ''Proc.\n2nd Euromicro Workshop on Parallel and Distributed Processing, Malaga, 26–28 January 1994'', pp. 156-161.\n[Abstract](https://bliptext.com/articles/undefined) In Vertan's model, the machines communicate indirectly, via a shared communication matrix (essentially an array of pigeonholes), rather than directly via shared channels.\nBălănescu, Cowling, Georgescu, Vertan and others have studied the formal properties of this CSXM model in some detail.\nFull input/output relations can be shown.\nThe communication matrix establishes a protocol for synchronous communication.\nThe advantage of this is that it decouples each machine's processing from their communication, allowing the separate testing of each behaviour.\nThis compositional model was proven equivalent to a standard [Stream X-Machine](https://bliptext.com/articles/stream-x-machine), so leveraging the earlier testing theory developed by Holcombe and Ipate.\nThis X-machine variant is discussed [in more detail](https://bliptext.com/articles/communicating-x-machine) on a separate page.\n\n## Object X-Machine (OXM)\nKirill Bogdanov and Anthony Simons developed several variants of the X-machine to model the behaviour of objects in object-oriented systems.\nThis model differs from the [Stream X-Machine](https://bliptext.com/articles/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.\nFurther 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.\nA \"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 communicationM.\nStannett and A. J. H. Simons (2002)\n'CCS-Augmented X-Machines',\nTechnical Report CS-2002-04, Department of Computer Science, Sheffield University, UK.\nThis is expected to bear some similarity with [NASA](https://bliptext.com/articles/nasa)'s recent proposal; but no definitive comparison of the two models has as yet been conducted.\n\n## Downloadable technical reports","current_revision":null,"created_by":"kACnuQmH5k9Nr5VNVEpVeg7XpvUmMctD","created_at":"2025-01-25T21:13:42.551Z","updated_at":"2025-01-25T21:13:42.551Z","search_vector":"'machin':3 'x':2 'x-machin':1","search_content":" \n \n\n# \nThe **X-machine** (XM) is a theoretical model of [computation](https://bliptext.com/articles/computation) introduced by [Samuel Eilenberg](https://bliptext.com/articles/samuel-eilenberg) in 1974. S.\nEilenberg (1974)\nAutomata, Languages and Machines, Vol. A.\nAcademic Press, London.\nThe 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.\nThe X-machine model is structurally the same as the [finite-state machine](https://bliptext.com/articles/finite-state-machine), except that the symbols used to label the machine's transitions denote [relations](https://bliptext.com/articles/relation-mathematics) of type X→X.\nCrossing 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.\n\n# Original theory\nEilenberg's original X-machine was a completely general theoretical model of computation (subsuming the [Turing machine](https://bliptext.com/articles/turing-machine), for example), which admitted deterministic, non-deterministic and non-terminating computations.\nHis seminal work published many variants of the basic X-machine model, each of which generalized the [finite-state machine](https://bliptext.com/articles/finite-state-machine) in a slightly different way.\nIn the most general model, an X-machine is essentially a \"machine for manipulating objects of type X\".\nSuppose that X is some [datatype](https://bliptext.com/articles/datatype), called the fundamental [datatype](https://bliptext.com/articles/datatype), and that Φ is a set of (partial) relations φ: X → X. An X-machine is a [finite-state machine](https://bliptext.com/articles/finite-state-machine) whose arrows are labelled by relations in Φ.\nIn any given state, one or more transitions may be enabled if the [domain](https://bliptext.com/articles/domain-of-a-relation) of the associated relation φi accepts (a subset of) the current values stored in X. In each cycle, all enabled transitions are assumed to be taken.\nEach recognised path through the machine generates a list φ1 ... φn of relations.\nWe call the composition φ1 o ... o φn of these relations the path relation corresponding to that path.\nThe behaviour of the X-machine is defined to be the union of all the behaviours computed by its path relations.\nIn general, this is non-deterministic, since applying any relation computes a set of outcomes on X. In the formal model, all possible outcomes are considered together, in parallel.\nFor practical purposes, an X-machine should describe some finite computation.\nAn encoding function α: Y → X converts from some input data type Y into the initial state of X, and a decoding function β: X → Z, converts back from the final state(s) of X into some output data type Z. Once the initial state of X is populated, the X-machine runs to completion, and the outputs are then observed.\nIn general, a machine may deadlock (be blocked), or livelock (never halt), or perform one or more complete computations.\nFor this reason, more recent research has focused on deterministic X-machines, whose behaviour can be controlled and observed more precisely.\n\n## Example\nA compiler with a peep-hole optimizer can be thought of as a machine for optimizing program structure.\nIn this **Optimizer**-machine, the encoding function α takes source code from the input-type Y (the program source) and loads it into the memory-type X (a parse tree).\nSuppose that the machine has several states, called **FindIncrements**, **FindSubExprs** and **Completed**.\nThe machine starts in the initial state **FindIncrements**, which is linked to other states via the transitions:\n****FindIncrements**** →DoIncrement ****FindIncrements****\n**FindIncrements** →SkipIncrement **FindSubExprs**\n****FindSubExprs**** →DoSubExpr ****FindSubExprs****\n**FindSubExprs** →SkipSubExpr **Completed**\nThe relation **DoIncrement** maps a parsed subtree corresponding to \"x := x + 1\" into the optimized subtree \"++x\".\nThe relation **DoSubExpr** maps a parse tree containing multiple occurrences of the same expression \"x + y ... x + y\" into an optimized version with a local variable to store the repeated computation \"z := x + y; ... z ... z\".\nThese relations are only enabled if X contains the domain values (subtrees) on which they operate.\nThe remaining relations **SkipIncrement** and **SkipSubExpr** are nullops (identity relations) enabled in the complementary cases.\nSo, the **Optimizer**-machine will run to completion, first converting trivial additions into in-place increments (while in the **FindIncrements** state), then it will move on to the **FindSubExprs** state and perform a series of common sub-expression removals, after which it will move to the final state **Completed**.\nThe decoding function β will then map from the memory-type X (the optimized parse-tree) into the output-type Z (optimized machine code).\n\n## Convention\nWhen referring to Eilenberg's original model, \"X-machine\" is typically written with a lower-case \"m\", because the sense is \"any machine for processing X\".\nWhen referring to later specific models, the convention is to use a capital \"M\" as part of the proper name of that variant.\n\n# 1980s\nInterest in the X-machine was revived in the late 1980s by Mike Holcombe, M.\nHolcombe (1988)\n'X-machines as a basis for dynamic system specification',\nSoftware Engineering Journal **3**(2), pp. 69-76.\nwho noticed that the model was ideal for software [formal specification](https://bliptext.com/articles/formal-specification) purposes, because it cleanly separates control flow from processing.\nProvided 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.\nThe structural simplicity of the model makes it extremely flexible; other early illustrations of the idea included Holcombe's specification of human-computer interfaces, M.\nHolcombe (1988)\n'Formal methods in the specification of the human-machine interface',\n''International J. Command and Control, Communications and Info.\nSystems.'' **2**, pp. **2**4-34.\nhis modelling of processes in cell biochemistry, M.\nHolcombe (1986)\n'Mathematical models of cell biochemistry'.\nTechnical Report CS-86-4, Dept of Computer Science, Sheffield University.\nand Stannett's modelling of decision-making in military command systems. M.\nStannett (1987)\n'An organisational approach to decision-making in command systems.'\n''International J. Command and Control, Communications and Info.\nSystems.'' **1**, pp. 23-34.\n\n# 1990s\nX-machines have received renewed attention since the mid-1990s, when Gilbert Laycock's deterministic [Stream X-Machine](https://bliptext.com/articles/stream-x-machine) was found to serve as the basis for specifying large software systems that are completely testable. M.\nHolcombe and F. Ipate (1998)\nCorrect Systems - Building a Business Process Solution.\nSpringer, Applied Computing Series.\nAnother variant,\nthe [Communicating Stream X-Machine](https://bliptext.com/articles/communicating-x-machine) offers a useful testable model for biological processes\nand future swarm-based satellite systems.\n \nM. G. Hinchey, C. A. Rouff, J. L. Rash and W. F. Truszkowski (2005)\n'Requirements of an Integrated Formal Method for Intelligent Swarms',\nin Proceedings of FMICS'05, September 5–6, 2005, Lisbon, Portugal.\nAssociation for Computing Machinery, pp. 125-133.\n\n# 2000s\nX-machines have been applied to [lexical semantics](https://bliptext.com/articles/lexical-semantics) by [András Kornai](https://bliptext.com/articles/andr-s-kornai), who models word meaning by `pointed' machines that have one member of the base set X distinguished.\nApplication to other branches of linguistics, in particular to a contemporary reformulation of [Pāṇini](https://bliptext.com/articles/p-ini) were pioneered by [Gerard Huet](https://bliptext.com/articles/gerard-huet) and his co-workers\n\n# Major variants\nThe X-machine is rarely encountered in its original form, but underpins several subsequent models of computation.\nThe most influential model on theories of software testing has been the [Stream X-Machine](https://bliptext.com/articles/stream-x-machine).\n[NASA](https://bliptext.com/articles/nasa) has recently discussed using a combination of [Communicating Stream X-Machines](https://bliptext.com/articles/communicating-x-machine) and the process calculus WSCSS in the design and testing of swarm satellite systems.\n\n## Analog X Machine (AXM)\nThe earliest variant, the continuous-time Analog X-Machine (AXM), was introduced by Mike Stannett in 1990 as a potentially \"super-Turing\" model of computation; M.\nStannett (1990)\n'X-machines and the Halting Problem: Building a super-Turing machine'.\nFormal Aspects of Computing **2**, pp. 331-41.\nit is consequently related to work in [hypercomputation](https://bliptext.com/articles/hypercomputation) theory. B.\nJ. Copeland (2002)\n'Hypercomputation'.\nMinds and Machines **12**, pp. 461-502.\n\n## Stream X-Machine (SXM)\nThe most commonly encountered X-machine variant is Gilbert Laycock's 1993 [Stream X-Machine](https://bliptext.com/articles/stream-x-machine) ([SXM](https://bliptext.com/articles/sxm-computational-model)) model,\nwhich forms the basis for Mike Holcombe and Florentin Ipate's theory of complete software testing, which guarantees known correctness properties, once testing is over.\nThe 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.\nThe 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.\nThese are witness values, that guarantee that particular functions were executed on each step.\nAs 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.\nThis 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.\n\n## Communicating X-Machine (CXM)\nThe earliest proposal for connecting several X-machines in parallel is Judith Barnard's 1995 Communicating X-machine (CXM or COMX) model, J.\nBarnard, 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 J.\nBarnard (1996)\nCOMX: A methodology for the formal design of computer systems using Communicating X-machines.\nPhD Thesis, Staffordshire University.\nin which machines are connected via named communication channels (known as ports); this model exists in both discrete- and real-timed variants. A.\nAlderson and J. Barnard (1997)\n'On Making a Crossing Safe',\nTechnical Report SOCTR/97/01, School of Computing, Staffordshire University.\n[(Citeseer)](https://bliptext.com/articles/undefined)\nEarlier versions of this work were not fully formal and did not show full input/output relations.\nA similar Communicating X-Machine approach using buffered\nchannels was developed by Petros Kefalas.\nThe focus of this work was on expressiveness in the composition of components.\nThe ability to reassign channels meant that some of the testing theorems from Stream X-Machines did not carry over.\nThese variants are discussed [in more detail](https://bliptext.com/articles/communicating-x-machine) on a separate page.\n\n## Communicating Stream X-Machine (CSXM)\nThe 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. P.\nR. Bird and A. J. Cowling (1994)\n'Modelling logic programming using a network of communicating machines', in ''Proc.\n2nd Euromicro Workshop on Parallel and Distributed Processing, Malaga, 26–28 January 1994'', pp. 156-161.\n[Abstract](https://bliptext.com/articles/undefined) In Vertan's model, the machines communicate indirectly, via a shared communication matrix (essentially an array of pigeonholes), rather than directly via shared channels.\nBălănescu, Cowling, Georgescu, Vertan and others have studied the formal properties of this CSXM model in some detail.\nFull input/output relations can be shown.\nThe communication matrix establishes a protocol for synchronous communication.\nThe advantage of this is that it decouples each machine's processing from their communication, allowing the separate testing of each behaviour.\nThis compositional model was proven equivalent to a standard [Stream X-Machine](https://bliptext.com/articles/stream-x-machine), so leveraging the earlier testing theory developed by Holcombe and Ipate.\nThis X-machine variant is discussed [in more detail](https://bliptext.com/articles/communicating-x-machine) on a separate page.\n\n## Object X-Machine (OXM)\nKirill Bogdanov and Anthony Simons developed several variants of the X-machine to model the behaviour of objects in object-oriented systems.\nThis model differs from the [Stream X-Machine](https://bliptext.com/articles/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.\nFurther 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.\nA \"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 M.\nStannett and A. J. H. Simons (2002)\n'CCS-Augmented X-Machines',\nTechnical Report CS-2002-04, Department of Computer Science, Sheffield University, UK.\nThis is expected to bear some similarity with [NASA](https://bliptext.com/articles/nasa)'s recent proposal; but no definitive comparison of the two models has as yet been conducted.\n\n## Downloadable technical reports","revisionCount":0},"hasMore":false,"nextCursor":null}

History