Formal specification of fault tolerant real time systems using minimal 3-sorted modal logic

Fault tolerance is the property of a system to provide a specified service despite the occurrence of faults, i. e. to prevent a system from failing even in the presence of faults. In this paper, we will contribute to the area of formal specification of fault tolerant real time systems to make fault tolerance and real time formally treatable in a unified approach.According to the paradigm of separation of concerns we get separation in two directions: In real time systems, a distinction can be made between functional, locational, and temporal properties. To explicitly state such properties in a formal specification we will use a three- sorted modal logic.In fault tolerant systems, two kinds of behaviour can be distinguished from each other: normal behaviour, which takes place if no fault occurs during system execution, and exceptional behaviour, which takes place just in the case of a fault occurrence. To separate system properties according to that a logical connective C (Combine) will be defined. This connective allows to state predicates about normal behaviour as well as exceptional behaviour and it also provides the possibility to specify the conditions under which the one or the other behaviour will be reached. To ensure that a fault tolerant real time system has precisely the properties stated in its formal specification minimal model interpretation is applied to the logical formulae.