Metamodeling Mathematics: A Precise and Visual Framework for Describing Semantics Domains of UML Models

Abstract. As UML 2.0 is evolving into a family of languages with in-dividually specified semantics, there is an increasing need for automated and provenly correct model transformations that (i) assure the integra-tion of local views (different diagrams) of the system into a consistent global view, and, (ii) provide a well–founded mapping from UML mod-els to different semantic domains (Petri nets, Kripke automaton, pro-cess algebras, etc.) for formal analysis purposes as foreseen, for instance, in submissions for the OMG RFP for Schedulability, Performance and Time. However, such transformations into different semantic domains typically require the deep understanding of the underlying mathemat-ics, which hinders the use of formal specification techniques in industrial applications. In the paper, we propose a UML-based metamodeling tech-nique with precise static and dynamic semantics (based on a refinement calculus and graph transformation) where the structure and operational semantics of mathematical models can be defined in a UML notation without cumbersome mathematical formulae