Show simple item record

2020-10-22Dissertation DOI: 10.18452/21978
Zertifizierende verteilte Algorithmen
dc.contributor.authorVöllinger, Kim
dc.date.accessioned2020-10-22T15:27:25Z
dc.date.available2020-10-22T15:27:25Z
dc.date.issued2020-10-22none
dc.identifier.urihttp://edoc.hu-berlin.de/18452/22745
dc.description.abstractEine 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.ger
dc.description.abstractA major problem in software engineering is to ensure the correctness of software. Testing offers no mathematical correctness. Formal verification is often too costly. Runtime verification stands between the two methods. Runtime verification answers the question whether an input-output pair is correct. A certifying algorithm convinces its user at runtime by offering a correctness argument. For each input, a certifying algorithm computes an output and additionally a witness. Each certifying algorithm has a witness predicate – a predicate with the property: being satisfied for an input, output and witness implies the input-output pair is correct. A simple algorithm deciding the witness predicate for the user is a checker. Hence, the checker’s correctness is crucial to the approach and motivates formal instance verification where we verify checkers and obtain machine-checked proofs for the correctness of an input-output pair at runtime. Certifying sequential algorithms are well-established. Distributed algorithms, designed to run on distributed systems, behave fundamentally different from sequential algorithms: their output is distributed over the system or they even run continuously. We investigate certifying distributed algorithms. Our research question is: How can we transfer the concept of certifying sequential algorithms to distributed algorithms such that we are in line with the original concept but also adapt to the conditions of distributed systems? In this thesis, we present a method to transfer the concept: Weighing up both sometimes conflicting goals, we develop a class of certifying distributed algorithms that compute distributed witnesses and have distributed checkers. We offer case studies, design patterns and a framework for formal instance verification. Additionally, we investigate other methods to transfer the concept of certifying algorithms to distributed algorithms.eng
dc.language.isogernone
dc.publisherHumboldt-Universität zu Berlin
dc.rights(CC BY 4.0) Attribution 4.0 Internationalger
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.subjectzertifizierende Algorithmenger
dc.subjectverteilte Algorithmenger
dc.subjectLaufzeitverifikationger
dc.subjectInstanzverifikationger
dc.subjectBeweisassistentger
dc.subjectCoqger
dc.subjectcertifying algortihmeng
dc.subjectdistributed algorithmeng
dc.subjectruntime verificationeng
dc.subjectinstance verificationeng
dc.subjectproof assistanteng
dc.subjectCoqeng
dc.subject.ddc000 Informatik, Informationswissenschaft, allgemeine Werkenone
dc.titleZertifizierende verteilte Algorithmennone
dc.typedoctoralThesis
dc.identifier.urnurn:nbn:de:kobv:11-110-18452/22745-3
dc.identifier.doihttp://dx.doi.org/10.18452/21978
dc.date.accepted2020-06-08
dc.contributor.refereeReisig, Wolfgang
dc.contributor.refereeMehlhorn, Kurt
dc.contributor.refereeSchlingloff, Holger
local.edoc.pages285none
local.edoc.type-nameDissertation
local.edoc.institutionMathematisch-Naturwissenschaftliche Fakultätnone
dc.relation.referenceshttps://doi.org/10.1007/978-3-319-67531-2_29
dc.relation.referenceshttps://doi.org/10.1007/978-3-319-22969-0_14
dc.relation.referenceshttps://doi.org/10.1007/978-3-319-57288-8_27
dc.relation.referenceshttps://doi.org/10.1007/978-3-319-92612-4_9
dc.relation.referenceshttps://doi.org/10.1007/978-3-030-31517-7_12
dc.relation.referenceshttps://doi.org/10.1007/978-3-030-21759-4_16

Show simple item record