Formalizing Domain-Specific Metamodeling
Language XMML Based on First-order Logic
Tao Jiang
School of Mathematics and Computer Science, Yunnan University of Nationalities, Kunming, P.R.China
Email: jtzwy123@gmail.com
Xin Wang
School of Mathematics and Computer Science, Yunnan University of Nationalities, Kunming, P.R.China
Email: wxkmyn@yahoo.com.cn
Abstract—Domain-Specific Modeling has been widely and
successfully used in software system modeling of specific
domains. In spite of its general important, due to its
informal definition, Domain-Specific Metamodeling
Language (DSMML) cannot strictly represent its structural
semantics, so its properties such as consistency cannot be
systematically verified. In response, the paper proposes a
formal representation of the structural semantics of
DSMML named XMML based on first-order logic. Firstly,
XMML is introduced, secondly, we illustrate our approach
by formalization of attachment relationship and refinement
relationship and typed constraints of XMML based on first-
order logic, based on this, the approach of consistency
verification of XMML itself and metamodels built based on
XMML is presented, finally, the formalization automatic
mapping engine for metamodels is introduced to show the
application of formalization of XMML.
Index Terms—Domain-Specific Metamodeling Language,
structural semantics, attachment, refinement, consistency
verification
I.
I
NTRODUCTION
Compared with the uniformity and standardization of
MDA [1], DSM [2] focuses on simplicity, practicability
and flexibility. As a metamodeling language for DSM,
DSMML plays an important role in system modeling of
specific areas.
DSMML is a metalanguage used to build Domain-
Specific Modeling Languages (DSMLs); this process that
we use DSMML to build domain metamodels indicating
the structural semantics of DSMLs is called
metamodeling. Correspondingly, DSML is modeling
language used to build domain application models; this
process that we use DSML to build domain application
models is called application modeling.
Semantics of DSMML can be grouped into structural
semantics [3] and behavioral semantics. The former
concerns static semantic constraints of relationship
between modeling elements, focusing on the static
structural properties; the latter concerns execution
semantics of domain metamodels, focusing on the
dynamic behavior of the metamodels. Although structural
semantics is very important, research in structural
semantics is not as extensive and deep as behavioral
semantics’, so this paper only studies structural semantics
of DSMML.
There are several problems that have not been solved
well for DSMML, which include precise formal
description of its semantics, method of verification of
properties of domain metamodels based on formalization
and automatic translation from metamodels to
corresponding formal semantic domain.
The paper proposes a formal representation of the
structural semantics of DSMML named XMML designed
by us based on first-order logic, based on this, the
approach of consistency verification of XMML and
metamodels is presented, and then design and
implementation of corresponding formalization automatic
mapping engine for metamodels is introduced to show the
application of formalization of XMML.
II.
R
ELATED
W
ORKS
Within the domain-specific language community,
graph-theoretic formalisms have received the most
research attention [4]. The majority of work focuses on
model transformations based on graph, but analysis and
validation of properties of models has not received the
same attention. For example, the model transformation
tool VIATRA [5] supports executable Horn logic to
specify transformations, but does not focus on restricting
expressiveness for the purpose of analysis.
Because UML includes many diagrams including
metamodeling, state machines, activities, sequence charts
and so on, approaches for formalizing UML must tackle
the temporal nature of its various behavioral semantics,
necessitating more expressive formal methods. All these
approaches must make trade-offs between expressiveness
and the degree of automated analysis. For example, Z [6]
or B [7] formalizations of UML could be a vehicle for
studying rich syntax, but automated analysis and
verification is less likely to be found.
Supported by Yunnan Provincial Department of Education Researc
Fund Key Project (No. 2011z025) and General Project (No. 2011y214)
Corresponding author: E-mail addresses: jtzwy123@gmail.com
JOURNAL OF SOFTWARE, VOL. 7, NO. 6, JUNE 2012 1321
© 2012 ACADEMY PUBLISHE
doi:10.4304/jsw.7.6.1321-1328