Parametrized semantics for fault tolerant real-time systems

Motivated by the close relation between real-time and fault tolerance, we investigate the foundations of a formal framework to specify and verify real-time distributed systems that incorporate fault tolerance techniques. Therefore a denotational semantics is presented to describe the real-time behaviour of distributed programs in which concurrent processes communicate by synchronous message passing. In this semantics we allow the occurrence of faults, due to faults of the underlying execution mechanism, and we describe the effect of these faults on the real-time behaviour of programs. Whenever appropriate we give alternative choices for the definition of the semantics. The main idea is that making only very weak assumptions about faults and their effect upon the behaviour of a program in the semantics, any hypothesis about faults must be made explicit in the correctness proof of a program. Next we introduce two parameters in the semantics that restrict the way in which variables and communication channels can be affected by faults. These parameters provide an easy way to incorporate some interesting fault hypotheses within the semantics.