License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.06161.5
URN: urn:nbn:de:0030-drops-7039
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/703/
Go to the corresponding Portal

Bauer, Jörg ; Wilhelm, Reinhard

Abstract Interpretation of Graph Transformation

pdf-format:
06161.BauerJoerg.ExtAbstract.703.pdf (0.2 MB)

Abstract

The semantics of many dynamic systems can be described by evolving
graphs. Graph transformation systems (GTS) are a natural,
intuitive, and formally defined method to specify
systems of evolving graphs, whereas verification techniques for GTS
are scarce.

We present an abstract interpretation based approach for
GTS verification. Single graphs are abstracted in two steps.
First similar nodes within a connected component, then
similar abstracted connected components are summarized.

Transformation rules are applied directly to abstract graphs
yielding a bounded set of abstract graphs of bounded size that
over-approximates the concrete GTS and can be used for
further verification.

Since our abstraction is homomorphic, existential positive properties
are preserved under abstraction. Furthermore, we identify
automatically checkable completeness criteria for the abstraction.
The technique is implemented and successfully tested on the platoon
case study.

BibTeX - Entry

@InProceedings{bauer_et_al:DagSemProc.06161.5,
  author =	{Bauer, J\"{o}rg and Wilhelm, Reinhard},
  title =	{{Abstract Interpretation of Graph Transformation}},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6161},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/703},
  URN =		{urn:nbn:de:0030-drops-7039},
  doi =		{10.4230/DagSemProc.06161.5},
  annote =	{Keywords: Abstract Interpretation, Graph Transformation}
}

Keywords: Abstract Interpretation, Graph Transformation
Collection: 06161 - Simulation and Verification of Dynamic Systems
Issue Date: 2006
Date of publication: 07.09.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI