Formal Methods
Das Forschungsgebiet "Formal Methods" entwickelt Methoden, Algorithmen und Werkzeuge zur präzisen Spezifikation, zur Entwicklung, Überprüfung und zum Testen von softwareintensiven Systemen. Softwareintensive Systeme sind solche, in denen ein wesentlicher Teil der Funktionalität mittels eingebetteter Software umgesetzt wird. Herausragende Beispiele sind mobile Systeme im Automobilbereich und in der Luftfahrt. Wir beschäftigen uns mit Verfahren zu Theorembeweisen, zum Durchsuchen des Zustandsraums – besonders zur Modellüberprüfung – zur abstrakten Interpretation und zum Testen.
Mitglieder
Jan Kretinsky, Prof. Dr. rer. nat.
Harald Räcke, Prof. Dr.
Forschung
Themenbereiche
Wir tragen zur Erforschung der wissenschaftlichen Grundlagen der oben genannten Verfahren bei, indem wir uns insbesondere mit folgenden Bereichen intensiv auseinandersetzen:
- Automatentheorie,
- Semantik,
- Logik,
- Parallelismus,
- Spieltheorie,
- Computeralgebra und
- Algorithmen- und Datenstrukturen.
Aktuelle Forschungsgebiete
Aktuelle Forschungsgebiete umfassen die Entwicklung von:
- Verifikationsverfahren für stochastische und hybride Systeme. Erstere spielen aktuell eine zentrale Rolle, wenn es etwa eine unsichere Umgebung oder auch Ausfallraten von Bauteilen bei der Verifikation zu berücksichtigen gilt. Letztere finden sich beispielweise in der Luft- und Raumfahrt, bei der Bahnregelung oder in der Chemietechnik. Hybride Systeme sind oft sicherheitskritisch und müssen deshalb formal analysiert werden.
- Spieltheoretischen Methoden für automatische Synthese. Hier werden mit Methoden der Automaten- und Spieltheorie automatisch korrekte Systeme aus ihrer formalen Verhaltensspezifikation generiert.
- Werkzeugen zur Programmanalyse für komplexe High-Level-Software. Dabei steht unter anderem die Entwicklung von Werkzeugen zur Analyse von C-Programmen für die Automobilindustrie im Mittelpunkt.
- Software- und Datensicherheit. Beispielsweise entwickeln wir ein sicheres System zur garantiert anonymen Bewertung wissenschaftlicher Artikel durch eine Gruppe von Gutachtern.
Exemplarische Projekte
Das Graduiertenkolleg ConVeY befasst sich mit dem Entwurf und der Analyse hybrider Systeme, d.h. von Software gesteuerter Systeme, die mit der physikalischen Welt interagieren und daher mit deren kontinuierlichem Verhalten umgehen müssen.