TY  - BOOK
A1  - Dyck, Johannes
A1  - Giese, Holger
T1  - Inductive invariant checking with partial negative application conditions
N2  - 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.
N2  - Graphtransformationssysteme stellen ein ausdrucksstarkes formales Modell zur Verfügung, um Modelltransformationen und Systeme mit unendlichem Zustandsraum zu beschreiben. Allerdings sorgt diese Ausdrucksstärke für signifikante Einschränkungen bei der automatischen Analyse. Ansätze, die die Analyse allgemeiner Systeme mit unendlichem Zustandsraum oder beliebig vielen initialen Graphen unterstützen, sind in ihrer Skalierbarkeit oder Ausdrucksstärke stark eingeschränkt. In diesem Bericht beschreiben wir Verbesserungen eines existierenden Ansatzes für die automatische Verifikation induktiver Invarianten in Graphtransformationssystemen. Durch die Verwendung partieller negativer Anwendungsbedingungen für die Repräsentation und Überprüfung einer Vielzahl an Bedingungen in kompakterer Form können Regeln und Bedingungen von deutlich höhrerer Komplexität verifiziert werden. Weiterhin wird die Ausdrucksstärke des Ansatzes beträchtlich erhöht, indem die Verwendung komplexerer negativer Anwendungsbedingungen und erweiterter Implikationstests ermöglicht wird. Alle diese Verbesserungen werden evaluiert und mit einem anderen anwendbaren Werkzeug anhand von drei Fallstudien verglichen.
T3  - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 98 
KW  - verification
KW  - inductive invariant checking
KW  - graph transformation
KW  - partial application conditions
KW  - Verifikation
KW  - induktives Invariant Checking
KW  - Graphtransformationen
KW  - partielle Anwendungsbedingungen
Y1  - 2015
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-77748
SN  - 978-3-86956-333-6
SN  - 1613-5652
SN  - 2191-1665
IS  - 98
PB  - Universitätsverlag Potsdam
CY  - Potsdam
ER  -