Inhalt des Dokuments
Stellenangebot
Stud. Mitarbeiter/in im Forschungsprojekt VATES (40h/Monat) gesucht
Projektbeschreibung :
Ziel des Projekts VATES (Verification and Transformation of Embedded Systems) ist die Entwicklung und Kombination von Grundlagen und Methoden zur Konstruktion und Verifikation eingebetteter reaktiver nebenläufiger echtzeitfähiger Software-Systeme. Derartige Systeme werden für die gesamte Kette von Spezifikation und Quellcode bis zum von Compilern generierten, ablauffähigen Maschinencode verifiziert. Die dabei anfallenden Verifikationsaufgaben werden mit maschineller Unterstützung, insbesondere durch Model Checking und den Einsatz maschineller Beweiser (wie dem interaktiven Theorembeweiser Isabelle/HOL) durchgeführt. Das eingebettete sicherheitskritische Echtzeit-Betriebssystem BOSS dient als Beispiel zum Praxistest der entwickelten Methoden.
Mögliche Aufgabengebiete:
- Entwicklung von formalen Spezifikationen zur Beschreibung von Komponenten von BOSS
- Führen von Korrektheitsbeweisen in Model Checkern (automatisch)
- Führen von Korrektheitsbeweisen im Theorembeweiser (interaktiv)
- Enwicklung von Transformationsvorschriften zwischen verschiedenen Absraktionsebenen und deren Implementierung
Voraussetzungen:
- Kenntnisse der formalen Logik (wie z.B. aus TheGI3)
- Interesse an der formalen Modellierung von Systemen
Bei Interesse wendet Euch an
Thomas GöthelE-Mail-Anfrage
Raum: TEL 1003
Telefon: 030 314-73451
