On Engineering a Distributed Algorithm

RISC-Linz logo

Wolfgang Schreiner
Research Institute for Symbolic Computation (RISC-Linz)
Johannes Kepler University, A-4040 Linz, Austria

Abstract

The aim of this paper to demonstrate rigorous reasoning in the context of concurrency. We present a small case study on the engineering of a distributed algorithm: its derivation from the problem specification, formal specifications of its behavior and of the desired correctness property, and rigorous proofs that the behavior always meets this property and eventually leads to a desired state.

Keywords: distributed algorithms, concurrency, temporal logic, specification, verification.

PostScript File

  • 1 Introduction
  • 2 The System Model
  • 3 The Termination Detection Algorithm
  • 4 Correctness of the Algorithm
  • 5 Progress of the Algorithm
  • References
  • Footnotes

  • Maintainer: Wolfgang Schreiner
    Last Modification: August 20, 1998

    [Up] [RISC-Linz] [University] [Search]