Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(4)
Graph Transformation
Software Systems
Structural Model
First Order Logic
Related Publications
(5)
A Static Analysis Technique for Graph Transformation Systems
Realizing Graph Transformations by Pre and Postconditions and Command Sequences
Towards Automated Formal Verification of Visual Modeling Languages by Model Checking
Model Checking G...
Automated formal verification of visual modeling languages by model checking
Subscribe
Academic
Publications
On the Use of Alloy to Analyze Graph Transformation Systems
On the Use of Alloy to Analyze Graph Transformation Systems,10.1007/11841883_22,Luciano Baresi,Paola Spoletini
Edit
On the Use of Alloy to Analyze Graph Transformation Systems
(
Citations: 17
)
BibTex

RIS

RefWorks
Download
Luciano Baresi
,
Paola Spoletini
This paper proposes a methodology to analyze graph trans formation systems by means of Alloy and its supporting tools. Alloy is a simple structural modeling language, based on firstorder 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 userconstrained 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.
Conference:
Graph Grammars Workshops  GG
, pp. 306320, 2006
DOI:
10.1007/11841883_22
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.springerlink.com
)
(
www.informatik.unitrier.de
)
(
home.dei.polimi.it
)
(
dscpi.uninsubria.it
)
(
dx.doi.org
)
More »
Citation Context
(13)
...On the other hand, as Alloy supports model checking, we would be able to check more complex properties on sequences of rule flrings [
5
]...
...In [
5
], rules are translated into Alloy in order to study the applicability of sequences of rules and the reachability of models...
...Even though Alloy is equipped with a SAT solver (so that similar properties to the ones we verify could be analysed), the properties in [
5
] are only related to reachability...
Jordi Cabot
,
et al.
A UML/OCL framework for the analysis of graph transformation rules
...
Baresi and Spoletini (2006)
described a proposal to verify graph transformation systems by means of Alloy (Jackson, 2006) based on first order logic...
Vahid Rafe
,
et al.
Towards automated software model checking using graph transformation s...
...For example, in [
2
] rules are translated into Alloy in order to study the applicability of sequences of rules and the reachability of models in [1] rules are translated into Petri nets to check safety properties in [46] they are transformed into Promela for modelchecking and in [9, 10] rules are transformed into OCL preconditions and postconditions for rule analysis (e.g...
José Eduardo Rivera
,
et al.
Formal Specification and Analysis of Domain Specific Models Using Maud...
...Graph transformations (described using AGG) can be transformed into an Alloy Model [
9
]...
...Additionally, Baresi and Spoletini [
9
] demonstrated how the Alloy tools can be used in graph transformation systems...
Zekai Demirezen
,
et al.
Verification of DSMLs using graph transformation: a case study with Al...
...For example, Baresi et al [
13
] demonstrate how the Alloy [14] tools can be used in graph transformation systems...
...Graph transformations (described using AGG) can be transformed into an Alloy Model [
13
]...
Zekai Demirezen
.
Semantic framework for DSLs
References
(17)
Reasoning about static and dynamic properties in alloy: A purely relational approach
(
Citations: 15
)
Marcelo F. Frias
,
Carlos G. López Pombo
,
Gabriel A. Baum
,
Nazareno M. Aguirre
,
Thomas S. E. Maibaum
Journal:
ACM Transactions on Software Engineering and Methodology  TOSEM
, vol. 14, no. 4, pp. 478526, 2005
Integrating Model Checking and Theorem Proving for Relational Reasoning
(
Citations: 19
)
Konstantine Arkoudas
,
Sarfraz Khurshid
,
Darko Marinov
,
Martin C. Rinard
Conference:
Relational Methods in Computer Science  RelMiCS
, pp. 2133, 2003
Compositional Verification of Reactive Systems Specified by Graph Transformation
(
Citations: 36
)
Reiko Heckel
,
Corso Italia
Conference:
Fundamental Approaches to Software Engineering  FASE
, pp. 138153, 1998
CheckVML: A Tool for Model Checking Visual Modeling Languages
(
Citations: 34
)
Ákos Schmidt
,
Dániel Varró
Conference:
The Unified Modeling Language  UML
, pp. 9295, 2003
Verification of Distributed ObjectBased Systems
(
Citations: 19
)
Fernando Luís Dotti
,
Luciana Foss
,
Leila Ribeiro
,
Osmar Marchi Dos Santos
Conference:
Formal Methods for Open ObjectBased Distributed Systems  FMOODS
, pp. 261275, 2003
Sort by:
Citations
(17)
Verification and validation of declarative modeltomodel transformations through invariants
(
Citations: 6
)
Jordi Cabot
,
Robert Clarisó
,
Esther Guerra
,
Juan De Lara
Journal:
Journal of Systems and Software  JSS
, vol. 83, no. 2, pp. 283302, 2010
A UML/OCL framework for the analysis of graph transformation rules
(
Citations: 2
)
Jordi Cabot
,
Robert Clarisó
,
Esther Guerra
,
Juan de Lara
Journal:
Software and System Modeling  SOSYM
, vol. 9, no. 3, pp. 335357, 2010
Towards a Rewriting Logic Semantics for ATL
(
Citations: 2
)
Javier Troya
,
Antonio Vallecillo
Conference:
International Conference on Model Transformation  ICMT
, pp. 230244, 2010
Towards automated software model checking using graph transformation systems and Bogor
(
Citations: 1
)
Vahid Rafe
,
Adel T. Rahmani
Journal:
Journal of Zhejiang University Science
, vol. 10, no. 8, pp. 10931105, 2009
Formal Specification and Analysis of Domain Specific Models Using Maude
José Eduardo Rivera
,
Francisco Durán
,
Antonio Vallecillo
Journal:
Transactions of The Society for Modeling and Simulation International  SIMULATION
, vol. 85, no. 1112, pp. 778792, 2009