ReVeriX: Effiziente Reverifikation geänderter Programme trotz Wechsels des Verifikationsansatzes

• Antragstellerin: Professorin Dr. Marie-Christine Jakobs
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung seit 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 496852682

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.

• DFG-Verfahren: Sachbeihilfen