Model-Driven Development is a field in Software Engineering that,
for several years, has represented software artifacts as models in
order to improve productivity, quality, and cost effectiveness.
Models provide a more abstract description of a software artifact
than the final code of the application. In this field, Model-Driven
Architecture (MDA) is an initiative, sponsored by the OMG, that is
constituted by a family of industry standards including: Meta-Object
Facility (MOF), Unified Modeling Language (UML), Object Constraint
Language (OCL), XML Metadata Interchange (XMI), and
Query/Views/Transformations (QVT). These standards provide common
guidelines for model-based tools and processes in order to improve
interoperability among executable frameworks, automation in the
software development process, and analysis techniques to avoid
errors during this process.


The MOF standard describes a generic framework where the abstract
syntax of modeling languages can be defined. This standard aims at
offering a good basis for Model-Driven Development processes,
providing some of the building blocks that are needed to support a
Model-Driven Development approach: what is a model, what is a
metamodel, what is reflection in a MOF framework, etc. However, most
of these concepts lack at present a formal semantics in the current
MOF standard. Furthermore, OCL is a constraint definition language
that permits adding semantics to a MOF metamodel. Unfortunately, the
relation between a metamodel and its OCL constraints also lacks a
formal semantics. This is, in part, due to the fact that metamodels
can only be defined as data in the MOF framework.

The MOF standard also provides the so-called MOF-Reflection
facilities, by means of a generic API, to manipulate software
artifacts that are made up out of objects. Broadly speaking,
\emph{reflection} is the capacity to represent entities that have a
formal semantics at a base level, such as types, as data at a
metalevel. Metalevel entities, once metarepresented, can be
computationally manipulated and transformed. This notion of
\emph{reflection} is still not supported in the MOF standard.

In this dissertation, we define a reflective, algebraic, executable
framework for precise metamodeling that provides support for the MOF
and the OCL standards. On the one hand, our formal framework
provides a formal semantics for the building blocks that are usually
involved in a Model-Driven Development process. On the other hand,
our framework provides an executable environment that is plugged
into the Eclipse Modeling Framework (EMF) and that constitutes the
kernel of a model management framework, supporting model
transformations and formal verification techniques. The main
contributions of this dissertation are:

\begin{itemize}
  \item The formal definition of the following notions: \emph{metamodel},
    \emph{model}, \emph{OCL constraint satisfaction}, and \emph{metamodel conformance}.
    We clearly distinguish the different roles that the notion of \emph{metamodel}
    usually plays in the literature: as data, as type and as theory.
    In addition, we have defined new notions: \emph{metamodel specification},
    capturing the relationship between
    a metamodel and its OCL constraints; \emph{metamodel realization}, referring to the
    mathematical representation of a metamodel; and \emph{model type} and \emph{constrained model type},
    allowing models to be considered as first-class citizens.

  \item A formal executable mechanism for metamodel reflection in the MOF framework,
    so that metamodels and models can be manipulated in a generic way.

  \item An algebraic executable metamodeling framework that is plugged into the Eclipse
    Modeling Framework, constituting a high-level prototyping environment to experiment with
    model management tasks where formal verification techniques can be applied.

  \item A set of prototypes that validate the ideas and notions that have been mathematically
    defined in this dissertation. These tools provide: OCL constraint validation and
    OCL query facilities, QVT-based model transformations, and model management tasks
    by means of generic algebraic operators. Some of these prototypes have already been
    applied in other universities to explore new areas of research, and in industry. Furthermore,
    we have shown how our algebraic MOF framework enables
    the application of formal verification techniques to graph rewriting systems with a simple example.
\end{itemize}

The outcome of this dissertation constitutes a mathematical
executable framework, where formal methods can be applied to several
areas of Software Engineering: precise definition of model-based
domain-specific languages, model-based formal verification
techniques (reachability analysis, model checking, inductive theorem
proving, OCL constraint validation, among others), formal definition
of model management tasks (model transformation, model merging,
traceability support, among others), as well as their application to
specific case studies.

Some preliminary experiments related with this dissertation have appeared in
\cite{DBLP:conf/jisbd/BoronatCR03,BoronatPCR-JUCS04,BoronatRC:CIT:2004,BoronatCR:NET:2005}.
Parts of this work have appeared in \cite{BoronatCR:CSMR:2005,DBLP:journals/entcs/BoronatCR05,BoronatCR-ECMDAFA05,BoronatICRG:JISBD:2005,BoronatCR-FASE06,BoronatCRL05-EVOL06,BoronatOGRC:ECMDA:2006,BoronatRC:WAFOCA:2006,BoronatCR:EASST:2006,GomezBCR:JISBD:2007a,MoraGRPBGCR:JISBD:2007,GomezBCR:JISBD:2007b}.