Trace-Based Compositional Proof Theory for Fault Tolerant Distributed Systems

摘要

We present a compositional network proof theory to specify and verify safetyproperties of fault tolerant distributed systems. In this proof theory we abstract from the precise nature and occurrence of faults, but model their effect on the externally visible input and output behavior. To this end we formalize a fault hypothesis as a reflexive relation between the normal behavior (i.e. the behavior when no faults occur) of a system and its acceptable behavior, that is, the normal behavior together with the exceptional behavior (i.e. the behavior whose abnormality should be tolerated). The method is compositional to allow for the reasoning with the specifications of processes while ignoring their implementation details. This compositionality is achieved by starting from a SAT formalism to reason about the normal behavior and extending it with a single rule to obtain a specification of the acceptable behavior from the specification of the normal behavior and a predicate characterizing the fault hypothesis. We prove soundness and relative network completeness of the method. Our approach is illustrated by applying it to a triple modular redundant component and the alternating bit protocol.