Model Checking

Developing sound software for embedded systems is an error prone task and requires a lot of experience and knowledge abhout the target system. In fact even elaborate testing of small programs might not reveal problems that might occur during field operation. The involved costs and risks are often very high. In contrast, model checking (see here for a short informal introduction), allows for a qualified testimony for given properties. The problems that have to be addressed in this context are:

  1. the state space explosion problem - even for small programs we have to deal with several milion states
  2. the state space generation problem - the model must reflect the real-world system

In [RHKS2008] we have highlighted how even trivial programs for embedded systems might lead to unnoticed errors and how model checking can help uncovering during the development process before any software is deployed to the field environment.

Model Checking for Microcontrollers

In 2007 the Formal Verification Group of the DECS project established a cooperation with the Research Group Informatik XI at the Technical University of Aachen to address these problems.

The Research Group Informatik XI at the Technical University of Aachen has focused its research interests on software engineering for embedded systems. In 2005 the development of an explicit model checker was started by a team built up around Dr. Bastian Schlich to perform CTL-model checking for microcontroller specific software.

Their model-checker [mc]square is capable of model checking embedded software for the Atmel ATmega and the Infineon xC167 microcontroller families.

In order to enable formal verification with [mc]square for a wider range of targets, the Research Group Embedded Systems enhanced the possible target-capabilities of [mc]square by adding an MCS-51 (8051) simulator component. Adding support for MCS-51 based microcontrollers drastically increases the number of applications where [mc]square can be applied in order to formally verify embedded systems software.

For more details refer to our respective publications.