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.