Probabilistic verification of a synchronous round-based consensus protocol

Harpreet S. Duggal, Michel Cukier, William H. Sanders

Research output: Contribution to journalConference articlepeer-review

Abstract

Consensus protocols are used in a variety of reliable distributed systems, including both safety- 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. In this paper, 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.

Original languageEnglish (US)
Pages (from-to)165-174
Number of pages10
JournalProceedings of the IEEE Symposium on Reliable Distributed Systems
StatePublished - Dec 1 1997
EventProceedings of the 1997 IEEE 16th Symposium on Reliable Distributed Systems - Durham, NC, USA
Duration: Oct 22 1997Oct 24 1997

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Probabilistic verification of a synchronous round-based consensus protocol'. Together they form a unique fingerprint.

Cite this