The Verigraph System for Graph Transformation

  • Guilherme Grochau Azzi
  • Jonas Santos Bezerra
  • Leila Ribeiro
  • Andrei Costa
  • Leonardo Marques Rodrigues
  • Rodrigo MachadoEmail author
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10800)


Graph transformation (GT) is a rule-based framework, suitable for modelling both static and dynamic aspects of complex systems in an intuitive yet formal manner. The algebraic approach to GT is based on category theory, allowing the instantiation of theoretical results to multiple graph-like structures (e.g. labelled or attributed graphs, Petri nets, even transformation rules themselves). There exists a rich theory of algebraic GT which underlies verification techniques such as static analysis. Current tools based on GT are implemented in a very concrete way, unlike the theory, making them hard to extend with novel theoretical results. Thus a new software system called Verigraph was created, with the goal of implementing the theory as closely as possible, while maintaining a reasonable execution time. In this paper we present the architecture of Verigraph, which enabled an almost direct implementation of the theory. We also provide a step-by-step guide to implementing a new graph model within the system, using second-order graph transformation as an example. Finally, we compare the performance of Verigraph and AGG.


Graph transformation Software system Static analysis 


  1. 1.
    Anjorin, A., Lauder, M., Patzina, S., Schürr, A.: eMoflon: leveraging EMF and professional CASE tools. Informatik 192, 281 (2011)Google Scholar
  2. 2.
    Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: advanced concepts and tools for In-Place EMF model transformations. In: Petriu, D.C., Rouquette, N., Haugen, Ø. (eds.) MODELS 2010. LNCS, vol. 6394, pp. 121–135. Springer, Heidelberg (2010). CrossRefGoogle Scholar
  3. 3.
    Bezerra, J.S., Costa, A., Ribeiro, L., Cota, É.F.: Formal verification of health assessment tools: a case study. Electron. Notes Theor. Comput. Sci. 324, 31–50 (2016)CrossRefGoogle Scholar
  4. 4.
    Braatz, B., Ehrig, H., Gabriel, K., Golas, U.: Finitary M-adhesive categories. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 234–249. Springer, Heidelberg (2010). CrossRefGoogle Scholar
  5. 5.
    Corradini, A., Duval, D., Echahed, R., Prost, F., Ribeiro, L.: AGREE – algebraic graph rewriting with controlled embedding. In: Parisi-Presicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 35–51. Springer, Cham (2015). CrossRefGoogle Scholar
  6. 6.
    Corradini, A., Heindel, T., Hermann, F., König, B.: Sesqui-pushout rewriting. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 30–45. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  7. 7.
    Costa, A., Bezerra, J., Azzi, G., Rodrigues, L., Becker, T.R., Herdt, R.G., Machado, R.: Verigraph: a system for specification and analysis of graph grammars. In: Ribeiro, L., Lecomte, T. (eds.) SBMF 2016. LNCS, vol. 10090, pp. 78–94. Springer, Cham (2016). CrossRefGoogle Scholar
  8. 8.
    Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. Springer, Heidelberg (2006). zbMATHGoogle Scholar
  9. 9.
    Ehrig, H., Pfender, M., Schneider, H.J.: Graph-grammars: an algebraic approach. In: Switching and Automata Theory, pp. 167–180 (1973)Google Scholar
  10. 10.
    Ehrig, H., Golas, U., Hermann, F., et al.: Categorical frameworks for graph transformation and HLR systems based on the DPO approach. Bull. EATCS 102, 111–121 (2010)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Ehrig, H., Habel, A., Padberg, J., Prange, U.: Adhesive high-level replacement categories and systems. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 144–160. Springer, Heidelberg (2004). CrossRefGoogle Scholar
  12. 12.
    Geiß, R., Batz, G.V., Grund, D., Hack, S., Szalkowski, A.: GrGen: a fast SPO-based graph rewriting tool. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 383–397. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  13. 13.
    Klassen, L., Wagner, R.: EMorF - a tool for model transformations. Electron. Commun. EASST 54, 1–6 (2012)Google Scholar
  14. 14.
    Lack, S., Sobociński, P.: Adhesive and quasiadhesive categories. RAIRO - Theor. Inf. Appl. 39(3), 511–545 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Lambers, L.: Certifying rule-based models using graph transformation. Ph.D. thesis, Elektrotechnik und Informatik der Technischen Universität Berlin (2010)Google Scholar
  16. 16.
    Machado, R.: Higher-order graph rewriting systems. Ph.D. thesis, Instituto de Informática - Universidade Federal do Rio Grande do Sul (2012)Google Scholar
  17. 17.
    Machado, R., Ribeiro, L., Heckel, R.: Rule-based transformation of graph rewriting rules: towards higher-order graph grammars. Theor. Comput. Sci. 594, 1–23 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Manning, G., Plump, D.: The GP programming system. Electron. Commun. EASST 10, 1–13 (2008)CrossRefGoogle Scholar
  19. 19.
    Marlow, S.: Haskell 2010 language report (2010).
  20. 20.
    Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007). CrossRefGoogle Scholar
  21. 21.
    Poskitt, C.M.: Verification of graph programs. Ph.D. thesis, University of York (2013)Google Scholar
  22. 22.
    Rensink, A.: The GROOVE simulator: a tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004). CrossRefGoogle Scholar
  23. 23.
    Ribeiro, L.: Parallel composition and unfolding semantics of graph grammars. Ph.D. thesis, Technical University of Berlin (1996)Google Scholar
  24. 24.
    Rozenberg, G.: Handbook of Graph Grammars and Computing by Graph Transformation: Volume 1, Foundations. World Scientific Publishing Co., Inc., River Edge (1997)CrossRefzbMATHGoogle Scholar
  25. 25.
    Schürr, A.: Specification of graph translators with triple graph grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol. 903, pp. 151–163. Springer, Heidelberg (1995). CrossRefGoogle Scholar
  26. 26.
    Taentzer, G.: AGG: a tool environment for algebraic graph transformation. In: Nagl, M., Schürr, A., Münch, M. (eds.) AGTIVE 1999. LNCS, vol. 1779, pp. 481–488. Springer, Heidelberg (2000). CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Instituto de InformáticaUniversidade Federal do Rio Grande do SulPorto AlegreBrazil

Personalised recommendations