Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen angezeigt.


—lehre:abschlussarbeiten:synthesizing_is_simulators_for_model_checking_es_software [2024/10/30 03:13] (aktuell) – angelegt - Externe Bearbeitung 127.0.0.1
Zeile 1: Zeile 1:
 +====== 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