Werkzeuggestützte Implementierung eines Simulators für Renesas R8C/Tiny-Mikrocontroller zur Erweiterung des Model-Checkers [mc]square

Motivation

Am Lehrstuhl Informatik 11 wurde ein Model-Checker für Mikrocontroller-Programme 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 Simulation der Ausführung des untersuchten Programms in einem Simulator. Der Simulator modelliert das Verhalten des jeweiligen Ziel-Mikrocontrollers. Dementsprechend ist keine manuelle Modellierung erforderlich. Mit diesem Ansatz lassen sich auch Fehler finden, die in hochgradig seltenen Szenarien auftreten, beispielsweise bestimmte Reihenfolgen von Interrupts.

Bislang unterstützt [mc]square die folgenden Plattformen:

  • Atmel ATmega16
  • Atmel ATmega128
  • Infineon XC167
  • Intel 8051
  • Renesas R8C
  • Speicherprogrammierbare Steuerungen
  • Abstract State Machines

Jeder dieser Simulatoren wurde manuell erstellt, einige davon im Rahmen von Abschlußarbeiten. Die manuelle Erstellung von Simulatoren ist aber zu zeitaufwendig. Daher wurde in einer vorhergehenden Masterarbeit ein Werkzeug geschaffen, mit dem sich Simulatoren aus einer Hardwarebeschreibung automatisch erzeugen lassen. Die zugehörige Beschreibungssprache wurde ebenfalls am I11 entwickelt und heißt SGDL. Beschrieben werden etwa der Befehlssatz, die vorhandenen Speicher und die On-Chip-Peripherie. Bislang wurden damit erfolgreich Simulatoren für Atmel ATmega16 und Intel MCS-51 erstellt. Obwohl vom Aufbau her deutlich unterschiedlich, sind beides 8-Bit-Architekturen.

Ziel der Arbeit

Mit dem bestehenden Werkzeug soll nun ein 16-Bit-Mikrocontroller beschrieben werden. Gegebenenfalls ist das Werkzeug anzupassen. Die Arbeit soll zeigen, daß sich mit SGDL und dem zugehörigen Synthesesystem auch 16-Bit-Architekturen beschreiben lassen. Zweites Ziel ist der Nachweis, daß die Implementierung mit Werkzeugunterstützung schneller möglich ist als die manuelle, insbesondere auch für einen vorher nicht mit der Technik vertrauten Entwickler.

Studienrichtung

  • Informatik (Bachelor)
  • Informatik (Diplom/Master/Software Systems Engineering) (dazu würde das Thema erweitert, um den nötigen Umfang zu erreichen)
  • Elektrotechnik

Vorkenntnisse

  • Java
  • Model-Checking (nicht zwingend, aber hilfreich)

Bewerbungshinweise

Hier finden sie Hinweise zu Bewerbungen.

Ansprechpartner

Status

In Bearbeitung

Student: Sebastian Wehlmann

Diese Website verwendet Cookies. Durch die Nutzung der Website stimmen Sie dem Speichern von Cookies auf Ihrem Computer zu. Wenn Sie nicht einverstanden sind, verlassen Sie bitte die Website.Weitere Information

RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland