Real-time interval logic for reasoning about executions of real-time programs

ABSTRACT

Research on the testing and debugging of distributed real-time programs now focuses on more formal approaches to specification and testing. Temporal logic is a natural candidate for this since it can specify properties of event and state sequences. However, the absence of any concept of real-time limits the application of temporal logic to non real-time behavior. This paper presents an extension of the interval logic of Schwartz et al. [SMSVP83], by increasing the expressive power of the logic (with respect to real time) while retaining its intuitive appeal and understandability. The extensions are added in a “layer” that can be stripped away if formal verification is the goal, or retained if timing behavior must be tested. The extensions include: the ability to deal with real time (as in [JM86b, JM86a, OW87, NA88]); more powerful interval specification mechanisms; a limited form of quantification; and the direct expression of event predicates (as in [LeD86]). Since our work is intended to yield practical tools for software testers, we emphasize the ease of expressing the complex timing properties of real-time software (e.g. periodic behavior, performance constraints), and we demonstrate the use of the interval logic on some real-time examples that represent a test of the expressiveness and understandability of the notation.

REFERENCES

• GKY88: G. Goldszmidt , S. Katz , S. Yemini, Interactive blackbox debugging for concurrent languages, Proceedings of the 1988 ACM SIGPLAN and SIGOPS workshop on Parallel and distributed debugging, p.271-282, May 05-06, 1988, Madison, Wisconsin, United States
• GR89: M. M. Gorlick and R. R. Raaouk. A model-theoretic semantics for real-time interval logic. Technical Report (in preparation), The Aerospace Corporation, El Segundo, California, April 1969.
• Jaf88: Matthew Saul Jaffe, Completeness, robustness, and safety in real-time software requirements specifications: a logical positivist looks at requirements engineering, University of California at Irvine, Irvine, CA, 1988
• JM86a: F. Jahanian and A. Mok. A graph-theoretic approach for timing analysis in real time logic. In Proceedings of the IEEE 1986 Real-Time Systems Symposium, pages 98-108, December 1986.
• JM86b: F Jahanian , A K Mok, Safety analysis of timing properties in real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.890-904, Sept. 1986
• Lam81: Leslie Lamport, TIMESETS -- A New Method for Temporal Reasoning about Programs, Logic of Programs, Workshop, p.177-196, May 01, 1981
• LeD86: C. H. LeDoux. A knowledge-based system for debugging concurrent software. Technical Report ATRS6(8134)-1, The Aerospace Corporation, El Segundo, CA, January 1986.
• NA88: K.T. Narayana and A.A. Aaby. Specification of real-time systems in real-time temporal interval logic. In 1988 Conference on Real-Time Systems, pages 86-95. IEEE Press, 1988.
• OW87: J.S. Ostroff and W.M. Wonham. Modelling, specifying and verifying real-time embedded computer systems. In Proceedings of the IEEE 1987ReaZ-Time Systems Symposium, pages 124-132, 1987.
• SMSVP83: R.L. Schwartz, P. M. Melliar-Smith, F. H. Vogt, and D. A. Plaisted. An interval logic for higher-level temporal reasoning. Technical report, SRI International, Menlo Park, CA, September 1983.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

General Terms:
Reliability, Theory, Verification