This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Temporal Logic Query Checking: A Tool for Model Exploration
October 2003 (vol. 29 no. 10)
pp. 898-914

Abstract—Temporal logic query checking was first introduced by W. Chan in order to speed up design understanding by discovering properties not known a priori. A query is a temporal logic formula containing a special symbol ?_1, known as a placeholder. Given a Kripke structure and a propositional formula \varphi, we say that \varphi satisfies the query if replacing the placeholder by \varphi results in a temporal logic formula satisfied by the Kripke structure. A solution to a temporal logic query on a Kripke structure is the set of all propositional formulas that satisfy the query. Query checking helps discover temporal properties of a system and, as such, is a useful tool for model exploration. In this paper, we show that query checking is applicable to a variety of model exploration tasks, ranging from invariant computation to test case generation. We illustrate these using a Cruise Control System. Additionally, we show that query checking is an instance of a multi-valued model checking of Chechik et al. This approach enables us to build an implementation of a temporal logic query checker, TLQSolver, on top of our existing multi-valued model checker \chi\rm Chek. It also allows us to decide a large class of queries and introduce witnesses for temporal logic queries—an essential notion for effective model exploration.

[1] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[2] E. Clarke, E. Emerson, and A. Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, Apr. 1986.
[3] W. Chan, Temporal-Logic Queries Proc. 12th Conf. Computer Aided Verification (CAV '00), pp. 450-463, July 2000.
[4] G. Bruns and P. Godefroid, Temporal Logic Query-Checking Proc. 16th Ann. IEEE Symp. Logic in Computer Science (LICS '01), pp. 409-417, June 2001.
[5] K. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[6] O. Kupferman, M. Vardi, and P. Wolper, An Automata-Theoretic Approach to Branching-Time Model Checking J. ACM, vol. 27, no. 2, pp. 312-360, Mar. 2000.
[7] S. Hornus and P. Schnoebelen, On Solving Temporal Logic Queries Proc. Ninth Int'l Conf. Algebraic Methodology and Software Technology (AMAST '02), pp. 163-177, 2002.
[8] M. Chechik, S. Easterbrook, and V. Petrovykh, Model-Checking over Multi-Valued Logics Proc. Formal Methods Europe (FME '01), pp. 72-98, Mar. 2001.
[9] M. Chechik, B. Devereux, and A. Gurfinkel, $\chi\rm Chek$: A MultiValued Model-Checker Proc. 14th Int'l Conf. Computer-Aided Verification (CAV'02), July 2002.
[10] B. Davey and H. Priestley, Introduction to Lattices and Order. Cambridge Univ. Press, 1990.
[11] M. Chechik, B. Devereux, S. Easterbrook, and A. Gurfinkel, Multi-Valued Symbolic Model-Checking ACM Trans. Software Eng. and Methodology, Jan. 2003.
[12] A. Gurfinkel and M. Chechik, MultiValued Model-Checking via Classical Model-Checking Proc. 14th Int'l Conf. Concurrency Theory (CONCUR '03), Sept. 2003.
[13] A. Gurfinkel, Multi-Valued Symbolic Model-Checking: Fairness, Counterexamples, Running Time Master's thesis, Dept. of Computer Science, Univ. of Toronto, Oct. 2002, http://www.cs.toronto. edu/chechik/pubsgurfinkelMSThesis.ps .
[14] A. Gurfinkel and M. Chechik, Proof-Like Counterexamples Proc. Ninth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '03), pp. 160-175, Apr. 2003.
[15] F. Somenzi, CUDD: CU Decision Diagram Package Release 2001, http://vlsi.colorado.edu/fabio/CUDDcuddIntro. html .
[16] M. Fujita, P.C. McGeer, and J.C.-Y. Yang, Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation Formal Methods in System Design: An Int'l J., vol. 10, nos. 2/3, pp. 149-169, Apr. 1997.
[17] M. Fröhlich and M. Werner, The Graph Visualization System daVinci A User Interface for Applications Technical Report 5/94, Dept. of Computer Science, Bremen Univ., 1994, citeseer.nj. nec.comfr94graph.html.
[18] Y. Dong, C. Ramakrishnan, and S.A. Smolka, Model Checking and Evidence Exploration Proc. 10th IEEE Int'l Conf. and Workshop Eng. of Computer Based Systems (ECBS '03), pp. 214-223, Apr. 2003.
[19] P. Stevens and C. Stirling, Practical Model-Checking Using Games Proc. Fourth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '98), pp. 85-101, 1998, citeseer.nj.nec.comstevens98practical.html .
[20] J. Kirby, Example NRL/SCR Software Requirements for an Automobile Cruise Control and Monitoring System technical report, Wang Inst. of Graduate Studies, Oct. 1988.
[21] C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw, Automated Consistency Checking of Requirements Specifications ACM Trans. Software Eng. and Methodology, vol. 5, no. 3, pp. 231-261, July 1996.
[22] M. Chechik, $\rm SC(R)^3$: Towards Usability of Formal Methods Proc. Ann. IBM Centre for Advanced Studies Conf., pp. 177-191, Nov. 1998.
[23] R. Jeffords and C. Heitmeyer, Automatic Generation of State Invariants from Requirements Specifications Proc. Sixth Int'l Symp. Foundations of Software Eng. (FSE '98), pp. 56-69, Nov. 1998.
[24] R.D. Jeffords and C.L. Heitmeyer, An Algorithm for Strengthening State Invariants Generated from Requirements Specifications Proc. Fifth IEEE Int'l Symp. Requirements Eng., pp. 182-191, Aug. 2001.
[25] J. Atlee, Automated Analysis of Software Requirements PhD dissertation, Univ. of Maryland, College Park, Dec. 1992.
[26] S. Rayadurgam and M.P. Heimdahl, Coverage Based Test-Case Generation Using Model Checkers Proc. Eighth Ann. IEEE Int'l Conf. and Workshop Eng. of Computer Based Systems (ECBS '01), pp. 83-93, Apr. 2001.
[27] A. Gargantini and C. Heitmeyer, Using Model Checking to Generate Tests from Requirements Specifications Proc. Joint Seventh European Software Eng. Conf. and Seventh ACM SIGSOFT Int'l Symp. Foundations of Software Eng. (ESEC/FSE '99), pp. 146-162, Sept. 1999.
[28] A. Engels, L. Feijs, and S. Mauw, Test Generation for Intelligent Networks Using Model Checking Proc. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '97), pp. 384-398, 1997.
[29] H. Hong, S. Cha, I. Lee, O. Sokolsky, and H. Ural, Data Flow Testing as Model Checking Proc. 25th Int'l Conf. Software Eng. (ICSE '03), May 2003.
[30] M. Chechik, B. Devereux, S. Easterbrook, A. Lai, and V. Petrovykh, Efficient Multiple-Valued Model-Checking Using Lattice Representations Proc. 12th Int'l Conf. Concurrency Theory (CONCUR '01), pp. 451-465, Aug. 2001.
[31] I. Wegener, Branching Programs and Binary Decision Diagrams: Theory and Applications. SIAM, 2000.
[32] G. Bruns and P. Godefroid, Generalized Model Checking: Reasoning about Partial State Spaces Proc. 11th Int'l Conf. Concurrency Theory (CONCUR '00), pp. 168-182, Aug. 2000.

Index Terms:
CTL, query checking, model checking, TLQSolver, model understanding, multi-valued logic.
Citation:
Arie Gurfinkel, Marsha Chechik, Benet Devereux, "Temporal Logic Query Checking: A Tool for Model Exploration," IEEE Transactions on Software Engineering, vol. 29, no. 10, pp. 898-914, Oct. 2003, doi:10.1109/TSE.2003.1237171
Usage of this product signifies your acceptance of the Terms of Use.