Verified Fiasco

Softwareverifikation bezeichnet die Untersuchung von Software mit mathematischen Methoden mit dem Ziel für ausgewählte Eigenschaften der Software einen mathematischen (das heißt, universell gültigen) Beweis zu finden. Softwareverifikation soll der Qualitätssicherung bei der Softwareentwicklung dienen. Softwareverifikation ist seit Beginn der Programmierung Forschungsgegenstand und wird derzeit in der Praxis kaum angewendet. Grund dafür ist hauptsächlich, dass eine Verifikation auch nur ausgewählter Eigenschaften um Größenordnungen teurer wäre als die Entwicklung der Software.

Zur Softwareverifikation gibt es verschiedene Ansätze. Prinzipiell werden die Programme zuerst in eine geeignete mathematische Theorie übersetzt. Das Resultat heißt Semantik. Man unterscheidet grob operationale, denotationelle und axiomatische Semantik. Im Vortag werden nach einer allgemeinen Einführung in Softwareverifikation diese drei Ansätze beispielhaft erläutert.

Der zweite Teil des Vortrages stellt den zur Zeit im VFiasco-Projekt entwickelten Ansatz zur Softwareverifikation vor. Fiasco ist ein an der TU-Dresden entwickeltes Mikrokernbetriebssystem für Echtzeit- und Sicherheitsanwendungen. Es ist auch möglich Linux (oder mehrere Instanzen von Linux) auf Fiasco zu booten und dann Linuxanwendungen neben direkt von Fiasco verwalteten Echtzeitanwendungen zu betreiben. Dabei garantiert Fiasco natürlich, dass die Echtzeitanwendungen weiterhin ihre garantierten Ressourcen erhalten. Fiasco ist fast komplett in C++ geschrieben.

Das VFiasco-Projekt stellt sich zum Ziel einige Eigenschaften des Fiasco-Mikrokerns zu verifizieren. Mit dem Ziel, den originalen C++ Quelltext zu verifizieren betritt das VFiasco-Projekt wissenschaftliches Neuland. Üblicherweise werden nur Programme in einer wohlgetypten funktionalen Programmiersprachen, wie zum Beispiel Haskell, verifiziert. Programme, die Sprungbefehlen (goto), Typecasts oder gar setjmp und longjmp enthalten, galten als nicht verifizierbar. Diese &quotschmutzigen" Programmidiome können allerdings bei der Programmierung eines Betriebsystemkern nicht vermieden werden. Im VFiasco-Projekt wurde deshalb eine C++ Semantik entwickelt, die diese &quotschmutzigen" Idiome auf elegante Weise behandelt. Der Vortrag erläutert die Semantik der C++ Befehle break, continue und goto.

Im dritten Teil des Vortrages wird eine Beispielverifikation eines kleinen Programmes durchgeführt.