TY - CONF T1 - Probabilistic verification of a synchronous round-based consensus protocol Y1 - 1997 A1 - Duggal,H.S. A1 - Michel Cukier A1 - Sanders,W. H. KW - business-critical applications KW - consensus protocol correctness KW - crash failures KW - formal verification KW - network environment KW - probabilistic verification KW - probabilities KW - probability KW - program verification KW - proper behavior KW - protocol behavior KW - Protocols KW - realistic environment KW - reliable distributed systems KW - safety-critical applications KW - simple consensus protocol KW - software reliability KW - stochastic assumptions KW - synchronous round based consensus protocol KW - synchronous round based consensus protocols KW - traditional proof techniques AB - Consensus protocols are used in a variety of reliable distributed systems, including both safety-critical and business-critical applications. The correctness of a consensus protocol is usually shown, by making assumptions about the environment in which it executes, and then proving properties about the protocol. But proofs about a protocol's behavior are only as good as the assumptions which were made to obtain them, and violation of these assumptions can lead to unpredicted and serious consequences. We present a new approach for the probabilistic verification of synchronous round based consensus protocols. In doing so, we make stochastic assumptions about the environment in which a protocol operates, and derive probabilities of proper and non proper behavior. We thus can account for the violation of assumptions made in traditional proof techniques. To obtain the desired probabilities, the approach enumerates possible states that can be reached during an execution of the protocol, and computes the probability of achieving the desired properties for a given fault and network environment. We illustrate the use of this approach via the evaluation of a simple consensus protocol operating under a realistic environment which includes performance, omission, and crash failures M3 - 10.1109/RELDIS.1997.632812 ER -