Durch die Komplexität heutiger Softwaresysteme und Hardwaresysteme und den vermuteten Anstieg der Zahl autonomer und intelligenter Systeme bleibt die Entwicklung korrekter Systeme eine wichtige Herausforderung. Obwohl Testen ein wichtiger Teil des Entwicklungszyklusses ist und bleibt, reichen Tests üblicherweise nicht aus, um die Korrektkeit eines Systems sicherzustellen. Formale Verifikation nimmt sich dieses Problems an: Nach Darstellung eines Systems in einem mathematischen Formalismus können Verifikationsansätze und Werkzeuge angewendet werden, um zu analysieren, ob das System seine Kernaufgabe und seine Sicherheitsanforderungen erfüllt. Ein solcher mathematischer Formalismus sind Graphen, die netzwerkartige Strukturen darstellen können. Knoten stellen Elemente eines wie auch immer gearteten Systems dar; Kanten verbinden Knoten und stellen deren Beziehungen zueinander dar. Sogenannte Graphtransformationen beschreiben dann, wie sich Knoten und Kanten verändern können. Auf Basis mathematischer Grundlagen stellt diese Arbeit einen automatischen Verifikationsansatz vor, der Sicherheitsanforderungen von Systemen überprüfen kann, die sich als Graphen und Graphtransformationen abstrahieren lassen. Die Korrektheit des Ansatzes wird mathematisch bewiesen. Eine Implementierung der Technik und deren Evaluierung anhand diverser Beispiele weisen nach, dass der Ansatz für die ausgewerteten Beispiele anwendbar ist und korrekte Ergebnisse in vernachlässigbarer Zeit liefert.
