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:
Jeder dieser Simulatoren wurde manuell erstellt, einige davon im Rahmen von Abschlußarbeiten.
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:
Hier finden sie Hinweise zu Bewerbungen.
Abgeschlossen
Student: Ivica Bogosavljevic