Automatic verification of fault-tolerant register emulations

Paul C. Attie, Hana Chockler

Research output: Contribution to journalConference article

Abstract

The design and verification of fault-tolerant distributed algorithms is a complicated task. Usually, the proof of correctness is done manually, and thus depends on the skill of the prover. Using automated verification methods, such as model checking, can greatly simplify the verification. However, model checking of distributed algorithms is often intractable because of the state-explosion problem. In this paper we present a novel approach to verification of quorum-based distributed register emulation algorithms with undetectable crash failures of processes. Our approach is based on projection and abstraction and allows us to reduce the task of model-checking the whole system to fair model-checking of subsystems consisting of a constant number of processes. Our method is highly scalable and can be applied to a large class of algorithms. Aside from efficient verification, it can also be used for finding redundancies in existing algorithms.

Original languageEnglish (US)
Pages (from-to)49-60
Number of pages12
JournalElectronic Notes in Theoretical Computer Science
Volume149
Issue number1
DOIs
StatePublished - Feb 3 2006
Externally publishedYes
EventProceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY 2005) -
Duration: Aug 27 2005Aug 27 2005

Keywords

  • Automatic verification
  • Crash failures
  • Distributed algorithms
  • Fault-tolerance
  • Model checking
  • Parametrized systems
  • Register emulation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automatic verification of fault-tolerant register emulations'. Together they form a unique fingerprint.

  • Cite this