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
Abstract: 
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
http://hdl.handle.net/20.500.12708/888
Library ID: AC11366275
ISBN: 9783319737218
Organisation: E191 - Institut für Computer Engineering 
Publication Type: Inproceedings
Konferenzbeitrag
Appears in Collections:Conference Paper

Files in this item:

Show full item record

Page view(s)

104
checked on Feb 26, 2021

Download(s)

194
checked on Feb 26, 2021

Google ScholarTM

Check


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