Abstract:

Die vorliegende Diplomarbeit befasst sich mit erkennbaren Graphsprachen und der Frage wie diese für die Spezifikation von Invarianten verwendet werden können. Die grundlegende Ansatz hierbei ist, dass viele Systeme, darunter beispielsweise verteilte Systeme, die aus mehreren untereinander verbundenen Komponenten bestehen, in ihrer statischen Form als Graphen beschrieben werden können. Die Dynamik solcher Systeme kann durch Graphtransformationsregeln spezifiziert werden, die sowohl das Entstehen und Verschwinden von Komponenten, als auch die Umstrukturierung der Topologie beschreiben können. Ausgehend von den regulären Wortsprachen in Kombination mit Zeichenersetzungsregeln wird das Konzept der Invarianten auf Graphsprachen in Zusammenhang mit Graphtransformationsregeln erweitert. Dazu wird das Theorem, welches besagt, dass eine Wortsprache genau dann regulär ist, wenn sie bezüglich einer monotonen Wohlquasiordnung nach oben abgeschlossen ist, entsprechend für erkennbare Graphsprachen verallgemeinert. Aufbauend auf diesen Ergebnissen wird zunächst ein Algorithmus zur Überprüfung von Invarianten bei Wortsprachen entwickelt, der anschließend als Grundlage für einen entsprechenden Algorithmus dient, der auf Graphsprachen anwendbar ist. Anhand dieses Algorithmus’ können erkennbare Graphsprachen daraufhin untersucht werden, ob sie invariant unter der Anwendung einer Graphtransformation sind. Für die Untersuchung der praktischen Realisierbarkeit wird parallel zu den theoretischen Überlegungen ein Programm entwickelt, welches den Algorithmus zum Überprüfen von Invarianten bei erkennbaren Graphsprachen implementiert. Mit Hilfe dieses Programms werden anhand eines Fallbeispiels, bei dem die Zugriffsregeln eines Mehrbenutzersystems verifiziert werden sollen, die Einsatzmöglichkeiten der vorgestellten Theorien aufgezeigt.