Go to page
 

Bibliographic Metadata

Title
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
AuthorAminof, Benjamin ; Rubin, Sasha ; Stoilkovska, Ilina ; Widder, Josef ; Zuleger, Florian
Published in
Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings / Dillig, Isil; Palsberg, Jens, Cham, 2018, page 1-24
Published2018
Edition
Accepted version
LanguageEnglish
SeriesLecture Notes in Computer Science ; 10747
Document typeArticle in a collected edition
Keywords (EN)parameterized model checking / fault tolerance / distributed algorithms / abstraction
Project-/ReportnumberAustrian Science Fund (FWF): S11403
Project-/ReportnumberAustrian Science Fund (FWF): S11405
Project-/ReportnumberAustrian Science Fund (FWF): P27722
Project-/ReportnumberAustrian Science Fund (FWF): W1255-N23
Project-/ReportnumberVienna Science and Technology Fund (WWTF): ICT12-059
ISBN9783319737218
URNurn:nbn:at:at-ubtuw:3-3417 Persistent Identifier (URN)
DOI10.1007/978-3-319-73721-8_1 
Restriction-Information
 The work is publicly available
Files
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction [0.52 mb]
Links
Reference
Classification
Abstract (English)

Parameterized verification of fault-tolerant distributed algorithms has recently gained more and more attention. Most of the existing work considers asynchronous distributed systems (interleaving semantics). However, there exists a considerable distributed computing literature on synchronous fault-tolerant distributed algorithms: conceptually, all processes proceed in lock-step rounds, that is, synchronized steps of all (correct) processes bring the system into the next state.

We introduce an abstraction technique for synchronous fault-tolerant distributed algorithms that reduces parameterized verification of synchronous fault-tolerant distributed algorithms to finite-state model checking of an abstract system. Using the TLC model checker, we automatically verified several algorithms from the literature, some of which were not automatically verified before. Our benchmarks include fault-tolerant algorithms that solve atomic commitment, 2-set agreement, and consensus.

Note
Stats
The PDF-Document has been downloaded 45 times.