Skip to main content
SpringerLink
Log in

Inductive Invariant Checking with Partial Negative Application Conditions

  • Conference paper
  • First Online:
Graph Transformation (ICGT 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9151))

Included in the following conference series:

Abstract

Graph transformation systems are a powerful formal model to capture model transformations or systems with infinite state space, among others. However, this expressive power comes at the cost of rather limited automated analysis capabilities. The general case of unbounded many initial graphs or infinite state spaces is only supported by approaches with rather limited scalability or expressiveness. In this paper we improve an existing approach for the automated verification of inductive invariants for graph transformation systems. By employing partial negative application conditions to represent and check many alternative conditions in a more compact manner, we can check examples with rules and constraints of substantially higher complexity. We also substantially extend the expressive power by supporting more complex negative application conditions and provide higher accuracy by employing advanced implication checks. The improvements are evaluated and compared with another applicable tool by considering three case studies.

This work was partially developed in the course of the project Correct Model Transformations II (GI 765/1–2), which is funded by the Deutsche Forschungsgemeinschaft.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

References

  1. Ghamarian, A.H., de Mol, M.J., Rensink, A., Zambon, E., Zimakova, M.V.: Modelling and analysis using GROOVE. Int. J. Softw. Tools Technol. Transf. 14(1), 15–40 (2012)

    Article  Google Scholar 

  2. Schmidt, A., Varró, D.: CheckVML: a tool for model checking visual modeling languages. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol. 2863, pp. 92–95. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  3. Boneva, I.B., Kreiker, J., Kurban, M.E., Rensink, A., Zambon, E.: Graph abstraction and abstract graph transformations (Amended version). Technical report TR-CTIT-12-26, Centre for Telematics and Information Technology, University of Twente, Enschede (2012)

    Google Scholar 

  4. Steenken, D.: Verification of infinite-state graph transformation systems via abstraction. Ph.D. thesis, University of Paderborn (2015)

    Google Scholar 

  5. König, B., Stückrath, J.: A general framework for well-structured graph transformation systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 467–481. Springer, Heidelberg (2014)

    Google Scholar 

  6. König, B., Kozioura, V.: Augur 2 - a new version of a tool for the analysis of graph transformation systems. In: Electronic Notes in Theoretical Computer Science, Proceedings of the Fifth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2006), vol. 211, pp. 201–210 (2008)

    Google Scholar 

  7. Blume, C., Bruggink, H.J.S., Engelke, D., König, B.: Efficient symbolic implementation of graph automata with applications to invariant checking. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 264–278. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  8. Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic invariant verification for systems with dynamic structural adaptation. In: Proceedings of the 28th International Conference on Software Engineering (ICSE), Shanghai, China. ACM Press (2006)

    Google Scholar 

  9. Pennemann, K.-H.: Development of correct graph transformation systems. Ph.D. thesis, Department of Computing Science, University of Oldenburg (2009)

    Google Scholar 

  10. Habel, A., Pennemann, K.-H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19, 1–52 (2009)

    Google Scholar 

  11. Giese, H., Lambers, L.: Towards automatic verification of behavior preservation for model transformation via invariant checking. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 249–263. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  12. Becker, B., Lambers, L., Dyck, J., Birth, S., Giese, H.: Iterative development of consistency-preserving rule-based refactorings. In: Cabot, J., Visser, E. (eds.) ICMT 2011. LNCS, vol. 6707, pp. 123–137. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Dyck, J., Giese, H.: Inductive invariant checking with partial negative application conditions, 98, Technical report, Hasso Plattner Institute at the University of Potsdam, Germany (2015)

    Google Scholar 

  14. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Secaucus (2006)

    Google Scholar 

  15. Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: M-Adhesive transformation systems with nested application conditions, part 1: parallelism, concurrency and amalgamation. Math. Struct. Comput. Sci. 24(4) (2014)

    Google Scholar 

  16. Hsu, A., Eskafi, F., Sachs, S., Varaiya, P.: The design of platoon maneuver protocols for IVHS. Technical report UCBITS-PRR-91-6, University of California, Berkley (1991)

    Google Scholar 

  17. Dyck, J., Giese, H., Lambers, L.: Automatic verification of behavior preservation for model transformation via invariant checking. Technical report, Hasso Plattner Institute at the University of Potsdam, Germany (2015, forthcoming)

    Google Scholar 

  18. Baldan, P., Corradini, A., König, B.: A static analysis technique for graph transformation systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 381–395. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Acknowledgments

We would like to thank the group of Annegret Habel, in particular the authors of the SeekSat/ProCon tool [9], for allowing us to do the comparison and Leen Lambers for her work on behavior preservation of model transformations.

Author information

Authors and Affiliations

  1. Hasso Plattner Institute at the University of Potsdam, Potsdam, Germany

    Johannes Dyck & Holger Giese

Authors
  1. Johannes Dyck
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Holger Giese
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Johannes Dyck .

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Sapienza Università di Roma, Rome, Italy

    Francesco Parisi-Presicce

  2. Angewandte Informatik 1, Universität Bayreuth, Bayreuth, Germany

    Bernhard Westfechtel

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Dyck, J., Giese, H. (2015). Inductive Invariant Checking with Partial Negative Application Conditions. In: Parisi-Presicce, F., Westfechtel, B. (eds) Graph Transformation. ICGT 2015. Lecture Notes in Computer Science(), vol 9151. Springer, Cham. https://doi.org/10.1007/978-3-319-21145-9_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-21145-9_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-21144-2

  • Online ISBN: 978-3-319-21145-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation