Aktuelle Forschung der Arbeitsgruppe Semantik und Verifikation paralleler Systeme

Unsere aktuellen Forschungsthemen

Die folgende Seite gibt Ihnen einen Überblick über unsere aktuellen Forschungsthemen. Die Ergebnisse unserer Forschung finden Sie in unserer Publikationsliste und detaillierte Informationen zu unseren Projekten finden Sie hier.

Inkrementelle Verifikation

Softwaresysteme verändern sich regelmäßig, weil Fehler eliminiert werden, neue Funktionalitäten hinzugefügt werden oder vorhandene Funktionalität angepasst werden muss. Nach jeder Änderung muss erneut verifiziert werden, ob sich das Softwaresystem gemäß der Anforderungen verhält. Anstatt nach einer Änderung die Verifikation vollständig neu zu starten, ist die Idee der inkrementellen Verifikation Informationen aus einer vorherigen Verifikation zu nutzen, um die Verifikation nach einer Softwareänderungen zu vereinfachen.

Im Teilprojekt L von Software-Factory 4.0 beschäftigen wir uns mit formalen Methoden zur effizienten Prüfung der funktionalen Äquivalenz zwischen sequentiellem und parallelisiertem Programm.

In Kooperation mit dem Lehrstuhl von Prof. Dirk Beyer untersuchen wir Methoden zur inkrementellen Verifikation, die nur geänderte Pfade verifizieren sollen. Dafür entwickeln wir Ansätze zur Identifikation von modifizierten Pfade. Das Wissen über die modifizierten Pfade wird anschließend genutzt, um die Verifikation auf die modifizierten Pfade zu fokussieren.

Kombination von Verifikationsverfahren

Verschiedene Verifikationsverfahren haben unterschiedliche Stärken und Schwächen und nicht immer ist ein einzelnes Verfahren ausreichend, um ein Programm zu verifizieren. Anstatt neue, stärkere Verfahren zu entwickeln, beschäftigen wir uns damit existierende Verfahren ohne großen Aufwand zu kombinieren.

Gemeinsam mit den Arbeitsgruppen von Prof. Dirk Beyer und Prof. Heike Wehrheim erforschen wir Methoden zur kooperativen Softwareverifikation. Wir untersuchen, welche Informationen wie zwischen Verifikationswerkzeugen ausgetauscht werden sollten, um eine erfolgreiche Kooperation zu ermöglichen, wie ausgetauschte Informationen für existierende Verifikationswerkzeuge aufbereitet werden müssen, damit sie diese verstehen, und wie in Kooperation gewonnene Informationen vereint dargestellt werden können. Unter anderem setzen wir dabei auf die Idee von Conditional Model Checking.

Mit dem Ansatz CoVeriTest erforschen wir weiterhin die Kombination von Verifizierern zum Zwecke der Testfallgenerierung.

Überprüfung von Verifikationsergebnissen

Resultate von Verifikationswerkzeugen sind nicht immer verlässlich. Implementierungsfehler, falsche Annahmen oder konzeptuelle Schwächen eines Verifikationsansatzes können dazu führen, dass ein Verifikationswerkzeug einen Fehler meldet, der im Programm nicht existiert, oder fälschlicherweise ein Programm mit Fehlern als fehlerfrei deklariert. Daher sollte man einem Ergebnis eines Verifikationswerkzeuges ohne weitere Erklärungen nicht trauen sondern bestenfalls die Erklärungen des Werkzeuges nutzen, um das Ergebnis mit einem unabhängigen Werkzeug zu überprüfen.

In der Vergangenheit haben wir uns vor allem mit Erklärungen und Überprüfungen für Ergebnisse von sequentiellen Programmen beschäftigt. Aktuell liegt unser Fokus auf der Prüfung von Ergebnissen für parallele Programme.