Korrekte Übersetzung abstrakter Spezifikationen in C-Programme

• Antragsteller: Professor Dr. Wolfgang Reif
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme ; Theoretische Informatik
• Förderung: Förderung seit 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 503992399

Korrekte Übersetzung abstrakter Spezifikationen in C-Programme (VeriCode)Die verfeinerungsbasierte Entwicklung von Software ist eine der erfolgreichen Techniken zur Entwicklung verifizierter Software.Sie endet in der Regel mit imperativen Programmen (organisiert in Komponenten), sowie mit axiomatischen Beschreibungenvon Datenstrukturen und Funktionen in Prädikatenlogik. In vielen Projekten wurde diese Methodik bereits erfolgreich verwendet.Ein sehr umfangreiches eigenes Projekt ist das Flashix-Projekt, in dem wir ein Dateisystem für Flash-Speicher entwickelt und verifiziert haben.Spezifikationen und Programme verwenden die referenziell transparente Kopiersemantik der Prädikatenlogik, den wp-Kalkül für sequenzielle Programme, sowie einen Rely-Guarantee-Kalkül für nebenläufige Programme. Um aus derartigen Programmen ausführbaren Code zu erzeugen, werden von Beweisern typischerweise funktionale Programme mit nicht mutierbaren Datenstrukturen generiert.Der entstehende Code ist meist ineffizient, da destruktive Updates, wie sie für die effiziente Verwendung von z.Bsp. Arrays notwendig sind, im allgemeinen nicht korrekt sind. Auch die notwendige Garbage Collection ist in Betriebssystemkernen oder ealzeitanwendungennicht möglich. Diese verlangen Code, der den Speicher explizit verwaltet, z.Bsp. C-Code.Der Übergang von abstrakten referenziell transparenten Datenstrukturen zu effizientem destruktivem C-Code ist schwierig, da expliziteInformationen, wann Speicher deallokiert werden soll, und wann Updates überschreiben können, nicht vorliegen.Wir haben in Vorarbeiten einen Ansatz entwickelt, der so übersetzt, dass alle Datenstrukturen möglichst disjunkt gehalten werden, so dass destruktive updates möglich sind. Obwohl das zu einer wesentliche Verbesserung führt, ist der Code gegenüber dem geschriebenem Code immer noch ineffizient (ca. factor 10 depending on application). Eine Zuweisung x := y muss die in y gespeicherte Datenstruktur kopieren, um Disjunktheit zu erhalten. Diese Kopieroperationen können mit einer sorgfältigen Analyse häufig vermieden werden.Ziel dieses Projekts ist es, eine systematische Datenflussanalyse zu entwickeln, die eine optimale C-Code-Generierung mit einer minimalen Zahl an Kopieroperationen ermöglicht, so dass der generierte Code so effizient wie handgeschriebener Code ist. Dazu wollenwir ein Spezifikationsrahmen mit algebraischen Spezifikationen für abstrakte Datenypen und nebenläufige imperative Programme definieren. Wir wollen den Kern der Datenflussanalyse formalisieren und verifizieren, dass die Transformation für alle Ausgangsspezifikationen korrekt ist, und keine Speicherlecks entstehen.Um den Erfolg des Projektes zu dokumentieren, werden die Ergebnisse an mehreren Fallstudien evaluiert. Durch den abstrakten Spezifikationsrahmen ist das Projektergebnis für alle Verifikationssysteme nutzbar, und kann den praktischen Einsatz verifizierter Programme wesentlich verbessern.

• DFG-Verfahren: Sachbeihilfen