El Desarrollo de Software Dirigido por Modelos es una rama de la Ingenier’a del Software en la que los artefactos software se representan como modelos para incrementar la productividad, calidad y eficiencia econ—mica en el proceso de desarrollo de software, donde un modelo proporciona una representaci—n abstracta del c—digo final de una aplicaci—n. En este campo, la iniciativa Model-Driven Architecture (MDA), patrocinada por la OMG, est‡ constituida por una familia de est‡ndares industriales, entre los que se destacan: Meta-Object Facility (MOF), Unified Modeling Language (UML), Object Constraint Language (OCL), XML Metadata Interchange (XMI), y Query/Views/Transformations (QVT). Estos est‡ndares proporcionan unas directrices comunes para herramientas basadas en modelos y para procesos de desarrollo de software dirigidos por modelos. Su objetivo consiste en mejorar la interoperabilidad entre marcos de trabajo ejecutables, en automatizar el proceso desarrollo de software de software y en proporcionar tŽcnicas que eviten errores durante ese proceso. El est‡ndar MOF describe un marco de trabajo genŽrico que permite definir la sintaxis abstracta de lenguajes de modelado. Este est‡ndar persigue la definici—n de los conceptos b‡sicos que son utilizados en procesos de desarrollo de software dirigidos por modelos: quŽ es un modelo, quŽ es un metamodelo, quŽ es reflexi—n en un marco de trabajo basado en MOF, etc. Sin embargo, la mayor’a de estos conceptos carecen de una sem‡ntica formal en la versi—n actual del est‡ndar MOF. Adem‡s, OCL se utiliza como un lenguage de definici—n de restricciones que permite a\~{n}adir sem‡ntica a un metamodelo MOF. Desafortunadamente, la relaci—n entre un metamodelo y sus restricciones OCL tambiŽn carece de una sem‡ntica formal. Este hecho es debido, en parte, a que los metamodelos s—lo pueden ser definidos como dato en un marco de trabajo basado en MOF. El est‡ndar MOF tambiŽn proporciona las llamadas facilidades de reflexi—n de MOF (\emph{MOF Reflection facilities}), mediante una API genŽrica que permite manipular artefactos software que est‡n compuestos por objetos. De manera informal, \emph{reflexi—n} es la capacidad para representar entidades que tienen una sem‡ntica formal en un nivel base, como por ejemplo tipos, como datos en un metanivel. Las entidades del metanivel pueden ser computacionalmente manipuladas y transformadas. Esta noci—n de \emph{reflexi—n} aœn no est‡ soportada en el est‡ndar MOF. En esta tesis, se define un marco de trabajo reflexivo, algebraico y ejecutable para el metamodelado preciso, que proporciona soporte para los est‡ndares MOF y OCL. Por una parte, nuestra aproximaci—n proporciona una definici—n formal de las nociones b‡sicas que se utilizan en procesos de desarrollo de software dirigidos por modelos. Por otra parte, nuestro marco de trabajo proporciona un entorno ejecutable que est‡ integrado en la herramienta Eclipse Modeling Framework (EMF), y que constituye el nœcleo de una herramienta de gesti—n de modelos, dando soporte a transformaciones de modelos y tŽcnicas de verificaci—n formal. Las principales contribuciones de esta tesis son: \begin{itemize} \item La definici—n formal de las siguientes nociones: \emph{metamodelo}, \emph{modelo}, \emph{satisfacci—n de restricciones OCL}, y \emph{correcci—n sint‡ctica} de un modelo. En este trabajo se distingue de una manera clara las diferentes situaciones en las que se utiliza el concepto de metamodelo en la literatura: como dato, como tipo y como teor’a. Con este objetivo, se han definido, adem‡s, las siguientes nociones: \emph{especificaci—n de metamodelo}, capturando la relaci—n entre un metamodelo y sus restricciones OCL; \emph{realizaci—n de un metamodelo}, haciendo referencia a la representaci—n matem‡tica de un metamodelo; y \emph{tipo de modelo} y \emph{tipo de modelo con restricciones}, permitiendo definir modelos como entidades de primer orden. \item Un mecanismo formal y ejecutable de reflexi—n de metamodelos en el marco de trabajo MOF, de manera que modelos y metamodelos se pueden manipular de manera genŽrica. \item Un marco de metamodelado algebraico y ejecutable que est‡ integrado en Eclipse Modeling Framework, constituyendo un prototipo de alto nivel para expermientar con tareas de gesti—n de modelos, en las que se pueden aplicar tŽcnicas de verificaci—n formal. \item Un conjunto de prototipos que validan las ideas y nociones que se han definido matem‡ticamente en esta tesis. Estas herramientas proporcionan: facilidades para la validaci—n de restricciones OCL y evaluaci—n de consultas OCL, transformaciones de modelos basadas en QVT, y gesti—n de modelos mediante operadores algebraicos genŽricos. Algunos de estos prototipos se han aplicado en otras universidades para explorar nuevas ‡reas de investigaci—n, y tambiŽn en industria. Adem‡s, se ha presentado c—mo se pueden aplicar tŽcnicas de verificaci—n formal a un sistema de reescritura de grafos en nuestro marco de trabajo MOF mediante un ejemplo sencillo. \end{itemize} El resultado de esta tesis constituye un prototipo de metamodelado matem‡tico y ejecutable, donde mŽtodos formales se pueden aplicar a varias ‡reas de la Ingenier’a del Software: definici—n precisa de lenguajes espec’ficos de dominio basados en modelos, tŽcnicas de verificaci—n formal basadas en modelos (an‡lisis de alcanzabilidad, model checking, demostraci—n inductiva de teoremas, validaci—n de restricciones OCL, entre otras), definici—n formal de tareas de gesti—n de modelos (transformaci—n de modelos, integraci—n de modelos, soporte para trazabilidad, entre otros), y sus aplicaciones a casos de estudio espec’ficos. Algunos experimentos preliminares fueron publicados en \cite{DBLP:conf/jisbd/BoronatCR03,BoronatPCR-JUCS04,BoronatRC:CIT:2004,BoronatCR:NET:2005}. Algunas partes de este trabajo han aparecido en \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}.