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
BibTeX file
title = { Towards the Automatic Verification of Inductive Invariants for Infinite State UML Models },
year = { 2004 },
number = { tr-ri-04-252 },
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 },
month = { 12 },
address = { Paderborn, Germany },
institution = { University of Paderborn }
Copyright Notice
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
last change: Mon, 23 Nov 2009 09:14:18 +0100