Zertifizierende Algorithmen für interaktive Komponenten und verteilte Systeme

Dieses Projekt wird für die drei Jahre 2015 bis 2017 durch die Deutsche Forschungsgemeinschaft (DFG) finanziert.

Kurzbeschreibung des Projekts

Ein zertifizierender Algorithmus produziert bei jeder Berechnung zusätzlich zum Resultat noch einen Zeugen, der die Korrektheit des Resultats zeigt. Im besten Fall ist der Zeuge unmittelbar verständlich. Andernfalls überprüft ein (vergleichsweise einfacher) Checker-Algorithmus den Zeugen. Seit den 2000er Jahren werden für zahlreiche „klassische“ Algorithmen zertifizierende Varianten entwickelt. Beispielsweise enthält die LEDA-Bibliothek des MPI Saarbrücken zahlreiche zertifizierende Algorithmen.

Rechnerintegrierte Systeme sind heutzutage oft aus interaktiven Komponenten aufgebaut, die als Knoten eines verteilten Systems lose gekoppelt miteinander interagieren. Algorithmen für interaktive Komponenten terminieren im Allgemeinen nicht. Weiterhin kennen die Komponenten eines verteilten Systems meist nicht die vollständige Struktur des Systems. Algorithmen für solche Komponenten und Systeme verhalten sich entsprechend prinzipiell anders als klassische Algorithmen.

In diesem Projekt wird untersucht, wie weit die Idee der Zertifizierung bei Algorithmen für interaktive Komponenten und verteilte Systeme trägt. Das ist deshalb besonders interessant, weil interaktive Komponenten und verteilte Systeme viel schwerer zu implementieren sind als klassische Algorithmen.

Dieses Ziel wird von mehreren Seiten her zugleich angestrebt. Dazu werden entsprechende Fallstudien ausgearbeitet. Wir gehen von den bekannten zertifizierenden Algorithmen für Datenstrukturen aus und versuchen, die dabei verwendeten Konstruktionsverfahren für Zeugen und deren Checker auf allgemeine interaktive Komponenten zu übertragen. Dazu gehört insbesondere die Idee, dass der Algorithmus als Zeuge einen Datenstrom produziert, den der Checker zeitlich versetzt, aber nebenläufig prüft.

Algorithmen für verteilte Systeme bestehen oft aus Algorithmen für interaktive Komponenten. Interessant ist deshalb die Frage nach der Komponierbarkeit zertifizierender Komponenten zu einem zertifizierenden System.

Ein Netzwerk aus Rechnerknoten und Kommunikationskanälen ist ein spezielles verteiltes System. Für solche Netzwerke gibt es zahlreiche bekannte Algorithmen. So zum Beispiel Kommunikationsprotokolle, die ein mögliches Fehlverhalten der Kommunikationskanäle ausgleichen. Das wirft die interessante Frage auf, ob solche Protokolle auf spezielle Weise zertifizierend gestaltet werden können.

In einem Netzwerk kann jeder Knoten nur mit seinen unmittelbaren Nachbarn kommunizieren. Das reicht, um globale Konstrukte des Netzwerks zu bilden und zu nutzen (beispielsweise einen virtuellen spannenden Baum). Dafür gibt es bereits geeignete Algorithmen; diese sollen nun zertifizierend ergänzt werden. Interessant ist es auch, bekannte zertifizierende Algorithmen auf Graphen zu Algorithmen auf den Knoten eines Netzwerks umzugestalten, zusammen mit den Zeugen und deren Checkern.

Vorträge

  • Was heißt "Korrektheit"?, Wolfgang Reisig, Vortrag, 11.3.2015, Workshop Modellierung, Gesellschaft für Informatik, Hamburg, 11.-13. März 2015

Publikationen