Testing Links |
MOTIVE is a 3-year project sponsored by
with industrial collaborators
Information Processing Ltd,
The aim of MOTIVE is to adapt the successful X-Machine testing method,
previously developed at the University of Sheffield, to object-oriented
The original X-Machine method is based on a proven theory that
allows a tester to generate the necessary and sufficient test set for
a system which will guarantee specific correctness properties, once
testing is complete. The theory assumes that a software system can be
described as a finite state machine with a global memory store; and that
individual transitions are functions, triggered by user inputs. The
functions may read and write to memory when they are triggered.
Three major differences exist between this and the object-oriented view
of a system, in which:
In addition to this, there are specific object-oriented language
features, such as the nested composition of objects and inheritance
with polymorphism, which require special treatment.
- memory is distributed among encapsulated objects, rather than
global to the system;
- behaviour is triggered by message-passing (method invocation)
rather than by supplying inputs;
- computing the next state must sometimes be delayed until
after a transition has fired, rather than determined beforehand
from the state of memory.
In the course of the project, Sheffield has revised the formal model.
The object machine is a variant of the state machine which has
encapsulated memory, is triggered by message passing and allows both
pre- and post-condition guards on transitions, to determine the next
state. Coupled with this, an object algebra specifies the
exact behaviour of an object's methods.
To deal with inheritance and subtpying, a formal set of rules
for state machine and algebra refinement have been established, in order
to determine when one specification is a subtype of another (that
is, considering the total behaviour of an object, not just looking at
its type signatures). Machine refinement is described in terms of how
additional states and transitions should be introduced in subtype machines,
with restrictions on the kinds of elaboration allowed. Algebra refinement
is explained in terms of theory inclusion. From this, we have developed
new theories about regression testing and conformance relations between
components and plug-and-play interfaces. In particular, we can show
that regression testing using
JUnit, the popular Java testing tool,
tells you less useful information than
you might think. Also, we can show that conventional flow-based models
of testing are less good in their coverage and in what properties they
can actually guarantee.
Our continuing industrial partners have options to further develop the
testing tools prototyped in the MOTIVE project. In the finished tool,
developers are intended to create their designs using small state
machines for each object, from which the tool may generate a template
for statements that are asserted in the algebra. These statements are
in the form of equivalences that are used to create tests in the later
testing phase. The structure of the state machine guides how much
testing should be carried out, using similar coverage criteria as in
the X-Machine approach. However, it is the algebraic assertions which are
checked in the tests, such that we can guarantee the exact behaviour
of each method. The same integration proofs apply, such that when
testing is complete, we can say that the integrated system is correct,
under the assmption that the components are individually correct.
History and Publications
History of project to follow here.
The presentation given to the September 2002 FORTEST Workshop, in York,
gives a complete overview of the MOTIVE approach to testing:
A J H Simons, M P Stannett, K E Bogdanov
and W M L Holcombe,
"Method for Object Testing, Integration and Verification",
FORTEST Workshop on Testing, York, September 13, ed. R Hierons,
(York: FORTEST, 2002).
the context of the research in our group, the mathematical theory behind
the testing method, the conversion of the X-Machine model to Object Machines
and Object Algebra, the refinement rules for subtyping, and the test
Here are some links to other research in the area of object-oriented
testing and related approaches using statecharts.