Parameterized model checking of fault-tolerant distributed algorithms

Abstract

Distributed algorithms play an inevitable role in our day to day life. Their applications extend to our household equipments, medical equipments, air trac control, space missions, Internet and such numerous elds of application. Fault-Tolerant Distributed Algorithms (FTDAs) were introduced to increase the reliability of distributed algorithms. FTDAs are designed in a way that the system functions correctly even in the presence of a certain number of faults in the system. However, in order to ful ll the purpose of an FTDA, it is necessary to ensure that no man-made errors have crept into its design. In other words, it needs to be veri ed that the FTDA satis es its speci cations. In the distributed algorithms community such algorithms are represented using informal pseudo code. Their correctness is proved by mathematical rea- soning in natural language. The many dimensions of non-determinism present in FTDAs make their manual reasoning a dicult and erroneous task. Thus verifying these algorithms formally is the only way to ensure their correctness. Our aim is to automatically verify a widely used class of FTDAs. FTDAs are parameterized in multiple parameters. Thus we need to consider all possible values the parameters can take, to verify these algorithms. We introduce a formal framework which captures the behaviour of such algorithms and an abstraction method to eliminate parameters. To validate our approach we present several case studies. We show that our abstraction method is sound by using simulation proofs.