El Desenvolupament de Programari Dirigit per Models Žs una branca de l'Enginyeria del Programari, on els artefactes de programari es representen com models per a incrementar la productivitat, qualitat i eficincia econ˜mica en el procŽs de desenvolupament de programari, on un model proporciona una representaci— abstracta del codi final d'una aplicaci—. En aquest camp, la iniciativa Model-Driven Architecture (MDA), patrocinada per l'OMG, estˆ constitu\"ida per una fam’lia d'estˆndars industrials, entre els quals destaquem: Meta-Object Facility (MOF), Unified Modeling Language (UML), Object Constraint Language (OCL), XML Metadata Interchange (XMI), i Query/Views/Transformations (QVT). Aquestos estˆndars proporcionen unes directrius comunes per a eines basades en models i per a processos de desenvolupament de programari dirigits per models. El seu objectiu consisteix en millorar la interoperabilitat entre marcs de treball executables, en automatitzar el procŽs de desenvolupament de programri i en proporcionar tcniques que eviten errors durant aquest procŽs. L'estˆndar MOF descriu un marc de treball genric que permet definir la sintaxi abstracta de llenguatges de modelat. Aquest estˆndar persegueix la definici— dels fonaments per a processos de desenvolupament de programari dirigits per models: qu Žs un model, qu es un metamodel, qu Žs la reflexi— en un marc de treball basat en MOF, etc. No obstant aix˜, la majoria d'aquestos conceptes manquen d'una semˆntica formal en la versi— actual de l'estˆndar MOF. A mŽs a mŽs, OCL s'empra com un llenguatge de definici— de restriccions que permet afegir semˆntica a un metamodel MOF. Malauradament, la relaci— entre un metamodel i les seues restriccions OCL tambŽ manquen d'una semˆntica formal. Aquest fet es deu, en part, a que els metamodels œnicament poden ser definits com a data en un marc de treball basat en MOF. L'estˆndar MOF tambŽ proporciona les anomenades facilitats de reflexi— MOF (\emph{MOF Reflection facilities}), mitjanant una API genrica que permet manipular artefactes de programari que estan composats per objectes. De manera informal, \emph{reflexi—} es la capacitat per a representar entitats que tenen una semˆntica formal en un nivell base, com per exemple tipus, com a dades en un metanivell. Les entitats del metanivell poden ser manipulades i transformades computacionalment. Aquesta noci— de \emph{reflexi—} encara no estˆ suportada en l'estˆndar MOF. En aquesta tesi, es defineix un marc de treball reflexiu, algebraic i executable per al metamodelat prec’s, proporcionant suport per als estˆndars MOF i OCL. D'una banda, la nostra aproximaci— proporciona una definici— formal de les nocions bˆsiques que s'empren en processos de desenvolupament de programari dirigits per models. D'altra banda, el nostre marc de treball proporciona un entorn executable que estˆ integrat en l'eina Eclipse Modeling Framework (EMF), i que constitueix el nucli d'una eina de gesti— de models, donant suport a transformacions de models i tcniques de verificaci— formal. Les principals constribucions d'aquesta tesi s—n: \begin{itemize} \item La definici— formal de les seg\"uents nocions: \emph{metamodel}, \emph{model}, \emph{satisfacci— de restriccions OCL}, i \emph{correcci— sintˆctica} d'un model. En aquest treball es distingueix d'una manera clara les diferents situacions en les quals s'empra el concepte de metamodel en la literatura: com a data, com a tipus, i com a teoria. Amb aquest objectiu, s'han incorporat les seg\"uent nocions: \emph{especificaci— de metamodel}, capturant la relaci— entre un metamodel i les seues restriccions OCL; \emph{realitzaci— d'un metamodel}, fent referncia a la representaci— matemˆtica d'un metamodel; i \emph{tipus de model} i \emph{tipus de model amb restriccions}, permetent definir models com a entitats de primer ordre. \item Un mecanisme formal i executable de reflexi— de metamodels en el marc de treball MOF, de manera que models i metamodels poden ser manipulats de manera genrica. \item Un marc de metamodelat algebraic i executable que estˆ integrat en Eclipse Modeling Framework, constituint un prototip d'alt nivell per tal d'experimentar amb tasques de gesti— de models, en les quals es poden aplicar tcniques de verificaci— formal. \item Un conjunt de prototips que validen les idees i nocions que s'han definit matemˆticament en aquesta tesi. Aquestes eines proporcionen: facilitats per a la validaci— de restriccions OCL i avaluaci— de consultes OCL, transformacions de models basades en QVT, i gesti— de models mitjanant operadors algebraics genrics. Alguns d'aquestos prototips s'han aplicat en altres universitats per a explorar noves ˆrees d'investigaci—. D'altres s'han aplicat en indœstria. A mŽs a mŽs, s'ha presentat com es poden aplicar tcniques de verificaci— formal a un sistema de reescriptura de grafs en el nostre marc de treball MOF mitjanant un exemple senzill. \end{itemize} El resultat d'aquesta tesi constitueix un prototip de metamodelat matemˆtic i executable, on mtodes formals es poden aplicar a diverses ˆrees de l'Enginyeria del Software: definici— formal de llenguatges espec’fics a domini basats en models, tcniques de verificaci— formal basades en models (anˆlisi d'arribada, model checking, demostració inductiva de teoremes, validaci— de restriccions OCL, entre altres), definici— formal de tasques de gesti— de models (transformaci— de models, integraci— de models, suport per a traabilitat, entre altres), i les seues aplicacions a casos d'estudi espec’fics. Alguns experiments preliminars foren publicats en \cite{DBLP:conf/jisbd/BoronatCR03,BoronatPCR-JUCS04,BoronatRC:CIT:2004,BoronatCR:NET:2005}. Algunes parts d'aquest treball han aparegut 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}.