Inductive invariant checking with partial negative application conditions

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.