An algebraic semantics for MOF

Artur Boronat, José Meseguer

Research output: Contribution to journalArticlepeer-review


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. TheMOF 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. BCS

Original languageEnglish (US)
Pages (from-to)269-296
Number of pages28
JournalFormal Aspects of Computing
Issue number3-4
StatePublished - May 2010


  • Formal analysis
  • MOF
  • Membership equational logic
  • Metamodeling semantics
  • Model-driven development
  • Reflection

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science


Dive into the research topics of 'An algebraic semantics for MOF'. Together they form a unique fingerprint.

Cite this