Title: Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
Language: English
Authors: Aminof, Benjamin
Rubin, Sasha 
Stoilkovska, Ilina 
Widder, Josef
Zuleger, Florian
Keywords: parameterized model checking; fault tolerance; distributed algorithms; abstraction
Issue Date: 2018
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.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3417
Library ID: AC11366275
ISBN: 9783319737218
Organisation: E191 - Institut für Computer Engineering 
Publication Type: Inproceedings
Appears in Collections:Conference Paper

Files in this item:

Show full item record

Page view(s)

checked on Feb 26, 2021


checked on Feb 26, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.