{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T17:21:45Z","timestamp":1791048105555,"version":"4.1.0"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2010,5,1]],"date-time":"2010-05-01T00:00:00Z","timestamp":1272672000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2010,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 (<jats:sc>mel<\/jats:sc>) that supports the MOF standard. Our framework provides a formal semantics of the following notions:<jats:italic>metamodel<\/jats:italic>,<jats:italic>model<\/jats:italic>, and<jats:italic>conformance<\/jats:italic>of a model to its metamodel. Furthermore, by using the Maude language, which directly supports<jats:sc>mel<\/jats:sc>specifications, this formal semantics is<jats:italic>executable<\/jats:italic>. 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.<\/jats:p>","DOI":"10.1007\/s00165-009-0140-9","type":"journal-article","created":{"date-parts":[[2010,2,19]],"date-time":"2010-02-19T14:40:10Z","timestamp":1266590410000},"page":"269-296","source":"Crossref","is-referenced-by-count":33,"title":["An algebraic semantics for MOF"],"prefix":"10.1145","volume":"22","author":[{"given":"Artur","family":"Boronat","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Leicester, University Road, LE1 7RH, Leicester, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"436","volume-title":"MoDELS, volume 4735 of LNCS","author":"Anastasakis K","year":"2007"},{"key":"e_1_2_1_2_2_2","unstructured":"Anastasakis K Bordbar B K\u00fcster JM (2008) Analysis of model transformations via alloy. In: MODEVVA volume 5002 of LNCS. Springer New York"},{"key":"e_1_2_1_2_3_2","unstructured":"AGG Homepage (2009) http:\/\/tfs.cs.tu-berlin.de\/agg\/"},{"key":"e_1_2_1_2_4_2","unstructured":"Alloy Analyzer Homepage (2009) http:\/\/alloy.mit.edu\/"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1147\/sj.453.0515"},{"key":"e_1_2_1_2_6_2","unstructured":"Bernstein PA (2003) Applying model management to classical meta data problems. In: Proceedings of the 1st biennial conference on innovative data systems research (CIDR)"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"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\u201390","DOI":"10.1007\/3-540-10003-2_61"},{"key":"e_1_2_1_2_8_2","first-page":"53","volume-title":"MoDELS\u201908, volume 5301 of LNCS","author":"Biermann E","year":"2008"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-005-0079-0"},{"key":"e_1_2_1_2_10_2","first-page":"316","volume-title":"ECMDA-FA, volume 3748 of LNCS","author":"Boronat A","year":"2005"},{"key":"e_1_2_1_2_11_2","first-page":"262","volume-title":"FASE, volume 3922 of LNCS","author":"Boronat A","year":"2006"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.06.013"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Bork M Geiger L Schneider C Z\u00fcndorf A (2008) Towards roundtrip engineering\u2014a template-based reverse engineering approach. In: Schieferdecker I Hartman A (eds) ECMDA-FA volume 5095 of LNCS. Springer New York pp 33\u201347","DOI":"10.1007\/978-3-540-69100-6_3"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Boronat A Heckel R Meseguer J (2009) Rewriting logic semantics and verification of model transformations. In: FASE volume 5503 of LNCS. Springer New York","DOI":"10.1007\/978-3-642-00593-0_2"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"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\u201387","DOI":"10.1007\/978-3-642-03429-9_6"},{"key":"e_1_2_1_2_16_2","volume-title":"TOOLS (47), LNBIP","author":"Boronat A","year":"2009"},{"key":"e_1_2_1_2_17_2","first-page":"316","volume-title":"ECMDA-FA, volume 4066 of LNCS","author":"Boronat A","year":"2006"},{"key":"e_1_2_1_2_18_2","unstructured":"Boronat A (2007) MOMENT: a formal framework for MOdel manageMENT. PhD in Computer Science Universitat Polit\u00e8nica de Val\u00e8ncia (UPV) Spain http:\/\/www.cs.le.ac.uk\/people\/aboronat\/papers\/2007_thesis_ArturBoronat.pdf"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00206-6"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.04.012"},{"key":"e_1_2_1_2_21_2","volume-title":"All about Maude\u2014a high-performance logical framework, LNCS, vol 4350","author":"Clavel M","year":"2007"},{"key":"e_1_2_1_2_22_2","first-page":"1684","volume-title":"FM\u201999\u2014Formal methods, volume 1709 of LNCS","author":"Clavel M","year":"1999"},{"key":"e_1_2_1_2_23_2","first-page":"17","volume-title":"FASE, volume 2029 of LNCS","author":"Clark T","year":"2001"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"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\u2013173","DOI":"10.1007\/3-540-45923-5_11"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"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\u20192004) vol 117 ENTCS. Barcelona Spain Elsevier","DOI":"10.1016\/j.entcs.2004.06.023"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.009"},{"key":"e_1_2_1_2_27_2","volume-title":"Fundamentals of algebraic graph transformation","author":"Ehrig H","year":"2006"},{"key":"e_1_2_1_2_28_2","unstructured":"Eclipse Organization. (2009) The Eclipse modeling framework http:\/\/www.eclipse.org\/emf\/"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1142\/4181"},{"key":"e_1_2_1_2_30_2","unstructured":"Alem\u00e1n JLF (2002) A formalization proposal of the UML four-layered architecture. PhD thesis Murcia University (In Spanish)"},{"key":"e_1_2_1_2_31_2","unstructured":"Fern\u00e1ndez 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"},{"key":"e_1_2_1_2_32_2","unstructured":"Fern\u00e1ndez 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\u2013248"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"e_1_2_1_2_34_2","unstructured":"Jackson D (2006) Software abstractions: logic language and analysis. The MIT Press"},{"key":"e_1_2_1_2_35_2","unstructured":"Java Community Process (2002) The Java metadata interface (JMI) specification (JSR 40). http:\/\/www.jcp.org\/en\/jsr\/detail?id=40"},{"key":"e_1_2_1_2_36_2","first-page":"171","volume-title":"FMOODS, volume 4037 of LNCS","author":"Jouault F","year":"2006"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-006-0017-9"},{"key":"e_1_2_1_2_38_2","unstructured":"Lacy LW (2005) Owl: representing information using the Web ontology language. Trafford Publishing"},{"issue":"3","key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/s00450-004-0155-7","article-title":"Models in software engineering\u2014an introduction","volume":"18","author":"Ludewig J","year":"2004","journal-title":"Inform Forsch Entwickl"},{"issue":"1","key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/S0022-4049(96)00007-2","article-title":"Generalized sketches as a framework for completeness theorems","volume":"115","author":"Makkai M","year":"1997","journal-title":"J Pure Appl Algebra"},{"key":"e_1_2_1_2_41_2","unstructured":"Maude Development Tools (2006) http:\/\/moment.dsic.upv.es"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Meseguer J Ro\u015fu G (2004) Rewriting logic semantics: from language specifications to formal analysis tools. In: Proceedings of international joint conference on automated reasoning IJCAR\u201904 Cork Ireland. Springer LNAI 3097 pp 1\u201344","DOI":"10.1007\/978-3-540-25984-8_1"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.018"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"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\u2013390","DOI":"10.7551\/mitpress\/2087.003.0017"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Meseguer J (1998) Membership algebra as a logical framework for equational specification. In: Parisi-Presicce F (ed) Proceedings of WADT\u201997 LNCS 1376. Springer pp 18\u201361","DOI":"10.1007\/3-540-64299-4_26"},{"key":"e_1_2_1_2_47_2","unstructured":"MOMENT2 (2009) http:\/\/www.cs.le.ac.uk\/~aboronat\/tools\/moment2"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky P Boronat A Meseguer J (2010) Formal semantics and analysis of behavioral AADL models in real-time Maude. Technical Report at UIUC (to appear)","DOI":"10.1007\/978-3-642-13464-7_5"},{"issue":"1","key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","article-title":"Semantics and pragmatics of real-time Maude","volume":"20","author":"\u00d6lveczky PC","year":"2007","journal-title":"Higher-Order Symbolic Comput"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"OMG (2006) Meta Object Facility (MOF) 2.0 Core Specification (ptc\/06-01-01)","DOI":"10.11156\/aibr.010102"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Paesschen EV Meuter WD D\u2019Hondt M (2005) Selfsync: a dynamic round-trip engineering environment. In OOPSLA \u201905: companion to the 20th annual ACM SIGPLAN conference on object-oriented programming systems languages and applications. ACM New York pp 146\u2013147","DOI":"10.1145\/1094855.1094906"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Poernomo I (2006) The meta-object facility typed. In: Haddad H (ed) SAC ACM pp 1845\u20131849","DOI":"10.1145\/1141277.1141710"},{"key":"e_1_2_1_2_53_2","unstructured":"Rensink A (2004) Subjects models languages transformations. In: B\u00e9zivin J Heckel R (eds) Language engineering for model-driven software development volume 04101 of Dagstuhl seminar proceedings. Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI) Schloss Dagstuhl Germany"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2007.6.9.a10"},{"key":"e_1_2_1_2_55_2","unstructured":"IBM (2009) Rational Software Architect for WebSphere Software http:\/\/www-01.ibm.com\/software\/awdtools\/swarchitect\/websphere\/"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"publisher","DOI":"10.5555\/278918"},{"key":"e_1_2_1_2_57_2","unstructured":"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\u2013July 3 2008. Proceedings LNBIP. Springer New York"},{"key":"e_1_2_1_2_58_2","unstructured":"SAE. (2007) AADL http:\/\/www.aadl.info\/"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2003.1231147"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2003.1231150"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/j.ic.2008.03.026","article-title":"A rewriting logic approach to operational semantics","volume":"2007","author":"Serbanuta T","year":"2009","journal-title":"Inf Comput"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"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\u2013375","DOI":"10.1007\/978-3-540-39993-3_16"},{"key":"e_1_2_1_2_63_2","unstructured":"Toval A Fern\u00e1ndez JL (2000) Formally modeling uml and its evolution: a holistic approach. FMOODS\u201900 formal methods for open object-based distributed systems September 2000. Stanford California USA. Kluwer Dordrecht"},{"key":"e_1_2_1_2_64_2","unstructured":"Triskell Team (2008) Kermeta http:\/\/www.kermeta.org\/"},{"key":"e_1_2_1_2_65_2","unstructured":"OASIS (2007) Web services business process execution language version 2.0 http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/wsbpel-v2.0.pdf"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-009-0140-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-009-0140-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-009-0140-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,24]],"date-time":"2024-03-24T05:14:19Z","timestamp":1711257259000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-009-0140-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5]]},"references-count":65,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["10.1007\/s00165-009-0140-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-009-0140-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5]]}}}