El objetivo de este artículo es describir las principales características del proceso de desarrollo de software basado en modelos, destacando la necesidad de integrar lenguajes de modelado gráficos, cercanos a las necesidades del dominio de la aplicación, con lenguajes de modelado formales, provistos de herramientas de análisis y verificación. A partir de la estandarización del lenguaje gráfico de modelado Unified Modeling Language (UML) han surgido activas discusiones acerca de la precisión semántica de sus construcciones. Mientras que el OMG fue responsable por la estandarización de UML como notación, la semántica de UML aún es un tema de investigación. Existe un número importante de trabajos teóricos que tratan diferentes partes de UML definiendo formalmente su semántica. En este artículo hemos seleccionamos los más representativos y los hemos clasificado en dos grupos: formalizaciones basadas en el modelo y formalizaciones basadas en el metamodelo. Realizamos un análisis comparativo de ambos grupos y finalmente describimos una propuesta intermedia que formaliza UML mediante una teoría formal de primer orden.