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

?

?