A trace-based compositional proof theory for fault tolerant distributed systems (Q1330425)

A compositional network proof theory for specification and verification of safety properties of fault-tolerant distributed systems is presented. Modeling the effects of faults on the external systems behaviour, i.e. their input/output, is focused. The relation between the system's regular behaviour in case no failure occurs and its acceptable behaviour under failure occurrence is formulated as a failure hypothesis. The paper considers only safety properties, ignoring liveness issues. The propagated method is compositional to allow reasoning with the specifications of processes while ignoring their implementation details. Examples are given applying the method to a triple-modular redundant system and the alternating bit protocol.