Abstract
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.
Recommended Citation
Tsai, Grace; Insall, Matt; and McMillin, Bruce M., "Constructing an Interval Temporal Logic for Real-Time Systems" (1993). Computer Science Technical Reports. 46.
https://scholarsmine.mst.edu/comsci_techreports/46
Department(s)
Computer Science
Report Number
CSC-93-25
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1993 University of Missouri--Rolla, All rights reserved.
Publication Date
20 Sep 1993
Comments
This work is supported by the research board of University of Missouri--Rolla, the National Science Foundation under Grant Numbers MSS-9216479 and CDA-9222827, and the Air Force Office of Scientific Research under contract number F49620-92-J-0546.