A compositional network proof theory for specifying and verifying fault tolerant real-time distributed systems is presented. Important in such systems is the failure hypothesis that stipulates the class of failures that must be tolerated. In the formalism presented, the failure hypothesis of a system is represented by a predicate which expresses how faults might transform the behavior of the system. The approach is illustrated by investigating a triple modular redundant system.
|Title of host publication||Proceedings of the 12th Symposium on Reliable Distributed Systems (Princeton NJ, USA, October 6-8, 1993)|
|Publisher||Institute of Electrical and Electronics Engineers|
|Number of pages||10|
|Publication status||Published - 1993|