Verisoft Repository

Im Verisoft-Projekt wird versucht, vier exemplarische Computersysteme, von denen drei aus dem industriellen Sektor stammen, formal durchgängig zu verifizieren. Die betrachteten Schichten dieser Systeme reichen von der Hardware auf Gatterebene über Systemsoftware bis zu kommunizierenden und verteilten Applikationen.

Das Verisoft Repository erlaubt die parallele Entwicklung der verschiedenen Einzelresultate, die zur Gesamtverifikation beitragen. Die Einzelresultate können mit Hilfe des Repositorys wohlkontrolliert verwaltet werden.

Im Repository werden die von den Projektpartnern entwickelten Artefakte als Module gesammelt und zueinander in Abhängigkeit gesetzt. Moduleinhalte können sowohl Dokumentation, formale Spezifikationen, Implementierung, Beweis und Werkzeuge für die Entwicklung und Verifikation sein.

Letztlich müssen die Inhalte des Repositorys in zweierlei Hinsicht in sich abgeschlossen sein: die Module, die für ein bestimmtes Computersystem betrachtet werden, müssen es erlauben

  • eine ausführbare Implementierung des Systems zu konstruieren und
  • die Top-Level Korrektheit des System nachzuweisen.

Momentan sind bereits wesentliche Teile der in Verisoft von den Projektpartner entwickelten Theorien und Systems in das Verisoft Repository integriert worden; das Repository wird von den Projektpartnern auch zur Weiterentwicklung benutzt.

Auf dieser Seite werden nach und nach Teile des internen Verisoft Repositorys, die hinreichend stabil sind und keine vertraulichen Daten der Industriepartner enthalten, veröffentlicht.

Veröffentlichungen

Bemerkung: die Theorien der unten angeführten Veröffentlichungen basieren meist auf der Version 2005 des interaktiven Theorembeweisers Isabelle. Bitte beachten Sie die Hinweise zur Isabelle-2005 Installation mit aktuellen Paketen von Poly/ML und ProofGeneral.

  • vlibolos-trunk-r31831.tar.gz (4.0M) — Durchgängige Verifikation eines Echtzeit-Computersystems (23 Dezember 2010)

    Diese Veröffentlichung enthält Beweise über das Echtzeit-Betriebssystem OLOS, das im Teilprojekt 6: Automotive entwickelt wurde. Die Features von OLOS umfassen ein zeitgesteuertes Scheduling, die Trennung von Applikationsprozessen, gepufferte Kommunikation und Treiber für den Automotive Bus Controller, mit dem verschiedene OLOS-Systeme miteinander kommunizieren können. OLOS-Applikationen kommunizieren mit Hilfe von Systemaufrufen, durch die Nachrichtenpuffer des Betriebssystems gelesen und beschrieben werden können. Genauer gesagt, umfasst die Veröffentlichung zwei Ergebnisse: Erstens enthält sie den Verfeinerungsbeweis der OLOS-Implementierung, der zeigt dass die Implementierung der formalen OLOS-Spezifikation genügt. Zweitens enthält sie die durchgängige Verifikation einer Programmbibliothek, die Benutzerprozessen ein Hochsprachen-Interface für die Systemaufrufe zur Verfügung stellt. Werden beide Ergebnisse kombiniert, lassen sich Eigenschaften, die auf dem abstrakten Programmiermodell der Hochsprache gezeigt wurden, auf die Implementierungsebene des Betriebssystems mit kompilierten Benutzerprozessen transferieren.

  • vlibvamos-trunk-r31570.tar.gz (5.2M) — Verifikationsergebnisse über die Korrektheit eines Mikrokerns und seiner Benutzerprozesse (1. September 2010)

    Diese Veröffentlichung enthält Beweise über den Mikrokern VAMOS und die Benutzerprozesse, die darauf laufen. Der Mikrokern VAMOS wurde für das Teilprojekt 2: Akademisches System entwickelt. Zwei Verfeinerungsbeweise stehen im Zentrum dieser Veröffentlichung: In einem ersten Schritt wird die Implementierung des Kerns mit einem abstrakten Spezifikationsmodell gekoppelt. In einem zweiten Schritt wird diese Kernspezifikation mit ihrem deterministischen Scheduler erneut abstrahiert zu einem nebenläufigen Prozesssystem mit nicht-deterministischem, aber temporal fairem Scheduling. Beide Ergebnisse zusammen bilden die formale Grundlage eines Verifikationsansatzes für systemnahe, nebenläufige C Programme.

  • volos-trunk-r29950.tar.gz (3.5M) — Implementierungskorrektheit des Echtzeitbetriebssystems OLOS (3. Dezember 2009)

    Diese Veröffentlichung beinhaltet die Code-Level-Verifikation des Echtzeitbetriebssystems OLOS, das im Teilprojekt 6: Automotive entwickelte und verwendet wird. Die Features von OLOS beinhalten Time-Triggered Scheduling, die Trennung von Applikationsprozessen, gepufferte Kommunikation, und Treiber für den Automotive Bus Controller, mit dem verschiedene OLOS-Systeme miteinander kommunizieren können. Die Kommunikation von OLOS-Applikationen wird über Systemaufrufe, die Nachrichtenpuffer des Betriebssystems lesen und schreiben, ermöglicht.

    Bemerkung: dieser Release ist auch Teil des neueren Releases vlibolos-trunk-r31831.tar.gz weiter oben.

  • vvamos-trunk-r28405.tar.gz (3.8M) — Fairness und Implementierungskorrektheit eines Mikrokern-Schedulers (16. Juni 2009)

    Diese Veröffentlichung beinhaltet zwei Verifikationsergebnisse für den Mikrokern VAMOS, die im Rahmen des Teilprojekt 2: Akademisches System entwickelt wurden. Bei dem ersten Ergebnis handelt es sich um einen Verfeinerungsbeweis für den VAMOS-Scheduler, der eine Simulationsbeziehung zwischen der Implementierung und einer abstrakten Spezifikation herstellt. Das zweite Ergebnis stützt sich auf diese abstrakte Spezifikation und beweist, dass der in VAMOS eingesetzte Scheduler temporale Fairness garantiert.

    Bemerkung: dieser Release ist auch Teil des neueren Releases vlibvamos-trunk-r31570.tar.gz weiter oben.

  • C0compilerCombined-trunk-r22114.tar.gz (5.7M) — Verifikation eines C0-Compilers (21. Februar 2008)

    Diese Veröffentlichung erweitert die Verifikation des C0 Compilers aus der vorherigen Veröffentlichung um einen Beweis, dass der generierte Assembler-Code das ursprüngliche C0 Programm simuliert, d.h. dass der generierte Code das gleiche Verhalten zeigt.
    Ebenfalls Bestandteil dieser Repository-Veröffentlichung sind ein Assembler und ein Simulator für die VAMP Architektur.

  • vc0compiler-trunk-r19956.tar.gz (4.0M) — Verifikation eines C0-Compilers auf Codeebene (19. Oktober 2007)

    Diese Veröffentlichung beinhaltet die Verifikation eines Compilers für die Sprache C0. C0 ist eine Untermenge von C und Hauptimplementierungssprache für Software in Verisoft. Der Compiler ist selbst in C0 implementiert. Die Verifikation des Compilers wird in einer Hoare-Logik-basierten interaktiven Software-Verifikationsumgebung für den Theorembeweiser Isabelle durchgeführt und zeigt, dass die Implementierung des Compilers den gleichen Assemblercode generiert wie die Isabelle Spezifikation der Codegenerierung. Die Korrektheit dieser Spezifikation wurde ebenfalls verifiziert; die entsprechenden Theorien sind aber in dieser Veröffentlichung noch nicht enthalten.
    Ebenfalls Bestandteil dieser Repository-Veröffentlichung sind eine formale Small-Steps-Semantik für C0 und eine formale Semantik für VAMP-Assembler, die Quell- und Zielsprachen des C0-Compilers.

    Bemerkung: dieser Release ist auch Teil des neueren Releases C0compilerCombined-trunk-r22114.tar.gz (5.7M) weiter oben.

  • vemail-trunk-r15868.tar.gz (3.6M) — Verifikation eines E-Mail-Clients auf Codeebene (18. Mai 2007)

    Diese Veröffentlichung beinhaltet die Verifikation des E-Mail-Clients aus Teilprojekt 2: Akademisches System relativ zu den Diensten, die vom einfachen Betriebssystem (SOS) bereitgestellt werden, und zu den Applikationen für Signieren und Versand der E-Mails. Die Implementierungssprache ist C0, eine Untermenge von C. Die Verifikation wird in einer Hoare-Logik-basierten interaktiven Software-Verifikationsumgebung für den Theorembeweiser Isabelle durchgeführt.

  • vString-4-r11594.tar.gz (1.8M) — Verifikation einer String-Bibliothek auf Codeebene (14. Dezember 2006)

    Diese Veröffentlichung beinhaltet die Verifikation einer Bibliothek für doppelt verkettete Listen und einer Bibliothek für Zeichenketten (Strings) auf der Codeebene. Die Implementierungssprache ist C0, eine Untermenge von C. Die Verifikation wird in einer Hoare-Logik-basierten interaktiven Software-Verifikationsumgebung für den Theorembeweiser Isabelle durchgeführt. Diese Software-Verifikationsumgebung ist ebenfalls in dem Paket enthalten.

    Bemerkung: dieser Release ist auch Teil des neueren Releases C0compilerCombined-trunk-r22114.tar.gz (5.7M) weiter oben.

 
Revision 14 Dec 2006