direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Projekt VATES2

-- Fortsetzungsprojekt --

gefördert von der DFG

Verification and Transformation of Embedded Systems

Ziel des, von der DFG geförderten, VATES-Projekts ist die Entwicklung von Methoden zur Konstruktion und Verifikation eingebetteter Echtzeitsysteme. Eine besondere Herausforderung ist dabei nicht nur die Komplexität dieser Systeme, sondern auch die Beherrschung von Nebenläufigkeit und Echtzeitanforderungen. Herausragendes Merkmal des VATES-Projekts ist, dass wir die gesamte Entwicklungskette von Spezifikation und Quellcode bis zum von Compilern generierten ausführbaren Code betrachten. Um nachweislich korrekte Beweise zu führen und einen möglichst hohen Automatisierungsgrad zu erzielen, arbeiten wir mit maschineller Unterstützung, insbesondere mit Model Checking, SAT/SMT-Solvern und maschinellen Beweisern (wie dem interaktiven Theorembeweiser Isabelle/HOL).

In der ersten Phase des VATES-Projekts haben wir einen neuartigen Ansatz entwickelt, der es uns ermöglicht, eine abstrakte prozessalgebraische Spezifikation, formuliert in dem zeitbehaftetem Prozesskalkül Timed CSP, mit seiner Implementierung in einer Compiler-Zwischensprache formal in Beziehung zu setzen. Basierend darauf können wir Korrektheitseigenschaften in Timed CSP nachweisen und auf die Ebene des ausführbaren Codes übertragen.

In der nun angelaufenen zweiten Projektphase von VATES soll die entwickelte Methodik in zwei Richtungen erweitert werden: Zum einen soll dem zunehmend zu beobachtenden Einsatz von Multicore-Architekturen in eingebetteten Systemen Rechnung getragen werden und die entwickelte Methodik so erweitert werden, dass bereits auf Spezifikationsebene Direktiven für die Transformation in Multicore-Zielarchitekturen ausgedrückt und bei der Verifikation berücksichtigt werden können. Zum anderen soll die Methodik so erweitert werden, dass auch adaptive Systeme (die sich z.B. bei Veränderungen ihrer Umgebungen dynamisch umstrukturieren können, um weiterhin einsatzfähig zu sein) damit spezifiziert, verifiziert und in ausführbaren, semantisch äquivalenten Code transformiert werden können.


Als Fallstudie dient, wie bereits in der ersten Projektphase, das am Fraunhofer FIRST
(Berlin) entwickelte Echtzeitbetriebssystem BOSS für eingebettete Systeme. Es kommt unter anderem in Satelliten, medizinischen Anwendungen und einem elektronischen Lotto-System zum Einsatz. Weiterhin eignet es sich gut für Verifikationszwecke aufgrund seiner vergleichsweise einfachen Struktur und seiner relativ kleinen Größe. In dieser Projektphase soll BOSS bzgl. der Ausführbarkeit auf Multicore-Architekturen und um Mechanismen zur Unterstützung von Adaptivität erweitert werden. Darauf aufbauend können die zu entwickelnden Methoden an einer praxisrelevanten Fallstudie evaluiert werden.

Kooperationspartner

Projektbeteiligte

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe