Static Verification Techniques for Attributed Graph Transformations

Deckwerth, Frederik (2017)
Static Verification Techniques for Attributed Graph Transformations.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

URL / URN: http://tuprints.ulb.tu-darmstadt.de/6150

Kurzbeschreibung (Abstract)

Graph transformation with its formal foundations and its broad range of theoretical results, on the one hand, and competitive tool support, on the other hand, constitutes an effective framework for model-driven software development. Within the last decade, the theory of algebraic graph transformations has been developed towards a comprehensive formal framework including several sophisticated results on modeling, analysing, and verifying graph transformation systems. Prominent theoretical results are the static verification of consistency constraints as well as static conflict detection and conflict resolution techniques. Consistency constraints provide means to declaratively define global assertions that must remain true. Conflict detection and resolution techniques provide means to statically discover potential unintended interactions of graph transformations.

Based on the framework for algebraic graph transformations several model transformation tools were developed over the last years. However, in order to become suitable for the practical needs in every-day software engineering, these tool oriented graph transformation approaches integrate language concepts that go beyond the simple manipulation of plain graphs. An important concept is the treatment of data values such as integers, booleans, and strings. The integration of primitive data attributes within the graph structure is indispensable to model almost all realistic systems, since they combine the structural aspects of a system with data aspects such as computations of values. While in the last years, many advanced language concepts were adapted from the tool oriented approaches and integrated within the theory of algebraic graph transformations, there is currently no theoretical approach that appropriately reflects the de-facto data attribute handling approach of practical implementations. Thus, the main body of theoretical results does not immediately apply to those implemented approaches. As a result, current tool support for analysis and verification techniques of attributed graph transformation systems is rather limited.

This thesis attempts to close this gap. To this end, a framework for attributed graph transformation systems is proposed. In contrast to existing approaches, the proposed framework reflects more closely the attribute handling of current state of the art graph transformation implementations. We show that our proposed approach preserves the fundamental theoretical results of the algebraic approach for graph transformations. Additionally, we verify the well-known results for the static verification of consistency constraints, conflict detection, and conflict resolution by confluence analysis within our framework. Finally, a prototypical implementation is provided to show that the theoretical concepts can be realized. Moreover, to assess its potential for analyzing real world applications, the prototype is applied to analyze a case study from the enterprise modeling domain.

Typ des Eintrags:

Dissertation

Erschienen:

2017

Autor(en):

Deckwerth, Frederik

Art des Eintrags:

Erstveröffentlichung

Titel:

Static Verification Techniques for Attributed Graph Transformations

Sprache:

Englisch

Referenten:

Schürr, Prof. Dr. Andy ; Annegret, Prof. Dr. Habel

Publikationsjahr:

2017

Ort:

Darmstadt

Datum der mündlichen Prüfung:

2 November 2016

URL / URN:

http://tuprints.ulb.tu-darmstadt.de/6150

Kurzbeschreibung (Abstract):

Alternatives oder übersetztes Abstract:

Alternatives Abstract

Sprache

Aufgrund der Vielzahl an formal fundierten theoretischen Resultaten bezüglich der Analyse und Verifikation von Softwaresystemen sowie der ausgereiften Werkzeugunterstützung, bieten Graphtransformationen ein effektives Werkzeug zur modellgetriebenen Entwicklung von Software. Innerhalb der letzten Jahre hat sich der algebraische Ansatz zur Formalisierung von Graphtransformationssystemen zu einem umfassenden Rahmenwerk zur Modellierung, Analyse und Verifikation entwickelt. Prominente Beispiele dafür sind die statische Verifikation von Konsistenzbedingungen sowie Techniken zur Konfliktdetektion und zur automatischen Konfliktauflösung. Konsistenzbedingungen sind ein Mittel zur deklarativen Beschreibung von Bedingungen, welche immer erfüllt sein müssen. Techniken für die Konfliktdetektion und Konfliktauflösung ermöglichen es, statisch die Interaktionen von einzelnen Graphtransformationsschritten zu analysieren um unbeabsichtigte Wechselbeziehungen aufzuspüren.

Darüber hinaus hat sich auf dieser Grundlage eine vielseitige Landschaft ausgereifter Graphtransformationswerkzeuge etabliert. Um jedoch den Anforderungen, welche sich bei der modellbasierten Entwicklung realer Systeme ergeben, gerecht zu werden, bieten alle modernen Graphtransformationswerkzeuge Sprachkonzepte, die über die reine Manipulation einfacher Graphstrukturen hinausgehen. In dieser Hinsicht ist die Einbettung von Datenattributen in Form von Zahlen oder Zeichenketten in die Graphstruktur sowie deren Manipulation in Form von Berechnungen eine der grundlegenden Erweiterungen für die Modellierung realer Softwaresysteme. Während es in den letzten Jahren gelang, viele dieser innovativen Sprachkonzepte aus der Welt der Graphtransformationswerkzeuge in das theoretische Rahmenwerk der algebraischen Graphtransformationen zu überführen, bildet die Einbettung von Datenattributen hier eine Ausnahme. So ist es bisher nicht gelungen, eine formale Repräsentation zu entwickeln, welche die praktische Behandlung von Datenattributen hinreichend widerspiegelt, um die theoretischen Resultate auf die Werkzeuge zu übertragen. Somit stellt diese Lücke zwischen den theoretischen Konzepten und der praktischen Umsetzung eine der Hauptursachen dar für die bis dato eingeschränkte Werkzeugunterstützung für die Analyse und Verifikation attributierter Graphtransformationssysteme. Im Rahmen dieser Dissertation soll diese Lücke geschlossen werden. Dazu wird ein Rahmenwerk zur Transformation attributierter Graphen beschrieben. Im Gegensatz zu existierenden Ansätzen bildet die vorgestellte Lösung die Bedingungen, wie sie für reale Implementierungen gelten, wesentlich genauer ab. Es wird gezeigt, dass die grundlegenden theoretischen Resultate des algebraischen Ansatzes auch in dem neuen Rahmenwerk gültig sind. Des Weiteren wird die Gültigkeit der bekannten Resultate zur Konsistenzverifikation sowie zur Konfliktdetektion und Konfluenz-Analyse in diesem Rahmenwerk gezeigt. Zum Schluss wird eine prototypische Implementierung vorgestellt und anhand einer Fallstudie gezeigt, dass die praktische Umsetzung der gezeigten theoretischen Resultate sich für die Analyse und Verifikation realer Systeme eignet.

Deutsch

URN:

urn:nbn:de:tuda-tuprints-61502

Sachgruppe der Dewey Dezimalklassifikatin (DDC):

000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik

Fachbereich(e)/-gebiet(e):

18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik > Echtzeitsysteme
LOEWE > LOEWE-Zentren > CASED – Center for Advanced Security Research Darmstadt
18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik
LOEWE > LOEWE-Zentren
18 Fachbereich Elektrotechnik und Informationstechnik
LOEWE

Hinterlegungsdatum:

07 Mai 2017 19:55

Letzte Änderung:

07 Mai 2017 19:55

PPN: