TU Darmstadt / ULB / TUprints

A Compass to Controlled Graph Rewriting

Kulcsár, Géza (2019):
A Compass to Controlled Graph Rewriting.
Darmstadt, Technische Universität, [Ph.D. Thesis]

[img]
Preview
Text
2019-10-08-KULCSAR-GEZA.pdf - Accepted Version
Available under CC-BY-SA 4.0 International - Creative Commons, Attribution Share-alike.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Title: A Compass to Controlled Graph Rewriting
Language: English
Abstract:

With the growing complexity and autonomy of software-intensive systems, abstract modeling to study and formally analyze those systems is gaining on importance. Graph rewriting is an established, theoretically founded formalism for the graphical modeling of structure and behavior of complex systems. A graph-rewriting system consists of declarative rules, providing templates for potential changes in the modeled graph structures over time. Nowadays complex software systems, often involving distributedness and, thus, concurrency and reactive behavior, pose a challenge to the hidden assumption of global knowledge behind graph-based modeling; in particular, describing their dynamics by rewriting rules often involves a need for additional control to reflect algorithmic system aspects. To that end, controlled graph rewriting has been proposed, where an external control language guides the sequence in which rules are applied. However, approaches elaborating on this idea so far either have a practical, implementational focus without elaborating on formal foundations, or a pure input-output semantics without further considering concurrent and reactive notions.

In the present thesis, we propose a comprehensive theory for an operational semantics of controlled graph rewriting, based on well-established notions from the theory of process calculi. In the first part, we illustrate the aforementioned fundamental phenomena by means of a simplified model of wireless sensor networks (WSN). After recapitulating the necessary background on DPO graph rewriting, the formal framework used throughout the thesis, we present an extensive survey on the state of the art in controlled graph rewriting, along the challenges which we address in the second part where we elaborate our theoretical contributions. As a novel approach, we propose a process calculus for controlled graph rewriting, called RePro, where DPO rule applications are controlled by process terms closely resembling the process calculus CCS. In particular, we address the aforementioned challenges: (i) we propose a formally founded control language for graph rewriting with an operational semantics, (ii) explicitly addressing concurrency and reactive behavior in system modeling, (iii) allowing for a proper handling of process equivalence and action independence using process-algebraic notions.

Finally, we present a novel abstract verification approach for graph rewriting based on abstract interpretation of reactive systems. To that end, we propose the so-called compasses as an abstract representation of infinite graph languages and demonstrate their use for the verification of process properties over infinite input sets.

Alternative Abstract:
Alternative AbstractLanguage
Heutzutage, die Relevanz abstrakter Modellierungsansätze für die formale Analyse komplexer Rechnersysteme gewinnt durch wachsende Komplexität und Autonomie auch zunehmend an Bedeutung. Graphersetzungssysteme stellen einen etablierten, theoretisch fundierten Formalismus zur Modellierung der graphischen Struktur und des Verhaltens solcher Systeme dar. Ein Graphersetzungssystem besteht aus deklarativen Regeln, die als Vorlage für potentielle Änderungen während der Evolution der modellierten Systemstruktur fungieren. Darüber hinaus stellen heutige komplexe Softwaresysteme oft zusätzliche Anforderungen bezüglich Nebenläufigkeitseigenschaften und reaktivem Verhalten dar, welche oft mit der verborgenen Annahme, dass die graphische Abstraktion das System vollständig repräsentiert, kollidieren. Insbesondere fordert die Beschreibung der dynamischen Systemaspekte oft zusätzliche externe Kontrollkonstrukte zur Steuerung der Anwendung von Graphersetzungs-Regeln. Um diese Herausforderungen anzugehen, kontrollierte Graphersetzungssysteme wurden in der Literatur vorgeschlagen, versehen mit einer externen Kontrollsprache für die Beschreibung der zugelassenen Regelsequenzen. Allerdings haben bisherige Ansätze entweder einen starken Fokus auf die Implementierung ohne näher auf formale Grundlagen einzugehen, oder sie beschränken sich auf eine reine Ein-/Ausgabe-Semantik ohne tiefergehende Betrachtung reaktiven und nebenläufigen Verhaltens. In der vorliegenden Arbeit schlagen wir daher eine ganzheitliche Theorie zur Formalisierung einer operationellen Semantik von kontrollierter Graphersetzung vor. Dabei verwenden wir etablierte Begriffe und Resultate der Theorie nebenläufiger Prozess-Kalküle als Grundlage für die Spezifikation unserer Kontrollsprache. Im ersten Teil der Arbeit illustrieren wir zunächst die vorgehende fundamentale Phänomene anhand eines simplifizierten Modells für drahtlose Sensornetzwerke (wireless sensor networks, WSN). Nachdem wir die Grundlagen der sog. DPO-Graphersetzung rekapituliert haben, präsentieren wir einen ausführlichen Überblick über bisherige Ansätze und offene Probleme im Bereich, und leiten daraus die für uns anstehende Herausforderungen ab. Im zweiten Teil präsentieren wir unsere theoretische Hauptresultate: wir schlagen ein Prozess-Kalkül namens RePro für kontrollierte Graphersetzung vor. In RePro werden Sequenzen von möglichen DPO-Regelanwendungen eingeschränkt durch die Transitionen eines zusätzlichen Kontrollprozesses, dessen Syntax und Semantik an das Prozess-Kalkül CCS angelehnt ist. Insbesondere betrachten wir die folgenden Herausforderungen: (i) RePro stellt eine formal fundierte Kontrollsprache mit einer operationellen Semantik, (ii) die auch Nebenläufigkeit und reaktives Verhalten explizit adressiert und (iii) das Definition formaler Begriffe für Prozessäquivalenz und Unabhängigkeit von Aktionen ermöglicht. Zum Schluss wird auf diesen Grundlagen ein Ansatz zur symbolischen Verifikation dieser Prozesse vorgestellt, basierend auf das Rahmenwerk der abstrakten Interpretation (abstract interpretation). Hierfür schlagen wir sog. Kompasse (compasses) als abstrakte Repräsentation unendlicher Graphmengen vor, und demonstrieren ihre Eignung zur Verifikation gewisser Prozesseigenschaften für unendliche Eingabemengen.German
Place of Publication: Darmstadt
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: 18 Department of Electrical Engineering and Information Technology > Institute of Computer Engineering > Real-Time Systems
Date Deposited: 22 Nov 2019 13:17
Last Modified: 09 Jul 2020 02:50
URN: urn:nbn:de:tuda-tuprints-93049
Referees: Schürr, Prof. Dr. Andy and Corradini, Prof. Dr. Andrea
Refereed: 7 June 2019
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/9304
Export:
Actions (login required)
View Item View Item