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

H. Schepers, J.J.M. Hooman

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

6 Citaten (Scopus)


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.
Originele taal-2Engels
Pagina's (van-tot)127-157
Aantal pagina's31
TijdschriftTheoretical Computer Science
Nummer van het tijdschrift1-2
StatusGepubliceerd - 1994


Duik in de onderzoeksthema's van 'A trace-based compositional proof theory for fault tolerant distributed systems'. Samen vormen ze een unieke vingerafdruk.

Citeer dit