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

===== 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 =====

[[:lehrstuhl:bewerbungshinweise|Hier]] finden sie Hinweise zu Bewerbungen.

===== Ansprechpartner =====

  * [[:lehrstuhl:mitarbeiter:gueckel]]

===== Status =====
In Bearbeitung

Student: Sebastian Wehlmann