Details

Autor(en) / Beteiligte

• Völlinger, Kim

Titel

Zertifizierende Verteilte Algorithmen

Ort / Verlag

ProQuest Dissertations & Theses

Erscheinungsjahr

2020

Quelle

ProQuest Dissertations & Theses A&I

Beschreibungen/Notizen

• Eine Herausforderung der Softwareentwicklung ist, die Korrektheit einer Software sicherzustellen. Testen bietet es keine mathematische Korrektheit. Formale Verifikation ist jedoch oft zu aufwändig. Laufzeitverifikation steht zwischen den beiden Methoden. Laufzeitverifikation beantwortet die Frage, ob ein Eingabe-Ausgabe-Paar korrekt ist. Ein zertifizierender Algorithmus überzeugt seinen Nutzer durch ein Korrektheitsargument zur Laufzeit. Dafür berechnet ein zertifizierender Algorithmus für eine Eingabe zusätzlich zur Ausgabe noch einen Zeugen – ein Korrektheitsargument. Jeder zertifizierende Algorithmus besitzt ein Zeugenprädikat: Ist dieses erfüllt für eine Eingabe, eine Ausgabe und einen Zeugen, so ist das Eingabe-Ausgabe-Paar korrekt. Ein simpler Algorithmus, der das Zeugenprädikat für den Nutzer entscheidet, ist ein Checker. Die Korrektheit des Checkers ist folglich notwendig für den Ansatz und die formale Instanzverifikation, bei der wir Checker verifizieren und einen maschinen-geprüften Beweis für die Korrektheit eines Eingabe-Ausgabe-Paars zur Laufzeit gewinnen. Zertifizierende sequentielle Algorithmen sind gut untersucht. Verteilte Algorithmen, die auf verteilten Systemen laufen, unterscheiden sich grundlegend von sequentiellen Algorithmen: die Ausgabe ist über das System verteilt oder der Algorithmus läuft fortwährend. Wir untersuchen zertifizierende verteilte Algorithmen. Unsere Forschungsfrage ist: Wie können wir das Konzept zertifizierender sequentieller Algorithmen so auf verteilte Algorithmen übertragen, dass wir einerseits nah am ursprünglichen Konzept bleiben und andererseits die Gegebenheiten verteilter Systeme berücksichtigen? Wir stellen eine Methode der Übertragung vor. Die beiden Ziele abwägend entwickeln wir eine Klasse zertifizierender verteilter Algorithmen, die verteilte Zeugen berechnen und verteilte Checker besitzen. Wir präsentieren Fallstudien, Entwurfsmuster und ein Framework zur formalen Instanzverifikation.