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 .

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.

Außerdem entwickeln wir Verfahren, welche die Informationen, die ein Verifizierer während oder nach der Verifikation eines Programms bereitstellt, für die Verifikation des modifizierten Programms mit einem anderen Verifizierer nutzen.

Testen ist eine weit verbreitete Methode der Softwarequalitätssicherung. Häufig werden automatische Methoden eingesetzt, um Tests zu generieren. Wie auch wir setzt eine Vielzahl von automatischen Testgenerierungsmethoden auf Verifikation. Auf Verifikation beruhende Verfahren prüfen die Erreichbarkeit von Testzielen und geben einen Test pro erreichbarem Testziel aus.

Um eine effizientere und effektivere Testfallgenerierung auf Basis von Verifizierern zu erreichen, setzen wir in unserer Forschung zum Beispiel auf die Kombination von verschiedenen Verifikationsansätzen, wie in unserem Testansatz CoVeriTest, der kooperative Kombinationen nutzt und erfolgreich an der International Competition on Software Testing teilnimmt.

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.

Runtime Monitoring ist eine weit verbreitete Methode, um dafür zu sorgen, dass eine Programmausführung gewisse Eigenschaften einhält. Zu diesem Zweck beobachtet ein Monitor die Programmausführung und greift ein, wenn eine Eigenschaftsverletzung droht. Während die Beobachtung einer einzelnen Ausführung die Analyse vereinfacht und die Laufzeitinformationen die Analyse sogar präziser werden lässt, verursacht der Monitor Zusatzkosten wie zusätzliche Laufzeit. Diese Zusatzkosten können so hoch sein, dass das Monitoring impraktikabel wird. Das Ziel von Optimierungen von Runtime Monitoring ist diese Zusatzkosten zu reduzieren, sodass sie tolerierbar werden.

Zusammen mit der Arbeitsgruppe von Prof. Dr. Heiko Mantel studieren wir Verfahren zur Optimierung von Runtime Monitoring, um diese in einem einheitlichen Framework zu beschreiben und zu analysieren. Ein wichtiger Aspekt ist, dass wir formal beweisen, dass die Optimierung gewisse Eigenschaften von Runtime Monitoring wie Soundness erhalten. Neben der experimentellen Evaluation der Verfahren beschäftigen wir uns auch mit der analytischen Evaluation der Zusatzkosten von Runtime Monitoring.

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.