MOTIVE: Method for Object Testing, Integration and Verification

Related project sites:

• Verification and Testing: MOTIVE Project Archive
• Object-Oriented Testing: The Internet Repository
• Dr. Mike Stannett's MOTIVE Research Pages
• FORTEST: Network for Formal Methods and Testing

MOTIVE is a 3-year project sponsored by EPSRC GR/M56777 with industrial collaborators currently including Information Processing Ltd, Genesys Solutions and NoiseFactory. The aim of MOTIVE is to adapt the successful X-Machine testing method, previously developed at the University of Sheffield, to object-oriented software systems.

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:

• 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.

• MOTIVE Research Publications, the official list of generated publications
• MOTIVE Research Pages, a local repository by the project RA

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).
conference: abstract, powerpoint.

Here are some links to other research in the area of object-oriented testing and related approaches using statecharts.