Synthesizing an Instruction Set Simulator for Model Checking Embedded Systems Software

Motivation

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.

Goal

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.

Tutor

Status

Finished

Student: Ivica Bogosavljevic


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