Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Bauer, Jörg; Wilhelm, Reinhard License: Creative Commons Attribution 4.0 license (CC BY 4.0)
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-7039


Abstract Interpretation of Graph Transformation



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

  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 =		{},
  URN =		{urn:nbn:de:0030-drops-7039},
  doi =		{10.4230/DagSemProc.06161.5},
  annote =	{Keywords: Abstract Interpretation, Graph Transformation}

Keywords: Abstract Interpretation, Graph Transformation
Seminar: 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