?

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)