====== Synthese eines Befehlssatz-Simulators für das Model-Checking von Software für eingebettete Systeme ======
~~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.

===== Ziel der Arbeit ===== 
Der bisherige manuelle Ansatz bei der Erweiterung von [mc]square um neue Plattformen funktioniert zwar, ist aber zu zeitaufwendig. Zur Beschleunigung der Entwicklung sollen stattdessen die Eigenschaften einer Hardware mittels einer Architektur-Beschreibungs-Sprache (ADL) beschrieben werden. Zu den Eigenschaften zählen etwa der Befehlssatz, die vorhandenen Speicher und die On-Chip-Peripherie. Aus dieser Beschreibung soll dann mittels zu erstellender Software-Werkzeuge der Plattform-Simulator erzeugt werden.

\\ Die Aufgaben im Detail:

  * Erweiterung einer gegebenen ADL
  * Anpassung einer gegebenen Beschreibung eines ATmega16-Mikrocontrollers
  * Erstellung von Software-Tools für die Verarbeitung der Hardware-Beschreibung
  * Erzeugung der Komponenten eines Simulators (Disassembler, Ressourcenmodell, Befehlsausführung, Interrupts)
  * Modellierung von Nichtdeterminismus

===== Studienrichtung =====

  * Informatik
  * Elektrotechnik

===== Vorkenntnisse =====

  * Java
  * Model-Checking

===== Bewerbungshinweise =====

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

===== Ansprechpartner =====

  * [[:lehrstuhl:mitarbeiter:gueckel]]

===== Status =====
Abgeschlossen

Student: Ivica Bogosavljevic