Deductive Verification of Parameterized Fault-Tolerant Systems: A Case Study

Nikolaj Bjorner, Uri Lerner, Zohar Manna

We present a methodology and a formal toolset for verifying fault-tolerant systems, based upon the temporal verification system STeP. Our test case is the modeling and verification of a parameterized fault-tolerant leader-election algorithm recently proposed in [GM96].

Our methods settle the general N-process correctness for the algorithm, which had been previously verified only for N=3. We formulate the notion of Uniform Compassion to model progress in faulty systems more faithfully, and combine it with the more standard notions of fairness. We also show how the correctness proofs generalize to different channel models by a reduction to a simple channel model.

In Proc. of International Conference on Temporal Logic, Kluwer, July 1997.

Postscript, PDF. © 1997, Kluwer Academic Publishers.

Last modified: Thu Mar 29 16:37:57 PST 2001