Advertisement

Sound and Complete Abstract Graph Transformation

  • Dominik Steenken
  • Heike Wehrheim
  • Daniel Wonisch
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)

Abstract

Graph transformation systems (GTS) are a widely used technique for the formal modeling of structures and structure changes of systems. To verify properties of GTS, model checking techniques have been developed, and to cope with the inherent infinity arising in GTS state spaces, abstraction techniques are employed.

In this paper, we introduce a novel representation for abstract graphs (which are shape graphs together with shape constraints) and define transformations (execution steps) on abstract graphs. We show that these abstract transformations are sound and complete in the sense that they capture exactly the transformations on the concrete graph level. Furthermore, abstract transformation can be carried out fully automatically. We thus obtain an effectively computable “best transformer” for abstract graphs which can be employed in an abstraction-based verification technique for GTS.

Keywords

Transformation Rule Graph Transformation Abstract Graph Abstract Domain Predicate Abstraction 
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.
This is a preview of subscription content, log in to check access.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Baldan, P., Corradini, A., König, B.: A framework for the verification of infinite-state graph transformation systems. Information and Computation 206(7), 869–907 (2008)zbMATHCrossRefGoogle Scholar
  2. 2.
    Ball, T., Podelski, A., Rajamani, S.: Boolean and cartesian abstraction for model checking c programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. 3.
    Bauer, J., Wilhelm, R.: Static analysis of dynamic communication systems by partner abstraction. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 249–264. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
    Bauer, J., Boneva, I., Kurbán, M., Rensink, A.: A modal-logic based graph abstraction. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 321–335. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  5. 5.
    Bisztray, D., Heckel, R., Ehrig, H.: Verification of architectural refactorings by rule extraction. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 347–361. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    Bogudlov, I., Lev-Ami, T., Reps, T., Sagiv, M.: Revamping TVLA: making parametric shape analysis competitive. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 221–225. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1979, pp. 269–282. ACM, New York (1979)Google Scholar
  8. 8.
    Engels, G., Güldali, B., Soltenborn, C., Wehrheim, H.: Assuring consistency of business process models and web services using visual contracts. In: Schürr, A., Nagl, M., Zündorf, A. (eds.) AGTIVE 2007. LNCS, vol. 5088, pp. 17–31. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Fitting, M.: Kleene’s three valued logics and their children. FI 20, 113–131 (1994)zbMATHGoogle Scholar
  10. 10.
    Graf, S., Saidi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  11. 11.
    Hülsbusch, M., König, B., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: Showing full semantics preservation in model transformation - a comparison of techniques. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 183–198. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  12. 12.
    Jha, S., Lu, Y., Grumberg, O., Clarke, E., Veith, H.: Counterexample-guided Abstraction Refinement. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 152–165. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Löwe, M.: Algebraic approach to single-pushout graph transformation. Theoretical Computer Science 109(1-2), 181–224 (1993)zbMATHCrossRefGoogle Scholar
  14. 14.
    Rensink, A.: The GROOVE simulator: A tool for state space generation. Applications of Graph Transformations with Industrial Relevance, 479–485 (2004)Google Scholar
  15. 15.
    Rensink, A., Distefano, D.: Abstract graph transformation. Electr. Notes Theor. Comput. Sci. 157(1), 39–59 (2006)zbMATHCrossRefGoogle Scholar
  16. 16.
    Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. ACM Trans. Program. Lang. Syst. 32, 24:1–24:55 (2010)zbMATHCrossRefGoogle Scholar
  17. 17.
    Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 3–25. Springer, Heidelberg (2004)Google Scholar
  18. 18.
    Reps, T.W., Sagiv, S., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002)CrossRefGoogle Scholar
  20. 20.
    Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 18–32. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    Steenken, D., Wehrheim, H., Wonisch, D.: Towards a shape analysis for graph transformation systems. In: Proceedings of the 22nd Nordic Workshop on Programming Theory (2010), Technical Report, http://www.cs.uni-paderborn.de/fileadmin/Informatik/AG-Wehrheim/Personen/Dominik_Steenken/ShapeAnalysis2010TR.pdf
  22. 22.
    Wonisch, D.: Increasing the preciseness of shape analysis for graph transformation systems. Master’s thesis, University of Paderborn (August 2010)Google Scholar
  23. 23.
    Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  24. 24.
    Yorsh, G., Reps, T., Sagiv, M., Wilhelm, R.: Logical characterizations of heap abstractions. ACM Trans. Comput. Logic 8 (January 2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Dominik Steenken
    • 1
  • Heike Wehrheim
    • 1
  • Daniel Wonisch
    • 1
  1. 1.Institut für InformatikUniversität PaderbornPaderbornGermany

Personalised recommendations

Cite paper

Buy options