Advertisement

Refinement of LTL Formulas for Abstract Model Checking

  • Marίa del Mar Gallardo
  • Pedro Merino
  • Ernesto Pimentel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)

Abstract

A crucial problem in abstract model checking is to find a tradeoff between constructing the “best” (the smallest) abstract model, approximating a given model, and preserving as much interesting properties over the original model as possible. In this paper, we present a method for dealing with this problem based on the definition of a new abstract satisfiability relation. This new relation allows us to analyze temporal properties with different degrees of precision, by means of a refinement process. The method subsumes the classic way of abstracting properties and the dual proposal of the authors. As a consequence, maintaining the same abstract model, we directly obtain the preservation of universal properties (as in the classic method) and the refutation of existential properties (as in the dual method). We also show the utility of this method by proving that the very important notions of completeness and precision in abstract model checking may be analyzed by using the new relation. In particular, we exploit the power of model checking to simultaneously refine both the model and the properties.1

Keywords

Model Check Abstract Model Universal Property Abstract Interpretation Atomic Proposition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    S. Bensalem, Y. Lakhnech, S. Owre, Computing abstractions of infinite state systems compositionally and automatically. In Computer-Aided Verification CAV’98, LNCS-1427, pp. 319–331, (1998).CrossRefGoogle Scholar
  2. 2.
    E.M. Clarke, O. Grumberg, D. Peled. Model Checking (The MIT Press, 2000).Google Scholar
  3. 3.
    E.M. Clarke, E. A. Emerson, A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. on Programming Languages and Systems, 8(2) (1986) 244–263.zbMATHCrossRefGoogle Scholar
  4. 4.
    E.M. Clarke, O. Grumberg, D.E. Long. Model Checking and Abstraction. ACM Transaction on Languages and Systems, 16(5) (1994) 1512–1245.CrossRefGoogle Scholar
  5. 5.
    E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-guided abstraction refinement. In Computer-Aided Verification CAV’00, LNCS-1855, pp. 154–169, (2000).CrossRefGoogle Scholar
  6. 6.
    R. Cleveland, P. Iyer, D. Yankelevich. Optimality in Abstractions of Model Checking. In Proceedings of Static Analysis Symposium LNCS-983, pp. 51–63, (1995)Google Scholar
  7. 7.
    J. Corbett, M. Dwyer, J. Hatcliff, L. Shawn, C. Pasareanu, H. Zheng. Bandera: Extracting Finite-State Models from Java Source Code. In Proc. 22nd Int. Conf. On Software Engineering, pp. 439–448, (2000).Google Scholar
  8. 8.
    P. Cousot, R. Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conf. Record of the 4th ACM Symp. on Princ. of Prog. Languages, pp. 238–252, (1977).Google Scholar
  9. 9.
    P. Cousot, R. Cousot. Refining Model Checking by Abstract Interpretation. Automated Software Engineering 6 (1999) 69–95.CrossRefGoogle Scholar
  10. 10.
    D. Dams, R. Gerth, O. Grumberg. Abstract Interpretation of Reactive Systems. ACM Trans. on Programming Languages and Systems, 19(2) (1997) 253–291.CrossRefGoogle Scholar
  11. 11.
    M.M. Gallardo, P. Merino. A Framework for Automatic Construction of Abstract PROMELA Models. In Theoretical and Practical Aspects of SPIN Model Checking, LNCS-1680, pp. 184–199, (1999).CrossRefGoogle Scholar
  12. 12.
    M.M. Gallardo, P. Merino, E. Pimentel. Verifying Abstract LTL Properties on Concurrent Systems. In Proc. of the 6th World Conference on Integrated Design & Process Technology, (2002).Google Scholar
  13. 13.
    M. M. Gallardo, J. Martίnez, P. Merino, E. Pimentel. αSPIN: Extending SPIN with Abstraction. In Proc. of the 9th International SPIN Workshop on Model Checking of Software, LNCS 2318, pp. 254–258, (2002).Google Scholar
  14. 14.
    R. Giacobazzi, F. Ranzato, F. Scozzari. Making abstract interpretation complete. In Journal of ACM, 47(2) (2000), 361–416.CrossRefzbMATHMathSciNetGoogle Scholar
  15. 15.
    R. Giacobazzi, E. Quintarelli. Incompleteness, Counterexamples and Refinement in Abstract Model-Checking. In The 8th International Static Analysis Symposium SAS’01, LNCS 2126, pp. 356–373, (2001).Google Scholar
  16. 16.
    S. Graf. Verification of a distributed Cache Memory by using abstractions. In Computer Aided Verification CAV’94, LNCS-818, pp. 207–219, (1994).Google Scholar
  17. 17.
    G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.Google Scholar
  18. 18.
    G.J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5) (1997) 279–295.CrossRefMathSciNetGoogle Scholar
  19. 19.
    C. Loiseaux, S. Graf, J. Sifakis, A. Boujjani, S. Bensalem. Property Preserving Abstractions for the Verification of Concurrent Systems. Formal Methods in System Design 6 (1995) 1–35.CrossRefGoogle Scholar
  20. 20.
    Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems-Specification. Springer-Verlag, New York, (1992).Google Scholar
  21. 21.
    C.S. Pasareanu, M.B. Dwyer, W. Visser. Finding Feasible Counter-examples when Model Checking Abstracted Java Programs. In Proc. of 7th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, LNCS-2031, pp. 284–298, (2001).Google Scholar
  22. 22.
    H. Saídi, N. Shankar. Abstract and model check while you prove. In Computer-Aided Verification CAV’99 LNCS-1633, pp. 443–454, (1999).CrossRefGoogle Scholar
  23. 23.
    H. Samídi. Model Checking guided abstraction and analysis. In Seventh Internationa Static Analysis Symposium (SAS’00), LNCS-1824, pp. 377–396, (2000).Google Scholar
  24. 24.
    αSpin project. University of Málaga. http://www.lcc.uma.es~gisum/fmse/tools.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Marίa del Mar Gallardo
    • 1
  • Pedro Merino
    • 1
  • Ernesto Pimentel
    • 1
  1. 1.Dpto. de Lenguajes y Ciencias de la ComputaciónUniversity of MálagaMálagaSpain

Personalised recommendations