Reference:

J. Bauer, Werner Damm, Tobe Toben, and Bernd Westphal. Verification and Synthesis of Ocl Constraints via Topology Analysis: A Case Study. In Applications of Graph Transformations with Industrial Relevance Third International Symposium. Springer, 2007.

Abstract:

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.

Keywords:

OCL constraints, UML, graph grammar verification, synthesis

Suggested BibTeX entry:

@inproceedings{BDTW07,
    author = {J. Bauer and Werner Damm and Tobe Toben and Bernd Westphal},
    booktitle = {Applications of Graph Transformations with Industrial Relevance Third International Symposium},
    publisher = {Springer},
    title = {{V}erification and {S}ynthesis of {O}CL {C}onstraints via {T}opology {A}nalysis: {A} {C}ase {S}tudy},
    year = {2007}
}