Towards the Automatic Verification of Inductive Invariants for Infinite State UML Models
Holger Giese, Daniela Schilling · 2005
The semantics of systems with infinite state space and complex structures such as UML models have been successfully specified with expressive graph transformation techniques. Available automatic approaches to verify the resulting system behavior are restricted to finite state models of moderate size. Algorithms for checking system invariants are restricted to simpler classes of graph transformation systems and properties. In this paper a sufficiently scalable algorithm to check inductive invariants for graph transformation systems is outlined. The employed graph transformation variant is expressive and includes negation. The properties, for which it is checked whether they are invariants of the system, are described by graph matching that can also deal with negations. Due to the inherent local specification style of the graph transformation rules and properties described by graph matching, the complexity of the sketched algorithm depends on the number of graph transformation rules, size of the rules, and the number and size of the graph patterns describing the system properties. It thus can address arbitrarily large or even infinite state systems, if the system and the required properties can be described with a reasonable numbers of rules and properties of limited size. ∗This work was developed in the course of the Special Research Initiative 614 Self-optimizing Concepts and Structures in Mechanical Engineering University of Paderborn, and was published on its behalf and funded by the Deutsche Forschungsgemeinschaft. †Supported by the International Graduate School of Dynamic Intelligent Systems.