Verification and Synthesis of OCL Constraints via Topology Analysis - A case study
Bauer, Jörg and Damm, Werner and Toben, Tobe and Westphal, Bernd
On the basis of a case-study, we demonstrate the usefulness of topology invariants for model-driven systems development. Considering a graph grammar semantics for a relevant fragment of UML, where a graph represents an object diagram, allows us to apply Topology Analysis, a particular abstract interpretation of graph grammars. The outcome of this analysis is a finite and concise over-approximation of all possible reachable object diagrams, the so-called topology invariant. We discuss how topology invariants can be used to verify that constraints on a given model are respected by the behaviour and how they can be viewed as synthesised constraints providing insight into the dynamic behaviour of the model.
10 / 2007
inproceedings
Springer
LNCS
361-376
5088
