On Engineering a Distributed Algorithm
Research Institute for Symbolic Computation (RISC-Linz)
Johannes Kepler University, A-4040 Linz, Austria
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.