Das Ziel des Einsatzes von formalen Methoden im Software Engineering ist Techniken anzubieten, die die Entwicklung von hochzuverlässigen und sicherheitskritschen Systemen unterstützen. Zwei Schritte sind notwendig um dieses Ziel zu erreichen: Das Aufstellen einer präzisen, formalen Spezifikation von Systemanforderungen, und das Durchführen eines mathematischen Beweises (Verifikation), dass die Implementierung die Anforderungen der Spezifikation erfüllt. Formale Methoden bieten eine große Vielfalt an mathematisch präzisen Spezifikationssprachen, wie Logik höherer Stufe, algebraischen Spezifikationen, Abstrakte Zustandsmaschinen, die Z-Notation und temporale Logik. Diese Sprachen ermöglichen eine unzweideutige Beschreibung des Systemverhaltens, die die Basis für eine spätere Verifikation der Korrektheit des Systems bilden. Systemkorrektheit besteht aus verschiedenen Aspekten, die von funktionaler Korrektheit über Sicherheit (Safety und Security) bis zu Zuverlässigkeit reichen.

Mathematische Beweise für Sytemkorrektheit können mit verschiedenen Ansätzen konstruiert werden, u.a. durch interaktives Theorembeweisen, statische Codeanalyse, Model Checking und SMT-Beweisern.
Ein wichtiges Konzept, um die Komplexität großer Systeme und ihrer Beweise in den Griff zu bekommen ist Verfeinerung (Refinement). Damit wird eine modulare, schrittweise Entwicklung möglich, die mit einer abstrakten Spezifikation beginnt und mit korrektem Code endet. Wir arbeiten aktiv an der Weiterentwicklung von Techniken zur formalen Systementwicklung. Unsere Forschung konzentriert sich auf Verfeierung in Kombination mit Abstrakten Zustandsmaschinen und temporaler Logik. Unsere Gruppe entwickelt das KIV-System,     ein interaktives Beweisersystem. Wir wenden die Techniken auf verschiedene praktische Anwendungen an, wie zum Beispiel im VeriCAS-Projekt, das die Korrektheit nebenläufiger, lock-freier Algorithmen untersucht, oder im Flashix-Projekt, in dem ein verifiziertes Dateisystem für Flash-Speicher entwickelt wird.
Wir bieten unseren Vorlesung, Praktika und Seminare zu formalen Methoden und ihrer Anwendung im Software Engineering Prozess an.

1. Beweise für die funktionale Korrektheit von sicherheitskritschen Systemen (Safety und Security)

2. Beratung und Training für die Anwendung formaler Methoden zur Zertifizierung von Software nach den höchsten Sicherheitsstandards (Safety & Security, z.B. SIL, Common Criteria)