Advertisement

Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL

  • Jörg Hoffmann
  • Jan-Georg Smaus
  • Andrey Rybalchenko
  • Sebastian Kupferschmid
  • Andreas Podelski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)

Abstract

We focus on checking safety properties in networks of extended timed automata, with the well-known UPPAAL system. We show how to use predicate abstraction, in the sense used in model checking, to generate search guidance, in the sense used in Artificial Intelligence (AI). This contributes another family of heuristic functions to the growing body of work on directed model checking. The overall methodology follows the pattern database approach from AI: the abstract state space is exhaustively built in a pre-process, and used as a lookup table during search. While typically pattern databases use rather primitive abstractions ignoring some of the relevant symbols, we use predicate abstraction, dividing the state space into equivalence classes with respect to a list of logical expressions (predicates). We empirically explore the behavior of the resulting family of heuristics, in a meaningful set of benchmarks. In particular, while several challenges remain open, we show that one can easily obtain heuristic functions that are competitive with the state-of-the-art in directed model checking.

Keywords

Safety Property Heuristic Function Predicate Abstraction Error Path Pattern Database 
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.
    Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI 2001: Programming Language Design and Implementation, pp. 203–213 (2001)Google Scholar
  2. 2.
    Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE 2003: Int. Conf. on Software Engineering, pp. 385–395 (2003)Google Scholar
  3. 3.
    Culberson, J., Schaeffer, J.: Pattern databases. Computational Intelligence 14(3), 318–334 (1998)CrossRefMathSciNetGoogle Scholar
  4. 4.
    Dierks, H.: Comparing model-checking and logical reasoning for real-time systems. Formal Aspects of Computing 16(2), 104–120 (2004)zbMATHCrossRefGoogle Scholar
  5. 5.
    Dräger, K., Finkbeiner, B., Podelski, A.: Directed model checking with distance-preserving abstractions. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol. 3925, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology Transfer (2004)Google Scholar
  8. 8.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)Google Scholar
  9. 9.
    Groce, A., Visser, W.: Model checking Java programs using structural heuristics. In: International Symposium on Software Testing and Analysis, pp. 12–21 (2002)Google Scholar
  10. 10.
    Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: POPL 2004: Principles of Programming Languages, pp. 232–244 (2004)Google Scholar
  11. 11.
    Hoffmann, J., Koehler, J.: A new method to query and index sets. In: 16th International Joint Conference on Artificial Intelligence (IJCAI-1999), pp. 462–467 (1999)Google Scholar
  12. 12.
    Krieg-Brückner, B., Peleska, J., Olderog, E., Baer, A.: The UniForM Workbench, a universal development environment for formal methods. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 1186–1205. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  13. 13.
    Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol. 3925, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 497–511. Springer, Heidelberg (2004)Google Scholar
  16. 16.
    Rybalchenko, A.: A model checker based on abstraction refinement. Master’s thesis, Universität des Saarlandes (2002)Google Scholar
  17. 17.
    Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Jörg Hoffmann
    • 1
  • Jan-Georg Smaus
    • 2
  • Andrey Rybalchenko
    • 3
    • 4
  • Sebastian Kupferschmid
    • 2
  • Andreas Podelski
    • 2
  1. 1.Digital Enterprise Research Institute (DERI), InnsbruckAustria
  2. 2.University of FreiburgGermany
  3. 3.Max Planck Institute for Computer Science, SaarbrückenGermany
  4. 4.Ecole Polytechnique Fédérale de LausanneSwitzerland

Personalised recommendations