Language and Tool Support for Model Checking of Fault-Tolerant Distributed Algorithms

Model checking is a successful formal verification technique; however, its application to fault-tolerant distributed algorithms is still not common practice. One major reason for this is that model checking requires non-negligible users¿ efforts in representing the algorithm to be verified in the input language of a model checker. To alleviate this problem we propose an approach which encompasses (i) a language for concisely describing fault-tolerant distributed algorithms and (ii) a translator from the proposed language to PROMELA, the input language of the SPIN model checker. To demonstrate the feasibility of our approach, we show the results of an experiment where we described and verified several algorithms for consensus, a well-known distributed agreement problem.