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.