Compositional Proof Theory for Fault Tolerant Real-Time Distributed Systems

摘要

In this report we present a compositional network proof theory to specify andverify fault tolerant real-time distributed systems. Important in such systems is the failure hypothesis that stipulates the class of failures that must be tolerated. In the formalism presented in this report, the failure hypothesis of a system is represented by a predicate which expresses how faults might transform the observable input and output behavior of the system. A proof of correctness of a triple modular redundant system is given to illustrate our approach.