Implementierung eines Simulators für Renesas-Mikrocontroller

Motivation

| Am unserem Institut wurde und wird ein Model-Checker für Mikrocontroller-Code namens [mc]square entwickelt. [mc]square ist ein CTL-Model-Checker, der als Eingabe ein Assembler- oder C-Programm erwartet. Der Zustandsraum des Model-Checkers entsteht (vereinfacht ausgedrückt) durch die Ausführung des Programms durch einen Simulator für den jeweiligen Mikrocontroller. Derzeit verfügt [mc]square über Simulatoren für

  • Atmel ATmega16
  • Atmel ATmega128
  • Intel 8051
  • Infineon XC167

 |

Einige dieser Simulatoren sind das Ergebnis von Diplomarbeiten. Im Rahmen eines EU-Forschungsprojektes mit Beteiligung eines Industrieunternehmens, der VEMAC, soll nun [mc]square zur Verifikation eines auf einem Renesas R8C/Tiny basierenden Systems eingesetzt werden. Der dafür nötige Simulator ist im Rahmen dieser Diplomarbeit zu realisieren.

Aufgabenstellung

Implementierung eines Simulators für einen Renesas-Mikrocontroller. Bei dem Mikrocontroller handelt es sich um einen Renesas R8C/Tiny, voraussichtlich den R8C/Tiny \23. Der fertige Simulator sollte zumindest den Befehlssatz des Mikrocontrollers verarbeiten können. Weitere On-Chip-Peripherie ist wünschenswert, aber nicht unbedingtes Ziel.

Ziel der Arbeit

Implementierung des Simulators, Einsatz des Model-Checkers im Industrieprojekt.

Studienrichtung

Vorkenntnisse

Student

Ansprechpartner