zbMATH — the first resource for mathematics

An algebraic semantics for MOF. (English) Zbl 1213.68358
Summary: In model-driven development, software artifacts are represented as models in order to improve productivity, quality, and cost effectiveness. In this area, the meta-object facility (MOF) standard plays a crucial role as a generic framework within which a wide range of modeling languages can be defined. The MOF standard aims at offering a good basis for model-driven development, providing some of the building concepts that are needed: what is a model, what is a metamodel, what is reflection in the MOF framework, and so on. However, most of these concepts are not yet fully formally defined in the current MOF standard. In this paper we define a reflective, algebraic, executable framework for precise metamodeling based on membership equational logic (mel) that supports the MOF standard. Our framework provides a formal semantics of the following notions: \(metamodel, model\), and \(conformance\) of a model to its metamodel. Furthermore, by using the Maude language, which directly supports mel specifications, this formal semantics is \(executable\). This executable semantics has been integrated within the Eclipse modeling framework as a plugin tool called MOMENT2. In this way, formal analyses, such as semantic consistency checks, model checking of invariants and LTL model checking, become available within Eclipse to provide formal support for model-driven development processes.

68Q55 Semantics in the theory of computing
Full Text: DOI
[1] Anastasakis K, Bordbar B, Georg G, Ray I (2007) UML2Alloy: a challenging model transformation. In: Engels G, Opdyke B, Schmidt DC, Weil F (eds) MoDELS, volume 4735 of LNCS. Springer, New York, pp 436–450
[2] Anastasakis K, Bordbar B, Küster JM (2008) Analysis of model transformations via alloy. In: MODEVVA, volume 5002 of LNCS. Springer, New York
[3] AGG Homepage (2009) http://tfs.cs.tu-berlin.de/agg/
[4] Alloy Analyzer Homepage (2009) http://alloy.mit.edu/
[5] Aizenbud-Reshef N, Nolan BT, Rubin J, Shaham-Gafni Y (2006) Model traceability. IBM Syst J 45(3): 515–526 · Zbl 05421251 · doi:10.1147/sj.453.0515
[6] Bernstein PA (2003) Applying model management to classical meta data problems. In: Proceedings of the 1st biennial conference on innovative data systems research (CIDR)
[7] Bergstra J, Tucker J (1980) Characterization of computable data types by means of a finite equational specification method. In: de Bakker JW and van Leeuwen J (eds) Automata, languages and programming, seventh colloquium, LNCS, vol 81. Springer-Verlag, pp 76–90
[8] Biermann E, Ermel C, Taentzer G (2008) Precise semantics of EMF model transformations by graph transformation. In: Czarnecki K (eds) MoDELS’08, volume 5301 of LNCS. Springer, New York, pp 53–67
[9] Bézivin J (2005) On the unification power of models. Softw Syst Model 4(2): 171–188 · Zbl 02243134 · doi:10.1007/s10270-005-0079-0
[10] Boronat A, Carsí JA, Ramos I (2005) Automatic support for traceability in a generic model management framework. In: Hartman A, Kreische D (eds) ECMDA-FA, volume 3748 of LNCS. Springer, New York, pp 316–330
[11] Boronat A, Carsí JA, Ramos I (2006) Algebraic specification of a model transformation engine. In: Baresi L, Heckel R (eds) FASE, volume 3922 of LNCS. Springer, New York, pp 262–277
[12] Boronat A, Carsí JA, Ramos I, Letelier P (2007) Formal model merging applied to class diagram integration. Electr Notes Theor Comput Sci 166: 5–26 · Zbl 05417311 · doi:10.1016/j.entcs.2006.06.013
[13] Bork M, Geiger L, Schneider C, Zündorf A (2008) Towards roundtrip engineering–a template-based reverse engineering approach. In: Schieferdecker I, Hartman A (eds) ECMDA-FA, volume 5095 of LNCS. Springer, New York, pp 33–47
[14] Boronat A, Heckel R, Meseguer J (2009) Rewriting logic semantics and verification of model transformations. In: FASE, volume 5503 of LNCS. Springer, New York
[15] Boronat A, Knapp A, Meseguer J, Wirsing M (2009) What is a multi-modeling language? In: 19th International workshop on algebraic development techniques, volume 5486 of LNCS. Springer, New York, pp 71–87 · Zbl 1253.68225
[16] Boronat A, Meseguer J (2009) Algebraic semantics of OCL-constrained metamodel specifications. In: Paige RF, Meyer B (eds) TOOLS (47), LNBIP. Springer, New York
[17] Boronat A, Oriente J, Gómez A, Ramos I, Carsí JA (2006) An algebraic specification of generic OCL queries within the eclipse modeling framework. In: Rensink A, Warmer J (eds) ECMDA-FA, volume 4066 of LNCS. Springer, New York, pp 316–330
[18] Boronat A (2007) MOMENT: a formal framework for MOdel manageMENT. PhD in Computer Science, Universitat Politènica de València (UPV), Spain http://www.cs.le.ac.uk/people/aboronat/papers/2007_thesis_ArturBoronat.pdf
[19] Bouhoula A, Jouannaud J-P, Meseguer J (2000) Specification and proof in membership equational logic. Theor Comput Sci 236: 35–132 · Zbl 0938.68057 · doi:10.1016/S0304-3975(99)00206-6
[20] Bruni R, Meseguer J (2006) Semantic foundations for generalized rewrite theories. Theor Comput Sci 360(1–3): 386–414 · Zbl 1097.68051 · doi:10.1016/j.tcs.2006.04.012
[21] Clavel M, Durán F, Eker S, Meseguer J, Lincoln P, Martí-Oliet N, Talcott C (2007) All about Maude–a high-performance logical framework, LNCS, vol 4350. Springer, New York · Zbl 1115.68046
[22] Clavel M, Durán F, Eker S, Meseguer J, Stehr M-O (1999) Maude as a formal meta-tool. In: Wing J, Woodcock J (eds) FM’99–Formal methods, volume 1709 of LNCS. Springer-Verlag, New York, pp 1684–1703
[23] Clark T, Evans A, Kent S (2001) The metamodelling language calculus: foundation semantics for UML. In: Hußmann H (eds) FASE, volume 2029 of LNCS. Springer, New York, pp 17–31 · Zbl 0977.68766
[24] Clark T, Evans A, Kent S (2002) Engineering modelling languages: a precise meta-modelling approach. In: FASE 02, volume 2306 of LNCS. Springer, London, pp 159–173 · Zbl 1059.68553
[25] Cervesato I, Stehr M-O (2004) Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types. In: Degano P (ed) Proceedings of fifth international workshop on rewriting logic and its applications (WRLA’2004), vol 117, ENTCS. Barcelona, Spain, Elsevier · Zbl 1115.68073
[26] Clavel M, Meseguer J, Palomino M (2007) Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. Theor Comput Sci 373: 70–91 · Zbl 1111.03034 · doi:10.1016/j.tcs.2006.12.009
[27] Ehrig H, Ehrig K, Prange U, Taentzer G (2006) Fundamentals of algebraic graph transformation. Springer, New York · Zbl 1095.68047
[28] Eclipse Organization. (2009) The Eclipse modeling framework, http://www.eclipse.org/emf/
[29] Ehrig H, Montanari U, Kreowski H-J, Rozenberg G, Kreowski H-J (1999) Handbook of graph grammars and computing by graph transformations, vol 3. World Scientific Publishing Company · Zbl 0951.68049
[30] Alemán JLF (2002) A formalization proposal of the UML four-layered architecture. PhD thesis, Murcia University (In Spanish)
[31] Fernández JL, Toval A (2000) Can intuition become rigorous? Foundations for UML model verification tools. In: International symposium on software reliability engineering (ISSRE 2000). IEEE. San Jose, California, USA
[32] Fernández JL, Toval A (2001) Seamless formalizing the UML semantics through metamodels. Unified modeling language: systems analysis, design, and development issues. Idea Group Publishing, pp 224–248
[33] Goguen JA, Burstall RM (1992) Institutions: abstract model theory for specification and programming. J ACM 39(1): 95–146 · Zbl 0799.68134 · doi:10.1145/147508.147524
[34] Jackson D (2006) Software abstractions: logic, language, and analysis. The MIT Press
[35] Java Community Process (2002) The Java metadata interface (JMI) specification (JSR 40). http://www.jcp.org/en/jsr/detail?id=40
[36] Jouault F, Bézivin J (2006) Km3: a dsl for metamodel specification. In: Gorrieri R, Wehrheim H (eds) FMOODS, volume 4037 of LNCS. Springer, New York, pp 171–185
[37] Kühne T (2006) Matters of (meta-) modeling. Softw Syst Model 5: 369–385 · Zbl 05149635 · doi:10.1007/s10270-006-0017-9
[38] Lacy LW (2005) Owl: representing information using the Web ontology language. Trafford Publishing
[39] Ludewig J (2004) Models in software engineering–an introduction. Inform Forsch Entwickl 18(3–4): 105–112 · Zbl 02243434 · doi:10.1007/s00450-004-0155-7
[40] Makkai M (1997) Generalized sketches as a framework for completeness theorems. J Pure Appl Algebra 115(1): 49–79 · Zbl 0871.03045 · doi:10.1016/S0022-4049(96)00007-2
[41] Maude Development Tools (2006) http://moment.dsic.upv.es
[42] Meseguer J, Roşu G (2004) Rewriting logic semantics: from language specifications to formal analysis tools. In: Proceedings of international joint conference on automated reasoning IJCAR’04, Cork, Ireland. Springer LNAI 3097, pp 1–44 · Zbl 1126.68464
[43] Meseguer J, Roşu G (2007) The rewriting logic semantics project. Theor Comput Sci 373: 213–237 · Zbl 1111.68068 · doi:10.1016/j.tcs.2006.12.018
[44] Meseguer J (1992) Conditional rewriting logic as a unified model of concurrency. Theor Comput Sci 96(1): 73–155 · Zbl 0758.68043 · doi:10.1016/0304-3975(92)90182-F
[45] Meseguer J (1993) A logical theory of concurrent objects and its realization in the Maude language. In: Agha G, Wegner P, Yonezawa A (eds) Research directions in concurrent object-oriented programming. MIT Press, pp 314–390
[46] Meseguer J (1998) Membership algebra as a logical framework for equational specification. In: Parisi-Presicce F (ed) Proceedings of WADT’97, LNCS 1376. Springer, pp 18–61 · Zbl 0903.08009
[47] MOMENT2, (2009) http://www.cs.le.ac.uk/\(\sim\)aboronat/tools/moment2
[48] Ölveczky P, Boronat A, Meseguer J (2010) Formal semantics and analysis of behavioral AADL models in real-time Maude. Technical Report at UIUC (to appear)
[49] Ölveczky PC, Meseguer J (2007) Semantics and pragmatics of real-time Maude. Higher-Order Symbolic Comput 20(1–2): 161–196 · Zbl 1115.68095 · doi:10.1007/s10990-007-9001-5
[50] OMG (2006) Meta Object Facility (MOF) 2.0 Core Specification (ptc/06-01-01)
[51] Paesschen EV, Meuter WD, D’Hondt M (2005) Selfsync: a dynamic round-trip engineering environment. In OOPSLA ’05: companion to the 20th annual ACM SIGPLAN conference on object-oriented programming, systems, languages, and applications. ACM, New York, pp 146–147
[52] Poernomo I (2006) The meta-object facility typed. In: Haddad H (ed) SAC, ACM, pp 1845–1849
[53] Rensink A (2004) Subjects, models, languages, transformations. In: Bézivin J, Heckel R (eds) Language engineering for model-driven software development, volume 04101 of Dagstuhl seminar proceedings. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany
[54] Romero JR, Rivera JE, Durán F, Vallecillo A (2007) Formal and tool support for model driven engineering with Maude. J Object Technol 6(9): 187–207 · Zbl 05515552 · doi:10.5381/jot.2007.6.9.a10
[55] IBM (2009) Rational Software Architect for WebSphere Software, http://www-01.ibm.com/software/awdtools/swarchitect/websphere/
[56] Rozenberg G (1997) Handbook of grammars and computing by graph transformation, vol 1. World Scientific Publishing Company, Singapore · Zbl 0908.68095
[57] Rutle YLA, Rossini A, Wolter U (2009) A Diagrammatic formalisation of MOF-based modelling languages. In: Paige RF, Meyer B (eds) Objects, components, models and patterns, 47th international conference, TOOLS EUROPE 2009, Zurich, Switzerland, June 29–July 3, 2008. Proceedings, LNBIP. Springer, New York
[58] SAE. (2007) AADL http://www.aadl.info/
[59] Seidewitz E (2003) What models mean. IEEE, Software 20(5): 26–32 · Zbl 05102231 · doi:10.1109/MS.2003.1231147
[60] Sendall S, Kozaczynski W (2003) Model transformation: the heart and soul of model-driven software development. IEEE Softw 20(5): 42–45 · Zbl 05102233 · doi:10.1109/MS.2003.1231150
[61] Serbanuta T, Roşu G, Meseguer J (2009) A rewriting logic approach to operational semantics. Inf Comput 2007: 305–340 · Zbl 1165.68041 · doi:10.1016/j.ic.2008.03.026
[62] Stehr M-O, Meseguer J (2004) Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework. In: Essays in memory of Ole-Johan Dahl, LNCS, vol 2635. Springer, New York, pp 334–375 · Zbl 1278.03066
[63] Toval A, Fernández JL (2000) Formally modeling uml and its evolution: a holistic approach. FMOODS’00, formal methods for open object-based distributed systems, September 2000. Stanford, California, USA. Kluwer, Dordrecht
[64] Triskell Team (2008) Kermeta, http://www.kermeta.org/
[65] OASIS (2007) Web services business process execution language version 2.0, http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.