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.

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

• Informatik
• Elektrotechnik

• Java
• Model-Checking

Hier finden sie Hinweise zu Bewerbungen.

• Dr. rer. nat. Dominique Marcel Gückel

Abgeschlossen

Student: Ivica Bogosavljevic