Stream X-Machine

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".Gilbert Laycock (1993) "The Theory and Practice of Specification Based Software Testing". PhD Thesis, University of Sheffield, Dept of Computer Science. [http://www.mcs.le.ac.uk/people/gtl1/PhDabstract.html 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,M. Holcombe (1988) 'X-machines as a basis for dynamic system specification'. "Software Engineering Journal" 3 "(2)", pp. 69-76.] 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,Mike Holcombe and Florentin Ipate (1998) "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.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.]

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") = (<>, "mem"0, "ins") β("outs", "mem"n, <>) = "outs"

where "ins: In"*, "outs: Out"* and "mem"i: "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", "mem"i, "in" :: "ins") = ("outs" :: "out", "mem"i+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 "mem"0 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 "mem"n 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.F. Ipate and M. Holcombe (1998) 'A method for refining and testing generalised machine specifications'. "Int. J. Comp. Math." 68, pp. 197-219.] 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.

Applications

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

Cell Biology

Please add content here.

Social Insect Behaviour

Please add content here.

Software Systems

Please add content here.

Hardware Systems

Please add content here.

Computational Economics

Please add content here.

ee also

* X-machines, a general description of the X-machine model, including a simple example.

* The Stream X-Machine Testing Methodology, 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), a concurrent version of the SXM model, with applications in fields ranging from social insects to economics.

External links

* [http://www.dcs.shef.ac.uk/~ajhs/motive/ The MOTIVE project] , using SXM techniques to generate test sets for object-oriented software.
* [http://www.dcs.shef.ac.uk/~stc/eurace/ The EURACE project] , an application of CSXM techniques to agent-based computational economics.
* [http://www.x-machines.net x-machines.net] , a site describing the background to X-machine research.
* [http://www.dcs.shef.ac.uk/~wmlh/ Mike (Prof. W.M.L.) Holcombe] 's web page at Sheffield University.

References


Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Stream of Passion — Stream of Passion …   Википедия

  • machine tool — machine tooled, adj. a power operated machine, as a lathe, used for general cutting and shaping of metal and other substances. [1860 65] * * * Stationary, power driven machine used to cut, shape, or form materials such as metal and wood. Machine… …   Universalium

  • Stream of Consciousness (álbum) — Stream of Consciousness Álbum de Vision Divine Publicación 2004 Género(s) Progressive metal Power metal Duración 1:01:40 D …   Wikipedia Español

  • Machine Age — is a term associated with the early 20th Century. Considered to be at a peak in the time between the first and second World Wars it forms a late part of the Industrial Age. It was ultimately eclipsed by the Atomic Age beginning in 1945.Artifacts… …   Wikipedia

  • machine gun — ☆ machine gun n. an automatic gun, usually mounted and with a cooling apparatus, firing a rapid and continuous stream of bullets machine gun vt. machine gunned, machine gunning …   English World dictionary

  • machine gun — machine′ gun n. mil a firearm capable of shooting a continuous stream of bullets • Etymology: 1865–70 ma•chine′ gun , v.t. gunned, gun•ning. ma•chine′ gun ner, n …   From formal English to slang

  • Machine pistol — This article is about full auto or burst capable pistols. For semi automatic weapons, see semi automatic pistol. A fully automatic Steyr M1912, which was used as a side arm by the Austro Hungarian Army A machine pistol is a handgun style,[1]… …   Wikipedia

  • Machine Empire — The Machine Empire is a group of robotic villains in the Power Rangers universe, who first appeared in the television show Power Rangers Zeo and were later mentioned in Power Rangers in Space and Power Rangers Wild Force. Contents 1 History 2… …   Wikipedia

  • Machine vision glossary — Common definitions related to the machine vision field.Compiled for application on the Society of Manufacturing Engineers interest area.General related fields *Machine vision *Computer vision *Image processing *Signal processing NOTOC 0 9*1394.… …   Wikipedia

  • Stream of Consciousness (album) — Infobox Album | Name = Stream of Consciousness Type = studio Artist = Vision Divine Released = 2004 Recorded = Genre = Progressive metal, power metal Length = 1:01:40 Label = Metal Blade Producer = Olaf Thorsen Oleg Smirnoff Last album = Send me… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”