@TechReport{GS04_ag,
AUTHOR = {Giese, Holger and Schilling, Daniela},
TITLE = {{Towards the Automatic Verification of Inductive Invariants for Infinite State UML Models}},
YEAR = {2004},
MONTH = {December},
NUMBER = {tr-ri-04-252},
ADDRESS = {Paderborn, Germany},
INSTITUTION = {University of Paderborn},
URL = {http://www.upb.de/cs/ag-schaefer/Veroeffentlichungen/Quellen/Papers/2004/tr-ri-04-252.pdf},
PDF = {tr-ri-04-252.pdf},
ABSTRACT = {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}
}