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

H. Schepers, J.J.M. Hooman

Research output: Contribution to journalArticleAcademicpeer-review

9 Citations (Scopus)

Abstract

We present a compositional network proof theory to specify and verify safety properties of fault tolerant distributed systems. 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 a failure hypothesis is formalized as a relation between the normal behavior (i.e. the behaviour when no faults occur) of a system and its acceptable behaviour, that is, the normal behaviour together with the exceptional behaviour (i.e. the behaviour whose abnormality should be tolerated). The method is compositional to allow reasoning with the specifications of processes while ignoring their implementation details. A compositional formalism to reason about the normal behaviour is extended with a single rule by which a specification of the acceptable behaviour can be obtained from the specification of the normal behaviour and a predicate characterizing the failure hypothesis. Soundness and relative network completeness are proved. Our approach is illustrated by applying it to a triple modular redundant system and the alternating bit protocol.
Original languageEnglish
Pages (from-to)127-157
Number of pages31
JournalTheoretical Computer Science
Volume128
Issue number1-2
DOIs
Publication statusPublished - 1994

Fingerprint Dive into the research topics of 'A trace-based compositional proof theory for fault tolerant distributed systems'. Together they form a unique fingerprint.

Cite this