On the Use of Alloy to Analyze Graph Transformation Systems
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.
- 4.Baldan, P., König, B.: Approximating the behaviour of graph transformation systems. In: Proceedings of ICGT, pp. 14–29 (2002)Google Scholar
- 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.Beyer, M.: AGG1.0 - Tutorial. Technical University of Berlin, Department of Computer Science (1992)Google Scholar
- 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
- 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
- 15.Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)Google Scholar