On Engineering a Distributed Algorithm

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. Contents 1 Introduction 2 2 The System Model 3 3 The Termination Detection Algorithm 8 4 Correctness of the Algorithm 15 5 Progress of the Algorithm 23 1 Introduction 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. This paper was inspired by a le..