Stream X-Machine

The Stream X-machine (SXM) is a model of computation introduced by Gilbert Laycock in his 1993 PhD thesis, The Theory and Practice of Specification Based Software Testing.[1] Based on Samuel Eilenberg's X-machine, an extended finite state machine for processing data of the type X,[2] 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,[3] 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,[4] 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.[5]

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.

The Stream X-Machine

A Stream X-Machine (SXM) is an extended finite state machine 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.

Relationship to X-machines

The Stream X-Machine is a variant of X-machine 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 :: 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.[1]

Holcombe and Ipate developed this into a practical theory of software testing[4] which was fully compositional, scaling up to very large systems.[6] A proof of correct integration[5] 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.

Applications

Stream X-Machines have been used in a number of different application areas.

See also

External links

References

  1. 1 2 Gilbert Laycock (1993) The Theory and Practice of Specification Based Software Testing. PhD Thesis, University of Sheffield, Dept of Computer Science. Abstract
  2. ↑ Samuel Eilenberg (1974) Automata, Languages and Machines, Vol. A. London: Academic Press.
  3. ↑ M. Holcombe (1988) 'X-machines as a basis for dynamic system specification'. Software Engineering Journal 3 (2), pp. 69-76.
  4. 1 2 Mike Holcombe and Florentin Ipate (1998) Correct systems - building a business process solution. Applied Computing Series. Berlin: Springer-Verlag.
  5. 1 2 F. Ipate and W. M. L. Holcombe (1997) 'An integration testing method which is proved to find all faults'. Int. J. Comp. Math., 63, pp. 159-178.
  6. ↑ F. Ipate and M. Holcombe (1998) 'A method for refining and testing generalised machine specifications'. Int. J. Comp. Math. 68, pp. 197-219.
This article is issued from Wikipedia - version of the Thursday, March 24, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.