TU Berlin

Software and Embedded Systems EngineeringVATES - Verification and Transformation of Embedded Systems

SESE-Logo in blau

Inhalt des Dokuments

zur Navigation

Projekt VATES

gefördert von der DFG

Verification and Transformation of Embedded Systems

Ziel des Projekts 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.

Kooperationspartner

Projektbeteiligte

Leitung
Prof. Dr. Sabine Glesner
Wissenschaftliche Mitarbeiter
Björn Bartels
Thomas Göthel
Externe Mitarbeiter
Moritz Kleine


Navigation

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe