Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam
ISSN (print) 1613-5652
ISSN (online) 2191-1665
URN urn:nbn:de:kobv:517-series-822
Herausgegeben von den
Professoren des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam
Titel der Reihe bis Nummer 119: Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam
Die Schriftenreihe Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering (HPI) informieren über laufende Forschungsarbeiten und Projekte der Fachgebiete auf Deutsch und Englisch.
ISSN (online) 2191-1665
URN urn:nbn:de:kobv:517-series-822
Herausgegeben von den
Professoren des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam
Titel der Reihe bis Nummer 119: Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam
Die Schriftenreihe Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering (HPI) informieren über laufende Forschungsarbeiten und Projekte der Fachgebiete auf Deutsch und Englisch.
Refine
Has Fulltext
- yes (1)
Year of publication
- 2015 (1)
Document Type
Language
- English (1)
Is part of the Bibliography
- yes (1)
Keywords
- induktives Invariant Checking (1) (remove)
Institute
98
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.