Journal of Software, Vol 7, No 6 (2012), 1321-1328, Jun 2012
doi:10.4304/jsw.7.6.1321-1328

Formalizing Domain-Specific Metamodeling Language XMML Based on First-order Logic

Tao Jiang, Xin Wang

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.


Keywords


Domain-Specific Metamodeling Language; structural semantics; attachment; refinement; consistency verification

References


 

[1]Miller J, Mukerji J, MDA guide version 1.0.1. http://www.omg.org/docs/omg/03-06-01.pdf, 2003.

[2]dsmforum, Enterprise apps in smartphones, http://www.dsmforum.org/phone.html.

[3]Jackson.E.K, Sztipanovits.J, “Formalizing the Structural Semantics of Domain-Specific Modeling Languages”, Journal of Software and Systems Modeling, 2008.

[4]B’E ZIVIN, J., AND GERB’E, O, “Towards a precise definition of the omg/mda framework”, in Proceedings of the 16th Conference on Automated Software Engineering (ASE 01) (2001), pp. 273–280.

[5]CSERT’A N, G., HUSZERL, G., MAJZIK, I., PAP, Z., PATARICZA.A., AND VARR’O, D. “Viatra - visual automated transformations for formal verification and validation of uml models”, in ASE (2002), pp. 267–270.

[6]EVANS, A., FRANCE, R. B., AND GRANT, E. S, “Towards formal reasoning with uml models”, in Proceedings of the Eighth OOPSLA Workshop on Behavioral Semantics.

[7]MARCANO, R., AND LEVY, N, “Using b formal specifications for analysis and verification of uml/ocl models”, in Workshop on consistency problems in UML-based software development.5th International Conference on the Unified Modeling Language (2002), pp. 91–105.

[8]W.Andreopoulos, “Defining Formal Semantics for the Unified Modeling Language”, in Technique Report of University of Toronto[C], 2000, Toronto.

[9]K. Kaneiwa and K. Satoh, “Consistency Checking Algorithms for Restricted UML Class Diagrams”, in 4th International Symposium on Foundations of Information and Knowledge Systems (FoIKS 2006)[C], LNCS 3861, 2006. p.19 - 239.

[10]R. F. Paige, B. P. J, “Metamodel-Based Model Conformance and Multiview Consistency Checking”, ACM Transactions on Software Engineering and Methodology, 2007. 16(3): p. 1-49.
http://dx.doi.org/10.1145/1243987.1243989

[11]Jackson.E.K, Sztipanovits.J, “Towards a formal foundation for domain specific modeling languages”, Proceedings of the Sixth ACM International Conference on Embedded Software (EMSOFT'06) (October 2006) 53-62.

[12]Sun XP, A Research of Visual Domain-Specific Meta-Modeling Language and Its Instantiation, Kunming: Yunnan University.2008.

[13]Gu TL, Formal methods of software development, Higher Education Press, Beijing, 2005.

[14]Cheng MZ, Yu JW, Logic foundation—first-order logic and first-order theory, Chinese People University Press, Beijing, 2003.

[15]H. Zhu, L. Shan, I. Bayley, and R. Amphlett, “A Formal Descriptive Semantics of UML and Its Applications”, in UML 2 Semantics and Applications, K. Lano (Eds). 2008, John Wiley & Sons, Inc.

[16]Christoph Weidenbach, SPASS: Tutorial, 2000.


Full Text: PDF


Journal of Software (JSW, ISSN 1796-217X)

Copyright @ 2006-2013 by ACADEMY PUBLISHER – All rights reserved.