direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

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


Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe