Skip to main content
SpringerLink
Log in
Book cover

Brazilian Symposium on Formal Methods

SBMF 2011: Formal Methods, Foundations and Applications pp 92–107Cite as

Sound and Complete Abstract Graph Transformation

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  9. Fitting, M.: Kleene’s three valued logics and their children. FI 20, 113–131 (1994)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  13. Löwe, M.: Algebraic approach to single-pushout graph transformation. Theoretical Computer Science 109(1-2), 181–224 (1993)

    Article  MATH  Google Scholar 

  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. Rensink, A., Distefano, D.: Abstract graph transformation. Electr. Notes Theor. Comput. Sci. 157(1), 39–59 (2006)

    Article  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Wonisch, D.: Increasing the preciseness of shape analysis for graph transformation systems. Master’s thesis, University of Paderborn (August 2010)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  24. Yorsh, G., Reps, T., Sagiv, M., Wilhelm, R.: Logical characterizations of heap abstractions. ACM Trans. Comput. Logic 8 (January 2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Paderborn, 33098, Paderborn, Germany

    Dominik Steenken, Heike Wehrheim & Daniel Wonisch

Authors
  1. Dominik Steenken
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Heike Wehrheim
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Daniel Wonisch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Mathematics and Computer Science, University of São Paulo, Avenida Trabalhador, são carlense, 400, 13566-590, São Carlos, SP, Brazil

    Adenilso Simao

  2. School of Computer Science and Engineering, University of New South Wales, NSW 2052, Sydney, Australia

    Carroll Morgan

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Steenken, D., Wehrheim, H., Wonisch, D. (2011). Sound and Complete Abstract Graph Transformation. In: Simao, A., Morgan, C. (eds) Formal Methods, Foundations and Applications. SBMF 2011. Lecture Notes in Computer Science, vol 7021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25032-3_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-25032-3_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-25031-6

  • Online ISBN: 978-3-642-25032-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation