
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 898914, October, 2003.  
BibTex  x  
@article{ 10.1109/TSE.2003.1237171, author = {Arie Gurfinkel and Marsha Chechik and Benet Devereux}, title = {Temporal Logic Query Checking: A Tool for Model Exploration}, journal ={IEEE Transactions on Software Engineering}, volume = {29}, number = {10}, issn = {00985589}, year = {2003}, pages = {898914}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2003.1237171}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Temporal Logic Query Checking: A Tool for Model Exploration IS  10 SN  00985589 SP898 EP914 EPD  898914 A1  Arie Gurfinkel, A1  Marsha Chechik, A1  Benet Devereux, PY  2003 KW  CTL KW  query checking KW  model checking KW  TLQSolver KW  model understanding KW  multivalued logic. VL  29 JA  IEEE Transactions on Software Engineering ER   
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] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[2] E. Clarke, E. Emerson, and A. Sistla, Automatic Verification of FiniteState Concurrent Systems Using Temporal Logic Specifications ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244263, Apr. 1986.
[3] W. Chan, TemporalLogic Queries Proc. 12th Conf. Computer Aided Verification (CAV '00), pp. 450463, July 2000.
[4] G. Bruns and P. Godefroid, Temporal Logic QueryChecking Proc. 16th Ann. IEEE Symp. Logic in Computer Science (LICS '01), pp. 409417, June 2001.
[5] K. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[6] O. Kupferman, M. Vardi, and P. Wolper, An AutomataTheoretic Approach to BranchingTime Model Checking J. ACM, vol. 27, no. 2, pp. 312360, 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. 163177, 2002.
[8] M. Chechik, S. Easterbrook, and V. Petrovykh, ModelChecking over MultiValued Logics Proc. Formal Methods Europe (FME '01), pp. 7298, Mar. 2001.
[9] M. Chechik, B. Devereux, and A. Gurfinkel, $\chi\rm Chek$: A MultiValued ModelChecker Proc. 14th Int'l Conf. ComputerAided 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, MultiValued Symbolic ModelChecking ACM Trans. Software Eng. and Methodology, Jan. 2003.
[12] A. Gurfinkel and M. Chechik, MultiValued ModelChecking via Classical ModelChecking Proc. 14th Int'l Conf. Concurrency Theory (CONCUR '03), Sept. 2003.
[13] A. Gurfinkel, MultiValued Symbolic ModelChecking: 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, ProofLike Counterexamples Proc. Ninth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '03), pp. 160175, 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, MultiTerminal 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. 149169, 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. 214223, Apr. 2003.
[19] P. Stevens and C. Stirling, Practical ModelChecking Using Games Proc. Fourth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '98), pp. 85101, 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. 231261, July 1996.
[22] M. Chechik, $\rm SC(R)^3$: Towards Usability of Formal Methods Proc. Ann. IBM Centre for Advanced Studies Conf., pp. 177191, 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. 5669, 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. 182191, 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 TestCase Generation Using Model Checkers Proc. Eighth Ann. IEEE Int'l Conf. and Workshop Eng. of Computer Based Systems (ECBS '01), pp. 8393, 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. 146162, 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. 384398, 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 MultipleValued ModelChecking Using Lattice Representations Proc. 12th Int'l Conf. Concurrency Theory (CONCUR '01), pp. 451465, 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. 168182, Aug. 2000.