Generating oracles from your favorite temporal logic specifications

ABSTRACT

This paper describes a generic tableau algorithm, which is the basis for a general customizable method for producing oracles from temporal logic specifications. A generic argument gives semantic rules with which to build the semantic tableau for a specification. Parameterizing the tableau algorithm by semantic rules permits it to easily accommodate a variety of temporal operators and provides a clean mechanism for fine-tuning the algorithm to produce efficient oracles.The paper develops conditions to ensure that a set of rules results in a correct tableau procedure. It gives sample rules for a variety of linear-time temporal operators and shows how rules are tailored to reduce the size of an oracle.

REFERENCES

• 1: M. Blum and H. Wasserman. Program result-checking: A theory of testing meets a test of theory. In Proc. IEEE Symp. Foundations of Computer Science, 1994.
• 2: G. V. Bochmann , R. Dssouli , J. R. Zhao, Trace Analysis for Conformance and Arbitration Testing, IEEE Transactions on Software Engineering, v.15 n.11, p.1347-1356, November 1989 [doi>10.1109/32.41328]
• 3: J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th IEEE Symp. Logic in Computer Science, pp. 428-439, 1990.
• 4: S E. Chodrow, F. Jahanian, and M. Donner. Run-time monitoring of real-time systems. In Proc. IEEE Real-Time Systems Symp., pp. 74-83, San Antonio, TX, December 1991.
• 5: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 6: L. K. Dillon , G. Kutty , L. E. Moser , P. M. Melliar-Smith , Y. S. Ramakrishna, A graphical interval logic for specifying concurrent systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.2, p.131-165, April 1994 [doi>10.1145/192218.192226]
• 7: Laura K. Dillon , Qing Yu, Oracles for checking temporal properties of concurrent systems, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.140-153, December 06-09, 1994, New Orleans, Louisiana, United States
• 8: Victor Jon Griswold, Core algorithms for autonomous monitoring of distributed systems, Proceedings of the 1991 ACM/ONR workshop on Parallel and distributed debugging, p.36-45, May 20-21, 1991, Santa Cruz, California, United States
• 9: Yonit Kesten , Zohar Manna , Hugh McGuire , Amir Pnueli, A Decision Algorithm for Full Propositional Temporal Logic, Proceedings of the 5th International Conference on Computer Aided Verification, p.97-109, June 28-July 01, 1993
• 10: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 11: Hugh Wingfield McGuire, Two methods for checking formulas of temporal logic, Stanford University, Stanford, CA, 1995
• 12: Angelo Morzenti , Dino Mandrioli , Carlo Ghezzi, A model parametric real-time logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.4, p.521-573, Oct. 1992 [doi>10.1145/133233.129397]
• 13: T. O. O'Malley, D. J. Richardson, and L. K. Dillon. Efficient specification-based oracles for critical systems. In Walter Scacchi and Richard Taylor, eds., Proc. 1996 California Systems Symp., pp. 50-59, Los Angeles, CA, April 1996.
• 14: Y. Srinivas Ramakrishna, Interval logics for temporal specification and verification, University of California at Santa Barbara, Santa Barbara, CA, 1994
• 15: Debra J. Richardson, TAOS: Testing with Analysis and Oracle Support, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.138-153, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.187158]
• 16: Debra J. Richardson , Stephanie Leif Aha , T. Owen O'Malley, Specification-based test oracles for reactive systems, Proceedings of the 14th international conference on Software engineering, p.105-118, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143100]
• 17: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990
• 18: P. Wolper. The tableau method for temporal logic: An overview. In Logique et Analyse, vol. 11-111, pp. 119-136, June-September 1985.
• 19: Pierre Wolper, On the Relation of Programs and Computations to Models of Temporal Logic, Temporal Logic in Specification, p.75-123, April 08-10, 1987

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  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
      D.2.5 Testing and Debugging
          Subjects: Tracing
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Reliability, Theory, Verification

Keywords:
formal specification, propositional temporal logic, specification-based test oracles, tableau methods, test validation, verification