Paper Info
Title
Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction
Abstract
We introduce an automated method for parameterized verification of fault-tolerant distribed algorithms. It rests on a novel parametric interval abstraction (PIA) technique, which works for systems with multiple parameters, for instance, where n and t are parameters describing the system size and the bound on the number of faulty processes, respectively. The PIA technique allows to map typical threshold-range intervals like [1,t+1) and [t+1,n-t) to values from a finite abstract domain. Applying PIA to both the local states of the processes and the global system state, the parameterized verification problem can be reduced to finite-state model checking. We demonstrate the practical feasibility of our method by verifying several variants of the well-known consistent broadcasting algorithm by Srikanth and Toueg for different fault models. To the best of our knowledge, this is the first successful automated parameterized verification of a Byzantine fault-tolerant distributed algorithm for message-passing systems.
Year
DOI
Venue
2013
10.1145/2484239.2484285
PODC
Keywords
Field
DocType
fault-tolerant distribed algorithm,brief announcement,parameterized model checking,successful automated parameterized verification,byzantine fault-tolerant,message-passing system,automated method,global system state,pia technique,system size,parameterized verification problem,parameterized verification,abstraction,fault tolerance
Abstraction model checking,Parameterized complexity,Model checking,Abstraction,Computer science,Fault tolerant distributed algorithms,Algorithm,Theoretical computer science,Distributed algorithm,Parametric statistics,Fault tolerance,Distributed computing
Conference
Citations 
PageRank 
References 
2
0.37
13
Authors
5
Name
Order
Citations
PageRank
Annu John1222.43
Igor Konnov25712.06
Ulrich Schmid3314.58
Helmut Veith42476140.58
Josef Widder522923.99