Stream X-Machine
Encyclopedia
The Stream X-machine is a model of computation introduced by Gilbert Laycock in his 1993 PhD thesis, The Theory and Practice of Specification Based Software Testing.
The Theory and Practice of Specification Based Software Testing.
PhD Thesis, University of Sheffield, Dept of Computer Science.
Abstract
Based on Samuel Eilenberg
's X-machine
, an extended finite state machine
for processing data of the type X,Samuel Eilenberg (1974)
Automata, Languages and Machines, Vol. A.
London: Academic Press. the Stream X-Machine is a kind of X-machine
for processing a memory data type Mem with associated input and output streams In* and Out*, that is, where X = Out* × Mem × In*. The transitions of a Stream X-Machine are labelled by functions of the form φ: Mem × In → Out × Mem, that is, which compute an output value and update the memory, from the current memory and an input value.
Although the general X-machine
had been identified in the 1980s as a potentially useful formal model for specifying software systems, it was not until the emergence of the Stream X-Machine that this idea could be fully exploited. Florentin Ipate and Mike Holcombe went on to develop a theory of complete functional testing
,
Correct systems - building a business process solution.
Applied Computing Series.
Berlin: Springer-Verlag. in which complex software systems with hundreds of thousands of states and millions of transitions could be decomposed into separate SXMs that could be tested exhaustively, with a guaranteed proof of correct integration.
Because of the intuitive interpretation of Stream X-Machines as "processing agents with inputs and outputs", they have attracted increasing interest, because of their utility in modelling real-world phenomena. The SXM model has important applications in fields as diverse as computational biology
, software testing
and agent-based computational economics
.
with auxiliary memory, inputs and outputs. It is a variant of the general X-machine
, in which the fundamental data type X = Out* × Mem × In*, that is, a tuple consisting of an output stream, the memory and an input stream. A SXM separates the control flow of a system from the processing carried out by the system. The control is modelled by a finite state machine
(known as the associated automaton) whose transitions are labelled with processing functions chosen from a set Φ (known as the type of the machine), which act upon the fundamental data type.
Each processing function in Φ is a partial function, and can be considered to have the type φ: Mem × In → Out × Mem, where Mem is the memory type, and In and Out are respectively the input and output types. In any given state, a transition is enabled if the domain of the associated function φi includes the next input value and the current memory state. If (at most) one transition is enabled in a given state, the machine is deterministic. Crossing a transition is equivalent to applying the associated function φi, which consumes one input, possibly modifies the memory and produces one output. Each recognised path through the machine therefore generates a list φ1 ... φn of functions, and the SXM composes these functions together to generate a relation on the fundamental data type |φ1 ... φn|: X → X.
in which the fundamental data type X = Out* × Mem × In*. In the original X-machine
, the φi are general relations on X. In the Stream X-Machine, these are usually restricted to functions; however the SXM is still only deterministic if (at most) one transition is enabled in each state.
A general X-machine
handles input and output using a prior encoding function α: Y → X for input, and a posterior decoding function β: X → Z for output, where Y and Z are respectively the input and output types. In a Stream X-Machine, these types are streams:
Y = In*
Z = Out*
and the encoding and decoding functions are defined as:
α(ins) = (<>, mem0, ins)
β(outs, memn, <>) = outs
where ins: In*, outs: Out* and memi: Mem. In other words, the machine is initialized with the whole of the input stream; and the decoded result is the whole of the output stream, provided the input stream is eventually consumed (otherwise the result is undefined).
Each processing function in a SXM is given the abbreviated type φSXM: Mem × In → Out × Mem. This can be mapped onto a general X-machine
relation of the type φ: X → X if we treat this as computing:
φ(outs, memi, in :: ins) = (outs :: out, memi+1, ins)
where
The behaviour is deterministic, if (at most) one transition is enabled in each state. This property, and the ability to control how the machine behaves in a step-wise fashion in response to inputs and memory, makes it an ideal model for the specification of software systems. If the specification and implementation are both assumed to be Stream X-Machines, then the implementation may be tested for conformance to the specification machine, by observing the inputs and outputs at each step. Laycock first highlighted the utility of single-step processing with observations for testing purposes.
Holcombe and Ipate developed this into a practical theory of software testing which was fully compositional, scaling up to very large systems. A proof of correct integration guarantees that testing each component and each integration layer separately corresponds to testing the whole system. This divide-and-conquer approach makes exhaustive testing feasible for large systems.
The testing method is described in a separate article on the Stream X-Machine testing methodology
.
The Theory and Practice of Specification Based Software Testing.
PhD Thesis, University of Sheffield, Dept of Computer Science.
Abstract
Based on Samuel Eilenberg
Samuel Eilenberg
Samuel Eilenberg was a Polish and American mathematician of Jewish descent. He was born in Warsaw, Russian Empire and died in New York City, USA, where he had spent much of his career as a professor at Columbia University.He earned his Ph.D. from University of Warsaw in 1936. His thesis advisor...
's X-machine
X-machine
The X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
, an extended finite state machine
Finite state machine
A finite-state machine or finite-state automaton , or simply a state machine, is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states...
for processing data of the type X,Samuel Eilenberg (1974)
Automata, Languages and Machines, Vol. A.
London: Academic Press. the Stream X-Machine is a kind of X-machine
X-machine
The X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
for processing a memory data type Mem with associated input and output streams In* and Out*, that is, where X = Out* × Mem × In*. The transitions of a Stream X-Machine are labelled by functions of the form φ: Mem × In → Out × Mem, that is, which compute an output value and update the memory, from the current memory and an input value.
Although the general X-machine
X-machine
The X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
had been identified in the 1980s as a potentially useful formal model for specifying software systems, it was not until the emergence of the Stream X-Machine that this idea could be fully exploited. Florentin Ipate and Mike Holcombe went on to develop a theory of complete functional testing
Functional testing
Functional testing is a type of black box testing that bases its test cases on the specifications of the software component under test. Functions are tested by feeding them input and examining the output, and internal program structure is rarely considered .Functional testing differs from system...
,
Correct systems - building a business process solution.
Applied Computing Series.
Berlin: Springer-Verlag. in which complex software systems with hundreds of thousands of states and millions of transitions could be decomposed into separate SXMs that could be tested exhaustively, with a guaranteed proof of correct integration.
Because of the intuitive interpretation of Stream X-Machines as "processing agents with inputs and outputs", they have attracted increasing interest, because of their utility in modelling real-world phenomena. The SXM model has important applications in fields as diverse as computational biology
Computational biology
Computational biology involves the development and application of data-analytical and theoretical methods, mathematical modeling and computational simulation techniques to the study of biological, behavioral, and social systems...
, software testing
Software testing
Software testing is an investigation conducted to provide stakeholders with information about the quality of the product or service under test. Software testing can also provide an objective, independent view of the software to allow the business to appreciate and understand the risks of software...
and agent-based computational economics
Computational economics
Computational economics is a research discipline at the interface between computer science and economic and management science. Areas encompassed include agent-based computational modeling, computational modeling of dynamic macroeconomic systems and transaction costs, other applications in...
.
The Stream X-Machine
A Stream X-Machine (SXM) is an extended finite state machineFinite state machine
A finite-state machine or finite-state automaton , or simply a state machine, is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states...
with auxiliary memory, inputs and outputs. It is a variant of the general X-machine
X-machine
The X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
, in which the fundamental data type X = Out* × Mem × In*, that is, a tuple consisting of an output stream, the memory and an input stream. A SXM separates the control flow of a system from the processing carried out by the system. The control is modelled by a finite state machine
Finite state machine
A finite-state machine or finite-state automaton , or simply a state machine, is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states...
(known as the associated automaton) whose transitions are labelled with processing functions chosen from a set Φ (known as the type of the machine), which act upon the fundamental data type.
Each processing function in Φ is a partial function, and can be considered to have the type φ: Mem × In → Out × Mem, where Mem is the memory type, and In and Out are respectively the input and output types. In any given state, a transition is enabled if the domain of the associated function φi includes the next input value and the current memory state. If (at most) one transition is enabled in a given state, the machine is deterministic. Crossing a transition is equivalent to applying the associated function φi, which consumes one input, possibly modifies the memory and produces one output. Each recognised path through the machine therefore generates a list φ1 ... φn of functions, and the SXM composes these functions together to generate a relation on the fundamental data type |φ1 ... φn|: X → X.
Relationship to X-machines
The Stream X-Machine is a variant of X-machineX-machine
The X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
in which the fundamental data type X = Out* × Mem × In*. In the original X-machine
X-machine
The X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
, the φi are general relations on X. In the Stream X-Machine, these are usually restricted to functions; however the SXM is still only deterministic if (at most) one transition is enabled in each state.
A general X-machine
X-machine
The X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
handles input and output using a prior encoding function α: Y → X for input, and a posterior decoding function β: X → Z for output, where Y and Z are respectively the input and output types. In a Stream X-Machine, these types are streams:
Y = In*
Z = Out*
and the encoding and decoding functions are defined as:
α(ins) = (<>, mem0, ins)
β(outs, memn, <>) = outs
where ins: In*, outs: Out* and memi: Mem. In other words, the machine is initialized with the whole of the input stream; and the decoded result is the whole of the output stream, provided the input stream is eventually consumed (otherwise the result is undefined).
Each processing function in a SXM is given the abbreviated type φSXM: Mem × In → Out × Mem. This can be mapped onto a general X-machine
X-machine
The X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
relation of the type φ: X → X if we treat this as computing:
φ(outs, memi, in :: ins) = (outs :: out, memi+1, ins)
where
:: denotes concatenation of an element and a sequence. In other words, the relation extracts the head of the input stream, modifies memory and appends a value to the tail of the output stream.Processing and Testable Properties
Because of the above equivalence, attention may focus on the way a Stream X-Machine processes inputs into outputs, using an auxiliary memory. Given an initial memory state mem0 and an input stream ins, the machine executes in a step-wise fashion, consuming one input at a time, and generating one output at a time. Provided that (at least) one recognised path path = φ1 ... φn exists leading to a state in which the input has been consumed, the machine yields a final memory state memn and an output stream outs. In general, we can think of this as the relation computed by all recognised paths: | path | : In* → Out*. This is often called the behaviour of the Stream X-Machine.The behaviour is deterministic, if (at most) one transition is enabled in each state. This property, and the ability to control how the machine behaves in a step-wise fashion in response to inputs and memory, makes it an ideal model for the specification of software systems. If the specification and implementation are both assumed to be Stream X-Machines, then the implementation may be tested for conformance to the specification machine, by observing the inputs and outputs at each step. Laycock first highlighted the utility of single-step processing with observations for testing purposes.
Holcombe and Ipate developed this into a practical theory of software testing which was fully compositional, scaling up to very large systems. A proof of correct integration guarantees that testing each component and each integration layer separately corresponds to testing the whole system. This divide-and-conquer approach makes exhaustive testing feasible for large systems.
The testing method is described in a separate article on the Stream X-Machine testing methodology
X-Machine Testing
The X-Machine Testing Methodology is a complete functional testing approach to software- and hardware testing that exploits the scalability of the Stream X-Machine model of computation....
.
See also
- X-machineX-machineThe X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
s, a general description of the X-machine model, including a simple example.
- The Stream X-Machine Testing MethodologyX-Machine TestingThe X-Machine Testing Methodology is a complete functional testing approach to software- and hardware testing that exploits the scalability of the Stream X-Machine model of computation....
, a complete functional testing technique. Using this methodology, it is possible to identify a finite set of tests that exhaustively determine whether an implementation matches its specification. The technique overcomes formal undecidability limitations by insisting that users apply carefully specified design for test principles during implementation.
- Communicating Stream X-Machines (CSXMs)Communicating X-MachineThe Communicating X-Machine is a model of computation introduced by various researchers in the 1990s to model systems composed of communicating agents. The model exists in several variants, which are either based directly on Samuel Eilenberg's X-machine or on Gilbert Laycock's later Stream...
, a concurrent version of the SXM model, with applications in fields ranging from social insects to economics.
External links
- The MOTIVE project, using SXM techniques to generate test sets for object-oriented software.
- The EURACE project, an application of CSXM techniques to agent-based computational economics.
- x-machines.net, a site describing the background to X-machine research.
- Mike (Prof. W.M.L.) Holcombe's web page at Sheffield University.