Johannes Dyck Livres

Graphtransformationssysteme bieten einen ausdrucksstarken Formalismus, jedoch sind die Möglichkeiten zur automatischen Analyse begrenzt, insbesondere bei Systemen mit vielen initialen Graphen oder großen, unendlichen Zustandsräumen. Induktive Invarianten könnten eine Lösung darstellen, erfordern jedoch oft erweitertes Wissen über das System und müssen spezifische Probleme wie Lokalität und fehlendes Kontextwissen adressieren. Der Bericht untersucht k-induktive Invarianten, eine Verallgemeinerung induktiver Invarianten, als Ansatz zur Bewältigung dieser Herausforderungen. Das zusätzliche Kontextwissen, das durch die Analyse mehrerer Schritte gewonnen wird, ermöglicht oft die Verifikation der gewünschten Invarianten ohne die iterative Entwicklung zusätzlicher Eigenschaften. Um unendliche Systeme in endlicher Zeit zu analysieren, wird eine symbolische Kodierung von Transformationssequenzen auf Basis verschachtelter Anwendungsbedingungen eingeführt. Der zentrale Beitrag umfasst einen formalen Ansatz und Algorithmus zur Verifikation von Graphbedingungen als k-induktive Invarianten. Ein formaler Beweis wird erbracht, um die Korrektheit des Verfahrens nachzuweisen, und die Anwendbarkeit wird anhand mehrerer Beispiele demonstriert, die mit einer prototypischen Implementierung verifiziert wurden.

Die Korrektheit von Modelltransformationen ist entscheidend für die modellgetriebene Softwareentwicklung, insbesondere zur Vermeidung semantischer Fehler durch Verhaltensbewahrung. Diese Eigenschaft gewährleistet, dass spezifische Merkmale während des Entwicklungsprozesses erhalten bleiben. Verifikationstechniken zeigen, dass entweder bestimmte Eigenschaften bewahrt werden oder eine Form von Verhaltensäquivalenz zwischen Quell- und Zielmodellen besteht. Automatisierte Werkzeuge existieren für die Verifikation auf der Instanzebene, um konkrete Modellpaare zu überprüfen. Ein automatisierter Ansatz für die Transformationsebene, der Aussagen zu allen Quell- und Zielmodellen treffen kann, fehlt jedoch. Dieser Bericht erweitert frühere Arbeiten und präsentiert einen neuen Ansatz zur automatischen Verifikation von Verhaltensbewahrung, der auf Bisimulation und Simulation basiert. Modelltransformationen werden durch Triple-Graph-Grammatiken und Verhaltensdefinitionen mittels Graphtransformationsregeln beschrieben. Wir zeigen, dass das Verhaltensbewahrungsproblem durch Bisimulation auf Invariant-Checking für Graphtransformationssysteme reduziert werden kann. Zudem wird demonstriert, dass unser Werkzeug zur Verifikation induktiver Invarianten das Invariant-Checking-Problem für ein komplexes Beispiel, die Transformation von Sequenzdiagrammen in Systeme kommunizierender Automaten, lösen kann. Abschließend werden Einschränkungen von Invaria

Graph transformation systems are a powerful formal model to capture model transformations or systems with infinite state space, among others. However, this expressive power comes at the cost of rather limited automated analysis capabilities. The general case of unbounded many initial graphs or infinite state spaces is only supported by approaches with rather limited scalability or expressiveness. In this report we improve an existing approach for the automated verification of inductive invariants for graph transformation systems. By employing partial negative application conditions to represent and check many alternative conditions in a more compact manner, we can check examples with rules and constraints of substantially higher complexity. We also substantially extend the expressive power by supporting more complex negative application conditions and provide higher accuracy by employing advanced implication checks. The improvements are evaluated and compared with another applicable tool by considering three case studies.

Das Buch ist das erste über Wieler. Es verbindet frühere Erkenntnisse mit neuen Forschungsergebnissen und enthält Texte von bis dahin unveröffentlichten Quellen aus Großbritannien, Kanada und Russland.