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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Baresi, L., & Spoletini, P. (2006). On the use of alloy to analyze graph transformation systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4178 LNCS, pp. 306–320). Springer Verlag. https://doi.org/10.1007/11841883_22
Mendeley helps you to discover research relevant for your work.