Synthesis of hardware simulators for model checking


Dominique Marcel Gückel

Title Synthesis ofhardwaresimulatorsforusein model checking
When 30.10.2008
Where Lecture Room Informatik 7
Abstract [mc]square is a model checker for microcontroller assembly code. Given a program as a executable binary compiler output, and a CTL formula, it creates an over-approximation of possible program behavior and checks whether the behavior described by the formula can occur. This allows detection of errors that occur only under rare conditions, such as sequences of occurrences of interrupts mixed with regular program code execution. However, due to the assembly level approach, [mc]square is hardware-dependent. For each platform, it requires a simulator, which then executes the target program. Experience values show that the implementation of such a simulator for a new platform requires about six months, if performed by a single developer.

In this talk we present an approach to use hardware description languages for reducing the complexity of creating new simulators. We present related work from the area of simulator synthesis and show why these approaches are not appropriate for the use in model checking.

Slides download