Show simple item record

dc.contributor.advisorJohansen, Håvard D.
dc.contributor.authorLund, Jørgen Aarmo
dc.date.accessioned2019-06-27T12:01:39Z
dc.date.available2019-06-27T12:01:39Z
dc.date.issued2019-05-15
dc.description.abstractIn traditional software engineering methodologies, software correctness is established through testing and progressive fault mitigation. Safety properties are established by demonstrating that a sufficiently large number of test cases fail to violate them. In contrast, formal verification methods permit a systems design process where desired safety properties are stated outright in the system specification, and enforced by automated analysis tools. This is of particular interest in designing distributed systems, where safety properties may be easy to formally define and specify, yet hard to implement in practice. Despite this promise, the use of formal methods has largely been confined to academia and certain classes of safety-critical systems. Recently, however, companies like Amazon and Microsoft have adopted formal verification tools to verify distributed system designs. In this thesis, we present a formal specification of the Chord distributed hash table protocol, using the TLA+ specification language. We specify the protocol at a coarse level with a relaxed failure model, and then increase the granularity and introduce fail-stop failures, yielding a formal specification of Chord with asynchronous messaging and fault-tolerance mechanisms. We first model-check the specification under the constraint that no failures occur, and show that it satisfies critical safety properties. We then show that the introduction of failures leads the specification to admit several behaviors which break the safety properties Chord promises, potentially leading to permanent partitions in the network and performance degradation. As part of this work, we provide an overview of formal verification methods; we discuss certain formalisms and logics involved in modelling and proving algorithms, show potential advantages of applying formal methods to distributed systems design, and identify barriers keeping formal methods from widespread use.en_US
dc.identifier.urihttps://hdl.handle.net/10037/15613
dc.language.isoengen_US
dc.publisherUiT Norges arktiske universiteten_US
dc.publisherUiT The Arctic University of Norwayen_US
dc.rights.accessRightsopenAccessen_US
dc.rights.holderCopyright 2019 The Author(s)
dc.rights.urihttps://creativecommons.org/licenses/by-nc-sa/4.0en_US
dc.rightsAttribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0)en_US
dc.subject.courseIDINF-3990
dc.subjectVDP::Mathematics and natural science: 400::Information and communication science: 420::Theoretical computer science, programming languages and programming theory: 421en_US
dc.subjectVDP::Matematikk og Naturvitenskap: 400::Informasjons- og kommunikasjonsvitenskap: 420::Teoretisk databehandling, programmeringsspråk og -teori: 421en_US
dc.subjectVDP::Mathematics and natural science: 400::Information and communication science: 420::Communication and distributed systems: 423en_US
dc.subjectVDP::Matematikk og Naturvitenskap: 400::Informasjons- og kommunikasjonsvitenskap: 420::Kommunikasjon og distribuerte systemer: 423en_US
dc.subjectVDP::Mathematics and natural science: 400::Information and communication science: 420::System development and system design: 426en_US
dc.subjectVDP::Matematikk og Naturvitenskap: 400::Informasjons- og kommunikasjonsvitenskap: 420::Systemutvikling og – arbeid: 426en_US
dc.titleVerification of the Chord protocol in TLA+en_US
dc.typeMaster thesisen_US
dc.typeMastergradsoppgaveen_US


File(s) in this item

Thumbnail
Thumbnail
Thumbnail

This item appears in the following collection(s)

Show simple item record

Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0)
Except where otherwise noted, this item's license is described as Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0)