Synthesizing an Instruction Set Simulator for Model Checking Embedded Systems Software


A model checker for microcontroller assembly programs called [mc]square has been developed at the Chair of Computer Science 11. [mc]square is a CTL model checker which expects as input an assembly or a C program. It can automatically create the system model by simulating the execution of the examined program. Simulation is performed by a simulator for the target platform. Using this approach, it is possible to find even such errors that occur only under rare circumstances, such as sequences of interrupts that need to occur in a special order to show up a malfunction.

These are the platforms currently supported by [mc]square:

  • Atmel ATmega16
  • Atmel ATmega128
  • Infineon XC167
  • Intel 8051
  • Renesas R8C
  • Programmable Logic Controllers
  • Abstract State Machines

Each of these simulators has been created manually. Some are the result of diploma and master theses.


Even though the current approach of manually implementing simulators works, it is not optimal. Implementing simulators manually takes too much time. In order to accelerate development, hardware properties shall be described by means of an architecture description language. Hardware properties refers for instance to the instruction set, available memories and the on-chip peripherals. The simulator shall then be generated from this description by software generator tools. Implementing these generator tools is part of the task.

Field of Study

  • Computer Science
  • Electrical Engineering

Required knowledge

  • Java
  • Model-Checking

Hints for applications

Hints for applications.




Student: Ivica Bogosavljevic

This website uses cookies. By using the website, you agree with storing cookies on your computer. If you do not agree please leave the website.More information about cookies

RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany