TU Darmstadt / ULB / TUprints

Static Verification Techniques for Attributed Graph Transformations

Deckwerth, Frederik (2017)
Static Verification Techniques for Attributed Graph Transformations.
Technische Universität Darmstadt
Ph.D. Thesis, Primary publication

[img]
Preview
Text
Static Verification Techniques for Attributed Graph Transformations, Dissertation Frederik Deckwerth.pdf
Copyright Information: CC BY-ND 4.0 International - Creative Commons, Attribution NoDerivs.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Static Verification Techniques for Attributed Graph Transformations
Language: English
Referees: Schürr, Prof. Dr. Andy ; Annegret, Prof. Dr. Habel
Date: 2017
Place of Publication: Darmstadt
Date of oral examination: 2 November 2016
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.

Alternative Abstract:
Alternative AbstractLanguage

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.

German
URN: urn:nbn:de:tuda-tuprints-61502
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 18 Department of Electrical Engineering and Information Technology > Institute of Computer Engineering > Real-Time Systems
LOEWE > LOEWE-Zentren > CASED – Center for Advanced Security Research Darmstadt
Date Deposited: 04 May 2017 12:28
Last Modified: 09 Jul 2020 01:36
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/6150
PPN: 402782178
Export:
Actions (login required)
View Item View Item