k-Inductive invariant checking for graph transformation systems

  • While offering significant expressive power, graph transformation systems often come with rather limited capabilities for automated analysis, particularly if systems with many possible initial graphs and large or infinite state spaces are concerned. One approach that tries to overcome these limitations is inductive invariant checking. However, the verification of inductive invariants often requires extensive knowledge about the system in question and faces the approach-inherent challenges of locality and lack of context. To address that, this report discusses k-inductive invariant checking for graph transformation systems as a generalization of inductive invariants. The additional context acquired by taking multiple (k) steps into account is the key difference to inductive invariant checking and is often enough to establish the desired invariants without requiring the iterative development of additional properties. To analyze possibly infinite systems in a finite fashion, we introduce a symbolic encoding for transformationWhile offering significant expressive power, graph transformation systems often come with rather limited capabilities for automated analysis, particularly if systems with many possible initial graphs and large or infinite state spaces are concerned. One approach that tries to overcome these limitations is inductive invariant checking. However, the verification of inductive invariants often requires extensive knowledge about the system in question and faces the approach-inherent challenges of locality and lack of context. To address that, this report discusses k-inductive invariant checking for graph transformation systems as a generalization of inductive invariants. The additional context acquired by taking multiple (k) steps into account is the key difference to inductive invariant checking and is often enough to establish the desired invariants without requiring the iterative development of additional properties. To analyze possibly infinite systems in a finite fashion, we introduce a symbolic encoding for transformation traces using a restricted form of nested application conditions. As its central contribution, this report then presents a formal approach and algorithm to verify graph constraints as k-inductive invariants. We prove the approach's correctness and demonstrate its applicability by means of several examples evaluated with a prototypical implementation of our algorithm.show moreshow less
  • Während Graphtransformationssysteme einerseits einen ausdrucksstarken Formalismus bereitstellen, existieren andererseits nur eingeschränkte Möglichkeiten für die automatische Analyse. Dies gilt insbesondere für die Analyse von Systemen mit einer Vielzahl an initialen Graphen oder mit großen oder unendlichen Zustandsräumen. Ein möglicher Ansatz, um diese Einschränkungen zu umgehen, sind induktive Invarianten. Allerdings erfordert die Verifkation induktiver Invarianten oft erweitertes Wissen über das zu verifizierende System; weiterhin muss diese Verifikationstechnik mit den spezifischen Problemen der Lokalität und des Mangels an Kontextwissen umgehen. Dieser Bericht betrachtet k-induktive Invarianten - eine Verallgemeinerung induktiver Invarienten - für Graphtransformationssysteme als einen möglichen Ansatz, um diese Probleme anzugehen. Zusätzliches Kontextwissen, das durch die Analyse mehrerer (k) Schritte gewonnen werden kann, macht den entscheidenden Unterschied zu induktiven Invarianten aus und genügt oft, um die gewünschtenWährend Graphtransformationssysteme einerseits einen ausdrucksstarken Formalismus bereitstellen, existieren andererseits nur eingeschränkte Möglichkeiten für die automatische Analyse. Dies gilt insbesondere für die Analyse von Systemen mit einer Vielzahl an initialen Graphen oder mit großen oder unendlichen Zustandsräumen. Ein möglicher Ansatz, um diese Einschränkungen zu umgehen, sind induktive Invarianten. Allerdings erfordert die Verifkation induktiver Invarianten oft erweitertes Wissen über das zu verifizierende System; weiterhin muss diese Verifikationstechnik mit den spezifischen Problemen der Lokalität und des Mangels an Kontextwissen umgehen. Dieser Bericht betrachtet k-induktive Invarianten - eine Verallgemeinerung induktiver Invarienten - für Graphtransformationssysteme als einen möglichen Ansatz, um diese Probleme anzugehen. Zusätzliches Kontextwissen, das durch die Analyse mehrerer (k) Schritte gewonnen werden kann, macht den entscheidenden Unterschied zu induktiven Invarianten aus und genügt oft, um die gewünschten Invarianten ohne die iterative Entwicklung zusätzlicher Eigenschaften zu verifizieren. Um unendliche Systeme in endlicher Zeit zu analysieren, führen wir eine symbolische Kodierung von Transformationssequenzen ein, die auf verschachtelten Anwendungsbedingungen basiert. Unser zentraler Beitrag ist dann ein formaler Ansatz und Algorithmus zur Verifikation von Graphbedingungen als k-induktive Invarianten. Wir führen einen formalen Beweis, um die Korrektheit unseres Verfahrens nachzuweisen, und demonstrieren die Anwendbarkeit des Verfahrens an mehreren Beispielen, die mit einer prototypischen Implementierung verifiziert wurden.show moreshow less

Download full text files

  • tbhpi119.pdfeng
    (4920KB)

    SHA-1:f47c839ed728c724452ff83efeaee0892ec60b48

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Johannes Dyck, Holger GieseORCiDGND
URN:urn:nbn:de:kobv:517-opus4-397044
ISBN:978-3-86956-406-7
ISSN:1613-5652 (print)
ISSN:2191-1665 (online)
Series (Serial Number):Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam (119)
Publisher:Universitätsverlag Potsdam
Place of publication:Potsdam
Document Type:Monograph/Edited Volume
Language:English
Year of Completion:2017
Publishing Institution:Universität Potsdam
Publishing Institution:Universitätsverlag Potsdam
Release Date:2017/07/27
Tag:Graphbedingungen; Graphtransformationen; Graphtransformationssysteme; Sequenzen von s/t-Pattern; Transformationssequenzen; formale Verifikation; k-Induktion; k-induktive Invarianten; k-induktives Invariant-Checking; statische Analyse; verschachtelte Anwednungsbedingungen
formal verification; graph constraints; graph transformation; k-induction; k-inductive invariant checking; k-inductive invariants; nested application conditions; s/t-pattern sequences; static analysis; transformation sequences; typed graph transformation systems
Issue:119
Pagenumber:45
RVK - Regensburg Classification:ST 230
Organizational units:An-Institute / Hasso-Plattner-Institut für Digital Engineering gGmbH
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Publication Way:Universitätsverlag Potsdam
Licence (German):License LogoKeine Nutzungslizenz vergeben - es gilt das deutsche Urheberrecht
Notes extern:In Printform erschienen im Universitätsverlag Potsdam:

k-Inductive invariant checking for graph transformation systems / Johannes Dyck, Holger Giese. – Potsdam: Universitätsverlag Potsdam, 2017. – 45 S. : Tabellen, Charts
(Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam ;119)
ISSN (print) 1613-5652
ISSN (online) 2191-1665
ISBN 978-3-86956-406-7
--> bestellen