Practical Model-Based Testing: A Tools Approach

by Mark Utting and Bruno Legeard, Morgan-Kaufmann 2006.

This web page contains model-based testing resources and examples for our book, Practical Model-Based Testing: A Tools Approach by Mark Utting and Bruno Legeard, Morgan-Kaufmann, 2007.

This web page provides downloads of some sample models for test generation, some free tools such as ModelJUnit and a list of commercial model-based testing tools. Here is an errata list of a few minor errors found in the book, and a selection of some of the figures and models used in the book (these are available for use in teaching courses from the book).

The MBT tools illustrated in the book include a Chinese Postman Algorithm by Harold Thimbleby, the ModelJUnit Java library developed by Mark Utting and others, the LTG/UML and LTG/B tools from Leirios Technologies (now, the Qtronic tool from Conformiq Software and the Spec Explorer tool from Microsoft Research.

The book contains these chapters:

  1. The Challenge; (What is MBT. An example.)
  2. The Pain and the Gain; (MBT compared to classic testing processes; experience reports, benefits, limitations)
  3. A Model of your System; (How to write good test models)
  4. Selecting your Tests; (Test selection criteria)
  5. Testing from Finite State Machines; (FSM and EFSM models)
  6. Testing from Pre/Post Models; (B and Spec# models)
  7. Testing from UML Models; (UML class diagram and state machine models)
  8. Making Tests Executable; (Adaptation versus Transformation)
  9. The GSM 11.11 Case Study; (A data-oriented model in B)
  10. The ATM Case Study; (A control-oriented model in UML)
  11. Putting it into Practice; (Prerequisites, selecting an approach, people, roles, training, MBT and agile methodologies, MBT and the Unified Process)

Here are several lists of MBT tools that you may find helpful:

Here is the Excel spreadsheet for the simple hypothetical simulation of the cost of testing discussed in Section 2.5 of the book. It compares the cost (in hours) of using various different testing processes to test ten releases of a software product.

Here is a link to the Chinese Postman Algorithm by Harold Thimbleby [Update 2015: this link seems to be broken, but his 2003 Software, Practice and Experience paper describes the Java algorithm in detail.] It contains his paper about the Chinese Postman algorithm plus the downloadable Java implementation that was used in Chapter 5 of the book to generate all-transition tours of the Qui-Donc model. (To apply this to your own FSM model, you must modify the main() method to define your own FSM graph.)

Here is some information about the ModelJUnit testing tool (see Sections 5.2 and 5.3 of the book). This is a Java library that allows you to write simple FSM or EFSM models as Java classes, then generate tests from those models and measure various model coverage metrics.

Lecture Slides

Here are a few PowerPoint slides that I have used while teaching material from this book. You are welcome to use and modify these slides for teaching purposes, so long as you acknowledge their source.

Last modified: Sat Oct 10 17:31:55 AEST 2015