Constructing an Interval Temporal Logic for Real-Time Systems

A real-time system is one that involves control of one or more physical devices with essential timing requirements. Examples of these systems are command and control systems, process control systems, flight control systems, and the space shuttle avionics systems. The characteristics of these systems are that severe consequences will occur if the logical and physical timing specifications of the systems are not met. Formal specification and verification are among the techniques to achieve reliable software for real-time systems, in which testing may be impossible or too dangerous to perform. This paper presents a modal logic, Interval Temporal , built upon a classical predicate logic In this logic system, we consider formulas that can be used to reason about timing properties of systems, in particular, responsiveness assertions. A responsiveness assertion describes constraints that a program must satisfy within an interval. Thus, it can be utilized to characterize behaviors of life-critical systems. We assume that a program P can be identified with a theory, a collection of formulas characterizing sequences of states of P with arbitrary initial states. In the following, we describe syntax and semantics of the logic, present a proof rule for responsiveness assertions, and show soundness and relative completeness of responsiveness assertions that we consider. There are other approaches to build temporal logics for real-time systems, which are included in bibliography