Formal Methods

Der Cluster 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. Dabei tragen wir zur Erforschung der wissenschaftlichen Grundlagen dieser Verfahren bei, indem wir uns insbesondere mit folgenden Bereichen intensiv auseinandersetzen:

  • Automatentheorie,
  • Semantik,
  • Logik,
  • Parallelismus,
  • Spieltheorie,
  • Computeralgebra und
  • Algorithmen- und Datenstrukturen.

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.

Unsere Ergebnisse und Werkzeuge kommen in unterschiedlichen Bereichen zum Einsatz, etwa in der Software für Autos und Flugzeuge, in Stromnetzen, autonomen Fahrzeugen und Robotersystemen.

Wissenschaftler

Exemplarische Projekte

Kontinuierliche Verifikation Hybrider Systeme (ConVeY)

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.

Mehr dazu

Verified Algorithm Analysis

Mehr dazu

Unifying Control and Verification of Cyber-Physical Systems (UnCoVerCPS)

Mehr dazu

CAVA: Computer Aided Verification of Automata

Mehr dazu

Statistical Unbounded Verification

Mehr dazu