K-inductive invariant checking for graph transformation systems

Mehr zum Buch

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.