Stream X-Machine

Last updated

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.

Contents

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.

See also

Related Research Articles

Finite-state machine Mathematical model of computation

A finite-state machine (FSM) or finite-state automaton, finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time. The FSM can change from one state to another in response to some inputs; the change from one state to another is called a transition. An FSM is defined by a list of its states, its initial state, and the inputs that trigger each transition. Finite-state machines are of two types—deterministic finite-state machines and non-deterministic finite-state machines. A deterministic finite-state machine can be constructed equivalent to any non-deterministic one.

Software testing is an investigation conducted to provide stakeholders with information about the quality of the software 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 implementation. Test techniques include the process of executing a program or application with the intent of finding failures, and verifying that the software product is fit for use.

Phase-locked loop

A phase-locked loop or phase lock loop (PLL) is a control system that generates an output signal whose phase is related to the phase of an input signal. There are several different types; the simplest is an electronic circuit consisting of a variable frequency oscillator and a phase detector in a feedback loop. The oscillator generates a periodic signal, and the phase detector compares the phase of that signal with the phase of the input periodic signal, adjusting the oscillator to keep the phases matched.

State diagram diagram used in computer engineering and computer science

A state diagram is a type of diagram used in computer science and related fields to describe the behavior of systems. State diagrams require that the system described is composed of a finite number of states; sometimes, this is indeed the case, while at other times this is a reasonable abstraction. Many forms of state diagrams exist, which differ slightly and have different semantics.

The C programming language provides many standard library functions for file input and output. These functions make up the bulk of the C standard library header <stdio.h>. The functionality descends from a "portable I/O package" written by Mike Lesk at Bell Labs in the early 1970s, and officially became part of the Unix operating system in Version 7.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

In the theory of computation, a Mealy machine is a finite-state machine whose output values are determined both by its current state and the current inputs. This is in contrast to a Moore machine, whose (Moore) output values are determined solely by its current state. A Mealy machine is a deterministic finite-state transducer: for each state and input, at most one transition is possible.

In software project management, software testing, and software engineering, verification and validation (V&V) is the process of checking that a software system meets specifications and requirements so that it fulfills its intended purpose. It may also be referred to as software quality control. It is normally the responsibility of software testers as part of the software development lifecycle. In simple terms, software verification is: "Assuming we should build X, does our software achieve its goals without any bugs or gaps?" On the other hand, software validation is: "Was X what we should have built? Does X meet the high level requirements?"

In computing, dataflow is a broad concept, which has various meanings depending on the application and context. In the context of software architecture, data flow relates to stream processing or reactive programming.

The X-machine (XM) is a theoretical model of computation introduced by Samuel Eilenberg in 1974. The X in "X-machine" represents the fundamental data type on which the machine operates; for example, a machine that operates on databases would be a database-machine. The X-machine model is structurally the same as the finite-state machine, except that the symbols used to label the machine's transitions denote relations of type X→X. Crossing a transition is equivalent to applying the relation that labels it, and traversing a path in the machine corresponds to applying all the associated relations, one after the other.

A virtual finite-state machine (VFSM) is a finite-state machine (FSM) defined in a Virtual Environment. The VFSM concept provides a software specification method to describe the behaviour of a control system using assigned names of input control properties and output actions.

A data-flow diagram is a way of representing a flow of data through a process or a system. The DFD also provides information about the outputs and inputs of each entity and the process itself. A data-flow diagram has no control flow, there are no decision rules and no loops. Specific operations based on the data can be represented by a flowchart.

Specification and Description Language (SDL) is a specification language targeted at the unambiguous specification and description of the behaviour of reactive and distributed systems.

Stream processing is a computer programming paradigm, equivalent to dataflow programming, event stream processing, and reactive programming, that allows some applications to more easily exploit a limited form of parallel processing. Such applications can use multiple computational units, such as the floating point unit on a graphics processing unit or field-programmable gate arrays (FPGAs), without explicitly managing allocation, synchronization, or communication among those units.

Functional testing is a quality assurance (QA) process and 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 is conducted to evaluate the compliance of a system or component with specified functional requirements. Functional testing usually describes what the system does.

DEVS abbreviating Discrete Event System Specification is a modular and hierarchical formalism for modeling and analyzing general systems that can be discrete event systems which might be described by state transition tables, and continuous state systems which might be described by differential equations, and hybrid continuous state and discrete event systems. DEVS is a timed event system.

The (Stream) 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. Using this methodology, it is likely to identify a finite test-set that exhaustively determines whether the tested system's implementation matches its specification. This goal is achieved by a divide-and-conquer approach, in which the design is decomposed by refinement into a collection of Stream X-Machines, which are implemented as separate modules, then tested bottom-up. At each integration stage, the testing method guarantees that the tested components are correctly integrated.

Software testability is the degree to which a software artifact supports testing in a given test context. If the testability of the software artifact is high, then finding faults in the system by means of testing is easier.

Device driver synthesis and verification

Device drivers are programs which allow software or higher-level computer programs to interact with a hardware device. These software components act as a link between the devices and the operating systems, communicating with each of these systems and executing commands. They provide an abstraction layer for the software above and also mediate the communication between the operating system kernel and the devices below.

This glossary of computer science is a list of definitions of terms and concepts used in computer science, its sub-disciplines, and related fields, including terms relevant to software, data science, and computer programming.

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 Archived 2007-11-05 at the Wayback Machine
  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 Journal3(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 page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.