Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26631
Titel: Cluster abstraction of graph transformation systems
Sonstige Titel: Cluster-Abstraktion von Graphtransformationssystemen
Verfasser: Backes, Peter
Sprache: Englisch
Erscheinungsjahr: 2015
SWD-Schlagwörter: Abstrakte Interpretation
Graphersetzungssystem
statische Analyse
Freie Schlagwörter: Graphtransformation
parametrisierte Verifikation
verteilte nachrichtenbasierte Systeme
graph transformation
abstract interpretation
parameterized verification
shape analysis
distributed message-passing systems
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: This dissertation explores the problem of analyzing the reachable graphs of graph transformation systems. Such systems rewrite graphs according to subgraph replacement rules; we allow negative application conditions to be specified in addition. This problem is hard because the number of reachable graphs is potentially unbounded. We use abstract interpretation to compute a finite, overapproximated representation of the reachable graphs. The main idea is the notion of a cluster: We abstract the graph locally for each of its nodes such that we obtain a bounded cluster with the node and its immediate neighborhood. Then, we eliminate duplicate clusters such that we obtain a bounded abstraction for the entire graph. We lift concrete rule application to this abstraction, eventually obtaining an overapproximation of all reachable graphs. We present ASTRA, an implementation of cluster abstraction, and the merge protocol from car platooning, our main test case. This protocol enables autonomous cars to form and merge platoons consisting of a leader car and several followers, such that the leader controls speed and lane. The abstraction does well with the merge protocol, and also manages to analyze several other standard case studies from the literature, as well as test cases automatically generated from a higher-level formalism.
Diese Dissertation untersucht, wie sich die erreichbaren Graphen eines Graphtransformationssystems analysieren lassen. Solche Systeme verändern Graphen gemäß Teilgraphersetzungsregeln; wir lassen zusätzlich negative Anwendungsbedingungen zu. Dieses Problem ist schwierig, da die Anzahl der erreichbaren Graphen potentiell unbeschränkt ist. Wir benutzen abstrakte Interpretation, um eine endliche überapproximierte Darstellung der erreichbaren Graphen zu berechnen. Die Hauptidee ist der Begriff des Clusters: Wir abstrahieren den Graphen lokal für jeden seiner Knoten und erhalten einen Cluster beschränkter Größe mit diesem Knoten und seiner direkten Umgebung. Dann eliminieren wir doppelte Cluster, so dass wir eine Abstraktion beschränkter Größe für den gesamten Graphen erhalten. Wir führen dann die Regelanwendung auf dieser Abstraktion durch, wodurch wir letztlich eine Überapproximation aller erreichbaren Graphen erhalten. Wir betrachten ASTRA, eine Implementierung der Cluster-Abstraktion, und als Hauptbeispiel das Merge-Protokoll aus dem Bereich automatisierter Kolonnenfahrten. Bei diesem Protokoll werden Kolonnen durch autonom fahrende Autos gebildet und verschmolzen, so dass das Führungsfahrzeug Geschwindigkeit und Spur kontrolliert. Die Abstraktion analysiert das gesamte Merge-Protokoll, mehrere weitere Standardfallbeispiele aus der Literatur, und auch Fallbeispiele, die aus einem Formalismus höherer Ordnung automatisch generiert wurden.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-63078
hdl:20.500.11880/26687
http://dx.doi.org/10.22028/D291-26631
ISBN der Druckausgabe: 978-3-7375-7665-9
Erstgutachter: Wilhelm, Reinhard
Tag der mündlichen Prüfung: 13-Nov-2015
SciDok-Publikation: 30-Nov-2015
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
thesis.pdf942 kBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.