Daniel|
Calegari|
dcalegar@fing.edu.uy|
Instituto de Computación, Facultad de Ingeniería|
Verificación de Transformaciones de Modelos|
ingeniería dirigida por modelos, transformaciones de modelos, verificación formal|
INVESTIGACION|
|
Esta charla presentará los avances de un trabajo de investigación sobre la construcción de un framework de certificación de transformaciones de modelos, mecanismo de construcción por excelencia en el contexto de la Ingeniería Dirigida por Modelos. El framework se basa en el Cálculo de Construcciones Inductivas (CCI), permitiendo la representación de metamodelos (expresados con el lenguaje KM3) como tipos en CCI, y transformaciones de modelos (expresados en ATL) como axiomas (predicados lógicos) en CCI. Sobre estas representaciones se pueden realizar pruebas de corrección de transformaciones, utilizando como criterio de corrección la satisfacción de propiedades específicas de estas últimas. El framework y las pruebas de corrección se realizan integradamente utilizando el asistente de pruebas Coq.|