Research on Metamodel Consistency Verification Based on First-order Logical Inference

• Autorzy: Jiang T.

Warianty tytułu

PL

Badania weryfikacji konsystencji metamodelu bazujące na interferencji logicznej pierwszego rzędu

• Języki publikacji: EN

Abstrakty

EN

Domain-Specific Metamodeling Language (DSMML) defined by informal method cannot strictly represent its structural semantics, so its properties such as consistency cannot be holistically and systematically verified. In response, the paper proposes an approach for verifying metamodels consistency based on formalization of DSMML named XMML. Firstly, we describe our approach of formalization, and then, the approach of consistency verification of XMML and its metamodels based on first-order logical inference is presented, finally, the formalization automatic mapping engine for metamodels is designed and relevant test is performed to show the feasibility of our formal method.

PL

W artykule zaproponowano metodę weryfikacji metamodelu DSMML (Domain Specific Metamodeling Language). Weryfikacja bazuje na interferencji logicznej pierwszego rzędu.

Słowa kluczowe

EN

meta-type; consistency verification; automatic mapping; DSMML

PL

metamodel; DSMML

• Wydawca: Wydawnictwo SIGMA-NOT
• Czasopismo: Przegląd Elektrotechniczny
• Rocznik: 2012
• Tom: R. 88, nr 1b
• Strony: 132--136
• Opis fizyczny: Bibliogr. 16 poz., rys., wykr.

Twórcy

autor

Jiang T.

• School of Mathematics and Computer Science, Yunnan University of Nationalities, 134 Yi Er Yi Avenue, Kunming, P.R.China, 650031,

Bibliografia

• [1] dsmforum, Enterprise apps in smartphones, http://www.dsmforum.org/phone.html..
• [2] Jackson.E.K, Sztipanovits.J, “Formalizing the Structural Semantics of Domain-Specific Modeling Languages”, Journal of Software and Systems Modeling, 2008.
• [3] 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.
• [4] 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.
• [5] 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.
• [6] W.Andreopoulos, “Defining Formal Semantics for the Unified Modeling Language”, in Technique Report of University of Toronto, 2000, Toronto.
• [7] Malcolm Shroff, “Towards A Formalization of UML Class Structures in Z”, in Proceedings of COMPSAC'97.
• [8] 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.
• [9] 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.
• [10] Sun XP, A Research of Visual Domain-Specific Meta- Modeling Language and Its Instantiation, Kunming: Yunnan University.2008.
• [11] Gu TL, Formal methods of software development, Higher Education Press, Beijing, 2005.
• [12] Cheng MZ, Yu JW, Logic foundation—first-order logic and first-order theory, Chinese People University Press, Beijing, 2003.
• [13] 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.
• [14] Christoph Weidenbach, SPASS: Tutorial, 2000.
• [15] Spass. 2008, http://www.spass-prover.org.
• [16] W.McCune. OTTER 3.0 reference manual and guide. Argonne National Laboratory Tech. Argonne,IL,USA,1994, http://www.cs.unm.edu/~mccune/otter.