Laufende Projekte
ReVeriX: Effiziente Reverifikation geänderter Programme trotz Wechsels des Verifikationsansatzes (DFG Sachbeihilfe)
Softwareverifikation dient dazu Software gegen Verletzungen von Eigenschaften oder Spezifikationen abzusichern und insbesondere nachzuweisen, dass in einem Programm keine Verletzungen auftreten können. Da jede Softwareänderung neue Verletzungen einführen kann, muss man jede geänderte Softwareversion reverifizieren, um sie zuverlässig gegen Verletzungen von Eigenschaften oder Spezifikationen abzusichern. Eine naive Verifikation der geänderten Software kann mit der Vielzahl an Änderungen in langlebigen und fortlaufend weiterentwickelten Softwareprojekten nicht Schritt halten. Daher gibt es heutzutage eine Vielzahl an Techniken, die die Reverifikation für einen spezifischen Verifikationsansatz effizienter machen. Eine Beschränkung der Reverifikation auf einen spezifischen Verifikationsansatz ist aus mehreren Gründen nicht wünschenswert. Zum einen kann sich während der langen Lebenszeit von Software die verfügbare Verifikationstechnologie gravierend ändern, sodass ein Austausch des Verifikationsansatzes notwendig wird. Zum anderen verwenden viele Verifikationswerkzeuge heutzutage mehr als einen Verifikationsansatz. Das Ziel dieses Projekts ist es daher die Möglichkeiten zur effizienten Reverifikation bei Änderungen des Verifikationsansatzes zu erhöhen. Um eine effizienten Reverifikation insbesondere bei Änderungen des Verifikationsansatzes zu erreichen, benötigt man (1) Möglichkeiten zur Weitergabe von Informationen an andere Verifikationsansätzen, die es diesen erlauben effizient zu reverifizieren, oder (2) Reverifikationstechniken, die von Anfang unabhängig von dem genutzten Verifikationsansatz sind. Die Zielsetzung des Projektes ist für Sicherheitseigenschaften (Safety) von Software zu untersuchen, in wieweit eine effizienten Reverifikation bei Änderungen des Verifikationsansatzes erreicht werden kann, wenn man (1) Informationen zwischen dem vorherigen und dem jetzigen Verifikationsansatz austauscht oder (2) die Reverifikation unabhängig vom Verifikationsansatz auf relevante, modifizierte Pfade beschränkt.
Abgeschlossene Projekte
Software-basierte Systeme spielen eine wichtige Rolle in der heutigen Wirtschaft und Gesellschaft. Gleichzeitig werden existierende Systeme laufend mit neuen Anforderungen und veränderten, technischen Rahmenbedingungen konfrontiert. Um diesen Herausforderungen zu begegnen, werden im LOEWE-Schwerpunkts Software-Factory 4.0 innovative Konzepte, Methoden und Werkzeuge entwickelt, die ein weitgehend automatisiertes Reengineering von Software unterstützen sollen. Drei Ziele stehen im Fokus der Forschung von Software-Factory 4.0: die Flexibilisierung spezialisierter Softwaresysteme, die Parallelisierung existierender Software und die Vereinfachung des Reengineerings.
Die Arbeitsgruppe Semantik und Verifikation paralleler Systeme ist mit Teilprojekt L an Software-Factory 4.0 beteiligt. Teilprojekt L beschäftigt sich mit der Absicherung der funktionalen Korrektheit des parallelisierten Programms. Konkret beschäftigt es sich mit der Fragestellung der funktionalen Äquivalenz zwischen sequentiellem und parallelisiertem Programm zu prüfen.
Der LOEWE-Schwerpunkt Software-Factory 4.0 ist ein 4-jähriges Projekt, das vom Bundesland Hessen finanziert wird.