Fakultät Informatik

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

  • Prof. Matthias Althoff
  • Prof. Javier Esparza
  • Prof. Jan Kretinsky
  • Prof. Tobias Nipkow
  • Prof. Alexander Pretschner
  • Prof. Harald Räcke
  • Prof. Helmut Seidl
  • Prof. Lawrence Paulson

Exemplarische Projekte

Programm- und Modell-Analyse (PUMA)

Kooperation der Fakultät für Informatik, Technische Universität München, und der Fakultät für Informatik, Ludwig-Maximilians-Universität München, finanziert durch die Deutsche Forschungsgemeinschaft (DFG)

Das Graduiertenkolleg PUMA vereint die vier zentralen Ansätze zur Analyse von Programmen und Modellen, nämlich Typsysteme, Theorembeweise, Model Checking und Abstrakte Interpretation. Ziel von PUMA ist die Entwicklung neuer Analysen im Schnittpunkt dieser Methoden. Die Analysen werden prototypisch implementiert und auf der Basis von ausgewählten Problemen aus dem Bereich softwareintensiver Systeme bewertet. 

Die Förderung von PUMA begann im Juli 2008. Im Sommer 2012 genehmigte die DFG eine zweite Förderperiode, die im Januar 2013 startete.

 Mehr dazu

Verified Algorithm Analysis

 Mehr dazu

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

 Mehr dazu