Inductive basic correctness reasoning in formal fault-tolerance proofs for distributed algorithms

Abstract

Standard distributed algorithmic solutions to recurring distributed problems are commonly specified and described informally. Formal analysis to demonstrate fault-tolerance of these distributed algorithms requires formal descriptions, however, formalisation tends to yield complex descriptions and proofs. Work has been conducted to alleviate the burden of formalisation. A technique proposed in [FH07a] decomposes fault-tolerance proofs into two phases; the basic correctness phase which verifies the algorithm's behaviour under no failures, and the correctness preservation phase which compares the behaviour under no failures to the behaviour of the distributed algorithm when failures are induced. In this dissertation we study two distributed broadcast algorithms. We exploit the regular replicated structure and behaviour (processes) of such distributed algorithms to give inductive formal encodings of both the algorithms and the respective specifications that are expected to be satisfied. We then use this inductive structure to extend the compositional verification technique in [FH07a] whereby we present inductive proofs that generalise over an arbitrary number of participants in broadcast algorithms for the basic correctness phase.