Im Bereich der modellgetriebenen Softwareentwicklung ist der Gebrauch von visuellen Modellierungssprachen weit verbreitet. Eine Anwendung solcher Modellierungssprachen ist die Spezifikation von strukturell dynamischen Systemen, also solchen Systemen die in der Lage sind, ihre strukturelle Konfiguration zur Laufzeit zu ändern. Um nützlich zu sein, müssen solche Systeme bestimmten Qualitätsanforderungen genügen, wie etwa die Eigenschaft, dass potenziell gefährliche Konfigurationen von dem System nicht generiert werden können. Wenn modellgetriebene Softwareentwicklung eine gangbare Alternative zur klassischen Softwareentwicklung darstellen soll, muss sie mit formalen Methoden untermauert werden, um eine automatische Überprüfung solcher Qualitätsanforderungen auf der Modellebene zu ermöglichen. Die naheliegendste Formalisierung von strukturell dynamischen Systemen ist das mathematische Konzept der Graphtransformationssysteme. Die formale Verifikation solcher Systeme stellt eine Herausforderung dar, da sie häufig unendlich große Zustandsräume aufweisen, d.h. sie sind in der Lage, eine unendliche Vielfalt unterschiedlicher Konfigurationen zu erzeugen. In dieser Arbeit entwickeln wir eine neue Methode um Graphtransformationssysteme mit unendlichem Zustandsraum mittels einer endlichen Abstraktion auf ihre Fähigkeit, potenziell gefährliche Konfigurationen zu erzeugen, zu überprüfen. Das Ergebnis ist eine Methode die eine hoch flexible Analyse von Graphtransformationssystemen mit unendlichem Zustandsraum erlaubt. Sie stellt daher einen Beitrag zum Gebiet der Verifikation komplexer, strukturell dynamischer Systeme im Kontext der modellgetriebenen Softwareentwicklung dar. Wir stellen eine prototypische Implementation, sowie erste experimentelle Ergebnisse vor.

In the field of model-driven software development (MDSD), the use of visual modeling languages is abundant. One particular application of such modeling languages is the specification of structurally dynamic systems, i.e. systems that are able to dynamically change their structural configuration at run-time. To be useful, such systems must adhere to certain quality constraints, such as the inability to produce configurations that are deemed dangerous.If MDSD is to be a viable alternative to traditional software development, it must be firmly grounded in formal methods, so as to support the automatic checking of such quality constraints at the model level. The natural formalization of structurally dynamic systems is the mathematical notion of graph transformation systems. The formal verification of such systems poses a challenge, since they often exhibit infinite state spaces, i.e. they are able to generate an unbounded variety of different configurations.In this thesis, we develop a new way to check infinite-state graph transformation systems for their capacity to produce potentially dangerous configurations using finite abstractions. In order to do so, we adapt established methods from other fields of verification to the graph transformation domain.The result is a method that allows for a highly flexible analysis of infinite-state graph transformation systems and thus represents a contribution to the verification of complex, structurally dynamic systems in the context of MDSD. We present a proof-of-concept implementation and report on first experimental results.