Model checking for early error detection

Detecting software design errors before you write the code

Long before starting to manufacture a new car, dozens of models – on paper, in clay, in differential equations and in wind tunnels – are constructed. The models are used to analyse and predict the new car’s properties, and to detect potential design errors. 

When designing software, using models is less common. Consequently, software design errors are often only detected during final testing, or worse, during usage when they are very costly to repair. 

However, errors can be detected at an early stage, even before the software is built, with the aid of model checking methods. The desired properties can be examined using model checking tools on an abstract model of the design.

The usefulness of these techniques has been demonstrated by checking several designs for critical properties. In a wireless sensor network it was shown that, in some topologies, synchronisation between network nodes – a desired property – can be lost. The worst case latency of a ‘Rapid I/O Packet Switch’ was verified to not exceed a desired value. And the task scheduling for a printer data path was proven to be deadlock free.

Model checking for early error detection

Method details


Method description

  1. Develop an abstract model of the software design’s behaviour
  2. Identify the design’s desired properties
  3. Check the properties using a model checker tool
  4. If not satisfied, adapt the design and the model, or add and modify properties and repeat the approach

Research projects

Partners

Industrial partners:

  • ASML
  • Chess
  • Océ

Academic partners:

  • Eindhoven University of Technology
  • Radboud University Nijmegen
  • University of Twente

Contact

Business manager:

Frans Beenker

Telephone:

+31 (0)88-866 5420

Email:

frans.beenker@tno.nl