On the Use of Alloy to Analyze Graph Transformation Systems

  • Luciano Baresi
  • Paola Spoletini
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4178)


This paper proposes a methodology to analyze graph transformation systems by means of Alloy and its supporting tools. Alloy is a simple structural modeling language, based on first-order logic, that allows the user to produce models of software systems by abstracting their key characteristics. The tools can generate instances of invariants, and check properties of models, on user-constrained representations of the world under analysis. The paper describes how to render a graph transformation system —specified using AGG— as an Alloy model and how to exploit its tools to prove significant properties of the system. Specifically, it allows the user to decide whether a given configuration (graph) can be obtained through a finite and bounded sequence of steps (invocation of rules), whether a given sequence of rules can be applied on an initial graph, and, given an initial graph and an integer n, which are the configurations that can be obtained by applying a sequence of n (particular) rules.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
    Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating model checking and theorem proving for relational reasoning. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 21–33. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Baldan, P., Corradini, A., König, B.: Verifying finite-state graph grammars: An unfolding-based approach. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 83–98. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Baldan, P., König, B.: Approximating the behaviour of graph transformation systems. In: Proceedings of ICGT, pp. 14–29 (2002)Google Scholar
  5. 5.
    Baresi, L., Heckel, R.: Tutorial Introduction to Graph Transformation: A Software Engineering Perspective. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 402–429. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Baresi, L., Heckel, R., Thöne, S., Varró, D.: Modeling and validation of service-oriented architectures: Application vs. style. In: Proceedings of European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 68–77. ACM Press, New York (2003)Google Scholar
  7. 7.
    Beyer, M.: AGG1.0 - Tutorial. Technical University of Berlin, Department of Computer Science (1992)Google Scholar
  8. 8.
    Csertán, G., Huszerl, G., Majzik, I., Pap, Z., Pataricza, A., Varró, D.: Viatra - visual automated transformations for formal verification and validation of UML models. In: Proceedings of ASE, pp. 267–270 (2002)Google Scholar
  9. 9.
    Dotti, F.L., Foss, L., Ribeiro, L., Marchi dos Santos, O.: Verification of distributed object-based systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 261–275. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Frias, M., Lopez Pombo, C., Baum, G., Aguirre, N., Maibaum, T.: Reasoning about static and dynamic properties in alloy: A purely relational approach. ACM Trans. Softw. Eng. Methodol. 14(4), 478–526 (2005)CrossRefGoogle Scholar
  11. 11.
  12. 12.
    Hausmann, J.H., Heckel, R., Taentzer, G.: Detection of conflicting functional requirements in a use case-driven approach: a static analysis technique based on graph transformation. In: Proceedings of ICSE, pp. 105–115 (2002)Google Scholar
  13. 13.
    Heckel, R.: Compositional verification of reactive systems specified by graph transformation. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 138–153. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  14. 14.
    Holzmann, G.J.: The model checker spin. IEEE Trans. Software Eng. 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  15. 15.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)Google Scholar
  16. 16.
    Jackson, D., Shlyakhter, I., Sridharan, M.: A micromodularity mechanism. In: Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 62–73. ACM Press, New York (2001)CrossRefGoogle Scholar
  17. 17.
    Kuske, S.: A formal semantics of UML state machines based on structured graph transformation. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, p. 241. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    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
  19. 19.
    Rensink, A., Schmidt, Á., Varró, D.: Model checking graph transformations: A comparison of two approaches. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 226–241. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    Schmidt, Á., 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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Luciano Baresi
    • 1
  • Paola Spoletini
    • 1
  1. 1.Dipartimento di Elettronica e InformazionePolitecnico di MilanoMilanoItaly

Personalised recommendations