University of Sheffield

MOTIVE: Method for Object Testing, Integration and Verification

Motive Cogwheels

Related project sites:

down to buttons

Department of Computer Science Motive Project Verification and Testing Research Group Extramural Interests
Description | Publications | Downloads | Testing Links |

Project Description

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

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.

Project Downloads

The presentation given to the September 2002 FORTEST Workshop, in York, gives a complete overview of the MOTIVE approach to testing:

It describes 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 generation method.

Testing Links

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

  • FORTEST: Network for Formal Methods and Testing
  • Object-Oriented Testing: The Internet Repository
  • Dr. Mike Stannett's Research Pages
  • Dr. Kirill Bogdanov's Research Pages
  • Prof. Mike Holcombe's Research Pages
  • Prof. John D McGregor's Research and Testing Pages
  • Robert Binder and RBSC Corporation
  • Erich Gamma and Kent Beck's JUnit Website
  • Information Processing Ltd, Bath: Cantata++ Testing Tool
  • Information Processing Ltd, Bath: AdaTEST 95 Testing Tool
    Home Page [here] Research Teaching Publications Consultancy Latest News Back: Poppy Up: Research Forth: Brunel
    up to the top
    Visit: | Home | Contact | Biography | Research | Teach | Publish | Consult | Interest | Links | News |

    © 2000, Anthony J H Simons, The Department of Computer Science, University of Sheffield.
    This page maintained by Anthony J H Simons.   Last modified 28 March 2003.