Das Institut arbeitet aktiv an neuen Techniken für die Systementwicklung mit Formalen Methoden. Unsere Forschung konzentriert sich auf Verfeinerung (Refinement) als grundlegende Methode zur modularen, schrittweisen top-down Entwicklung von Systemen beginnend mit einer abstrakten Spezifikation. Die Methodik für sequentielle Systeme basiert auf Abstrakten Zustandsmaschinen (Abstract State Machines).  Die Analyse nebenläufiger Systeme beruht auf der kompositionalen, temporalen Programmlogik "RGITL". Unsere Gruppe
bietet das von uns entwickelte KIV-System an, ein interaktives Beweisersystem, das die genannten Techniken unterstützt. Derzeit arbeiten wir am Flashix-Projekt, in dem ein verifiziertes, einsetzbares Dateisystem für Flashspeicher entwickelt wird.

Wissenschaftlicher Mitarbeiter
Institut für Software & Systems Engineering
  • Raum 3016 (Gebäude N)

Aktuelle Themen

Verfeinerung

Modulare, schritt-weise top-down Entwicklung von Systemen beginnend mit einer abstrakten Spezifikation

Temporale Logik

Analyse nebenläufiger Systeme basierend auf der kompositionalen, temporalen Programmlogik "RGITL"

Interaktives Theorembeweisen

Entwicklung und Anwendung von interaktiven Theorembeweiser-Systemen und -Techniken

 

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.

Tools & Projekte

KIV System

Ein interaktives Beweisersystem für die Systementwicklung mit Formalen Methoden

Flashix

Entwicklung und Verifikation eines State-of-the-Art Dateisystems für Flash-Speicher

Dienstleistungen

  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)

Abgeschlossene Projekte

VeriCAS

Verifikation von nebenläufigen, lock-freien Algorithmen

Go!Card

Formale Methoden für Secure Java Smart Cards

FORMOSA

Integrieren von Formalen Modellen und Safety Analyse

InopSys

Interoperabilität von Kalkülen zur System Modellierung

Protocure

Qualitätssicherung im Gesundheitswesen

Team

Wissenschaftlicher Mitarbeiter
Institut für Software & Systems Engineering
Wissenschaftlicher Mitarbeiter
Institut für Software & Systems Engineering
Institutsdirektor
Institut für Software & Systems Engineering

Institut für Software & Systems Engineering

Das Institut für Software & Systems Engineering, geleitet von Prof. Dr. Wolfgang Reif, ist eine wissenschaftliche Einrichtung in der Fakultät für Angewandte Informatik an der Universität Augsburg. Das Institut unterstützt sowohl Grundlagen- als auch angewandte Forschung in allen Bereichen der Software & Systems Engineering. In der Lehre ermöglicht es die weitere Entwicklung des relevanten Kursangebots von Fakultät und Universität.

Suche