Efficient temporal-logic query checking for presburger systems

ABSTRACT

This paper develops a framework for solving temporal-logic query-checking problems for a class of infinite-state system models that compute with integer-valued variables (so-called Presburger systems, in which Presburger formulas are used to define system behavior). The temporal-logic query checking problem may be formulated as follows: given a model and a temporal logic formula with placeholders, compute a set of assignments of formulas to placeholders such that the resulting temporal formula is satisfied by the given model. Temporal-logic query checking has proved useful as a means for requirements and design understanding; existing work, however, has focused only on propositional temporal logic and finite-state systems.Our method is based on a symbolic model-checking technique that relies on proof search. The paper first introduces this model-checking approach and then shows how it can be adapted to solving the temporal queries in which formulas may contain integer variables. We also present experimental results showing the computational efficacy of our approach.

REFERENCES

• 1: Henrik Reif Andersen, Model checking and boolean graphs, Theoretical Computer Science, v.126 n.1, p.3-30, April 11, 1994 [doi>10.1016/0304-3975(94)90266-6 ]
• 2: Joanne M. Atlee , Michael A. Buckley, A logic-model semantics for SCR software requirements, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.280-292, January 08-10, 1996, San Diego, California, United States
• 3: C. Bartzis and T. Bultan. Efficient symbolic representations for arithmetic constraints in verification. International Journal of Foundations of Computer Science (IJFCS), 14(4):605--624, Aug. 2003.
• 4: Girish Bhat , Rance Cleaveland , Orna Grumberg, Efficient On-the-Fly Model Checking for CTL, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.388, June 26-29, 1995
• 5: Glenn Bruns , Patrice Godefroid, Temporal Logic Query Checking, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.409, June 16-19, 2001
• 6: Tevfik Bultan , Richard Gerber , William Pugh, Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic, Proceedings of the 9th International Conference on Computer Aided Verification, p.400-411, June 22-25, 1997
• 7: William Chan, Temporal-Locig Queries, Proceedings of the 12th International Conference on Computer Aided Verification, p.450-463, July 15-19, 2000
• 8: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 9: R. Cleaveland, Tableau-based model checking in the propositional mu-calculus, Acta Informatica, v.27 n.9, p.725-747, Sep. 1990
• 10: Hubert Comon , Yan Jurski, Multiple Counters Automata, Safety Analysis and Presburger Arithmetic, Proceedings of the 10th International Conference on Computer Aided Verification, p.268-279, June 28-July 02, 1998
• 11: Arie Gurfinkel , Benet Devereux , Marsha Chechik, Model exploration with temporal logic query checking, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587073]
• 12: Constance L. Heitmeyer , Ralph D. Jeffords , Bruce G. Labaw, Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.3, p.231-261, July 1996 [doi>10.1145/234426.234431]
• 13: Samuel Hornus , Ph. Schnoebelen, On Solving Temporal Logic Queries, Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, p.163-177, September 09-13, 2002
• 14: Julian Bradfield , Colin Stirling, Local model checking for infinite state spaces, Theoretical Computer Science, v.96 n.1, p.157-174, 6 April 1992
• 15: N. Klarlund and A. Moller. MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus, Jan. 2001.
• 16: D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333--354, Dec. 1983.
• 17: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• 18: M. Samer and H. Veith. Validity of ctl queries revisited. In CSL'03, LNCS 2803, pages 470--483, 2003.
• 19: Li Tan , Rance Cleaveland, Evidence-Based Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.455-470, July 27-31, 2002
• 20: A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math., 1955.
• 21: Tuba Yavuz-Kahveci , Murat Tuncer , Tevfik Bultan, A Library for Composite Symbolic Representations, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.52-66, April 02-06, 2001
• 22: D. Zhang and R. Cleaveland. Fast generic model-checking for data-based systems. In F. Wang, editor, Proceedings of the 25th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2005), volume 3731 ofLecture Notes in Computer Science, Taiwan, Oct. 2005. Springer-Verlag.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Design, Experimentation, Performance, Verification

Keywords:
Presburger systems, formal methods, model checking, on-the-fly symbolic model checking, query checking