Synthesizing Simulators for Model Checking Microcontroller Assembly Code

Speaker

Dominique Gückel
Title Synthesizing Simulators for Model Checking Microcontroller Assembly Code
When 29.10.2009
Where Lecture Room Informatik 7
Abstract Model checking is recognized as a promising technique for the verification of embedded software. It can be applied to microcontroller software by simulating the behavior of the microcontroller during program execution. This approach allows for an automatic creation of the state space. The drawback, however, is that this approach always requires a simulator for the target platform, and if none is present, it has to be created first. Implementing new simulators manually can take years, depending on the complexity of the target platform and the desired accuracy of simulation. Hence it can be a very expensive process. In order to reduce the cost, we have developed a system which can automatically create the simulator from a description of the hardware. We present our new approach as well as a case study, in which we successfully applied the approach to the Atmel ATmega16 microcontroller.
Slides download