<div class="csl-bib-body">
<div class="csl-entry">Stoilkovska, I. (2021). <i>Modeling and verification of synchronous fault-tolerant distributed algorithms</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.90331</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2021.90331
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/17261
-
dc.description.abstract
Distributed systems have a wide range of applications: from autonomous vehicles, via data centers, to cryptocurrencies. A distributed system consists of multiple processes, which execute an algorithm locally and coordinate globally in order to reach a common goal. During the lifetime of a distributed system, some of its processes can exhibit faulty behaviors, whose severity and occurrence are unpredictable. To ensure that the system works correctly when some of its processes are faulty, distributed algorithms are designed to be fault-tolerant. Design of fault-tolerant distributed algorithms has been an active field in the area of theoretical computer science for over 40 years. As these algorithms are implemented in systems where a high degree of availability and reliability is expected, their correctness, as well as the correctness of their implementations, is paramount. The design and implementation of fault-tolerant distributed algorithms are led by algorithm designers and by software engineers, respectively. Both tasks are quite challenging, and thus susceptible to human error. Automated verification provides means for finding bugs at early stages in the process of designing and implementing correct fault-tolerant distributed algorithms. However, several characteristics, inherent to distributed systems, represent obstacles for the direct application of automated verification techniques. Moreover, fault-tolerant distributed algorithms are parameterized, in the sense that their execution is influenced by a set of parameters, whose values are a priori unknown, such as, e.g., the number n of processes. Thus, reasoning about the correctness of such an algorithm amounts to reasoning about the correctness of infinitely many finite instances of the algorithm. In the formal methods literature, this problem is called the parameterized verification problem, and is undecidable in general. In this thesis, we propose methods for formal specification and techniques for automated verification of fault-tolerant distributed algorithms. We focus on synchronous algorithms, whose computations are organized in rounds, in which the processes execute the algorithm synchronously. To solve the parameterized verification problem, we (i) propose formal models for the behavior of a process running a synchronous fault-tolerant distributed algorithm, (ii) define techniques for reducing certain instances of the parameterized verification problem for synchronous fault-tolerant distributed algorithms to some decidable problem, and (iii) show the usefulness our techniques by experimental evaluation, i.e., by automatically verifying several synchronous fault-tolerant distributed algorithms from the literature.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Distributed algorithms
en
dc.subject
Fault tolerance
en
dc.subject
Modeling
en
dc.subject
Model checking
en
dc.subject
Abstraction
en
dc.subject
Threshold automata
en
dc.title
Modeling and verification of synchronous fault-tolerant distributed algorithms
en
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2021.90331
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Ilina Stoilkovska
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Widder, Josef
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Doctoral
-
dc.identifier.libraryid
AC16190798
-
dc.description.numberOfPages
217
-
dc.thesistype
Dissertation
de
dc.thesistype
Dissertation
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
item.languageiso639-1
en
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_db06
-
item.fulltext
with Fulltext
-
item.openairetype
doctoral thesis
-
item.grantfulltext
open
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems