Grupo de Computación Teórica de la Facultad de Ingeniería
Grupo de Computación Teórica

Verificación de Transformaciones de Modelos de Comportamiento Basados en UML

Convocatoria: Fondo Clemente Estable (FCE 2007)

Fuente de financiamiento: Agencia Nacional de Investigación e Innovación.

Duración: 20 meses.

Fecha de aprobación: diciembre de 2008.

Fecha de comienzo: febrero de 2009.

Fecha de finalización: octubre de 2010.

Palabras clave: Model-Driven Development, UML, Formal Methods.

Resumen

El Desarrollo de Software Guiado por Modelos (Model-Driven Development, MDD) es un enfoque de ingeniería de software basado en el modelado de un sistema como la principal actividad del desarrollo.

La construcción del sistema es guiada por transformaciones de dichos modelos, terminando en la generación automática de código. Su éxito depende fuertemente de la disponibilidad de lenguajes y herramientas apropiados para realizar las transformaciones entre modelos y validar su corrección.

La mayoría de las técnicas de MDD utilizan el Unified Modeling Language (UML) como lenguaje de modelado, considerado el estándar de facto a nivel académico e industrial.

La validación de una transformación incluye la verificación de la corrección sintáctica de la misma y de los modelos producidos, así como la corrección semántica de la transformación, es decir, la preservación de la corrección del modelo resultante con respecto al correspondiente modelo original.

Muy pocas propuestas se ocupan de este último punto. Adicionalmente, la mayoría de las técnicas de transformación se enfocan en la transformación de la estructura del sistema, dejando de lado su comportamiento.

El objetivo principal de este proyecto es desarrollar herramientas para la definición y verificación de transformaciones de modelos de software, con el propósito de mejorar la calidad y la confiabilidad de los productos desarrollados utilizando el enfoque MDD.

Se pretende contribuir a la especificación formal de transformaciones de modelos de comportamiento especificados en UML, con el objetivo de hacer posible la verificación formal de la corrección sintáctica y semántica de dichas transformaciones.