Verification and Synthesis of OCL Constraints Via Topology Analysis

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 Analyarticular 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.

• Type: Conference
• Year: 2007
• Where: AGTIVE
• Authors: Jörg Bauer, Werner Damm, Tobe Toben, Bernd Westphal
• Keywords: AGTIVE 2007, Formal Methods, Graph Grammars, Object Diagrams, Topology Invariants