Die verfeinerungsbasierte Entwicklung von Software ist eine der erfolgreichen Techniken zur Entwicklung verifizierter Software. Sie endet typischerweise mit imperativen Programmen (organisiert in Komponenten), sowie mit axiomatischen Beschreibungen von 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.B. Arrays notwendig sind, im allgemeinen nicht korrekt sind. Auch die notwendige Garbage Collection ist in Betriebssystemkernen oder Realzeitanwendungen nicht möglich. Diese verlangen Code, der den Speicher explizit verwaltet, z.B. C-Code.

Der Übergang von abstrakten referenziell transparenten Datenstrukturen zu effizientem destruktivem C-Code ist schwierig, da explizite Informationen, 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, sodass destruktive Updates möglich sind. Obwohl das zu einer wesentliche Verbesserung führt, ist der Code gegenüber handgeschriebenem Code immer noch ineffizient. 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, sodass der generierte Code so effizient wie handgeschriebener Code ist. Dazu wollen wir eine Spezifikationssprache mit algebraischen Spezifikationen für abstrakte Datentypen 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.

Partners

Funded by