Dynamic logic semantics for UML consistency

Abstract

The Unified Modelling Language (UML) is intended to describe systems, but, it is not clear what systems satisfy a given collection of UML diagrams. Stephen Mellor has described a small collection of diagrams which appear to be inconsistent, yet are "cool" according to UML. We describe an approach to defining semantics for UML diagrams using dynamic logic, and show that Mellor's example is inconsistent, given a reasonable assumption. Our approach interprets all diagrams, static and dynamic, in a single semantic space. The modeller specifies how the meaning of a model is made up from the meanings of its diagrams, thus the "viewpoint" taken by each diagram is made explicit. This composition is achieved through formation of the dynamic logic formulae. It is therefore very flexible, and we propose it as a means for defining semantics for domain specific languages, and for specifying "bridges" or "weaving" model transformations used in aspect oriented modelling.