License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-7039
URL: http://drops.dagstuhl.de/opus/volltexte/2006/703/

Bauer, Jrg ; Wilhelm, Reinhard

Abstract Interpretation of Graph Transformation

pdf-format:
Dokument 1.pdf (191 KB)


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:DSP:2006:703,
  author =	{J{\"o}rg Bauer and Reinhard Wilhelm},
  title =	{Abstract Interpretation of Graph Transformation},
  booktitle =	{Simulation and Verification of Dynamic Systems},
  year =	{2006},
  editor =	{David M. Nicol and Corrado Priami and Hanne Riis Nielson and Adelinde M. Uhrmacher},
  number =	{06161},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2006/703},
  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 Published by LZI