Date post: | 31-Dec-2015 |
Category: |
Documents |
Upload: | zephania-estrada |
View: | 34 times |
Download: | 2 times |
Especificación y Verificación de Transformaciones de Modelos
Horacio LópezFernando VaresiMarcelo Viñolo
Situación
Especificación E1
Implementación I1
Especificación E2
Implementación I2
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Desarrollo Guiado por Modelos (Model Driven Development, MDD)
•Enfoque de ingeniería de software basado en el
modelado de un sistema como la principal actividad del desarrollo y la construcción
del mismo guiada por transformaciones de
dichos modelos.
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
refiererefiere
escribe
Transformación de modelos
Metamodelo Origen
Metamodelo Destino
Definición de Transformació
n
Motor de Transformacion
es
Modelo Destino
Modelo Origen
conforma conformaejecuta
lee
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Aplicaciones de transformaciones•Generar modelos de bajo nivel
(eventualmente código) a partir de modelos de alto nivel
• Ingeniería inversa de modelos de alto nivel a partir de modelos de bajo nivel o código.
•Mapeo y sincronización entre modelos.
•Crear vistas de un sistema basadas en una consulta
•Evolucionar modelos (ej: refactoring)
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Descripción del proyecto
•Objetivos:▫Realizar un estudio del estado del arte
sobre: lenguajes y herramientas existentes para la
especificación de transformaciones de modelos
verificación de estas transformaciones
▫Aplicación de lo relevado a nivel práctico a un caso de estudio.
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Descripción del proyecto•Resultados esperados:
▫Estudio del marco teórico de MDD y de la transformación de modelos.
▫1er. reporte técnico: lenguajes y mecanismos para especificar transformaciones de modelos.
▫2do. reporte técnico: técnicas y herramientas de validación y verificación de modelos y de transformaciones.
▫Aplicación práctica de los resultados mediante un caso de estudio.
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Lenguajes y Herramientas de Transformación
Lenguajes y Herramientas
•Relevamiento de trabajos actuales sobre especificación de transformaciones
•Caracterización:▫Generales▫Metamodelos▫Reglas de transformación
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Caracterización de los enfoques de transformación•Modelo-Modelo y Modelo-Texto•Características generales
▫Múltiples modelos origen/destino?▫Transformación “in-place”?▫Incrementabilidad▫Multidireccionalidad?▫Mecanismos de trazabilidad?
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Caracterización de los enfoques de transformación•Características de los metamodelos
▫Transformación endógena o exógena▫Transformación horizontal o vertical
horizontal vertical
endógena refactoring refinamiento
exógena traducción o migración de lenguaje
generación de código
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Caracterización de los enfoques de transformación•Características de las reglas de
transformación▫Precondiciones de aplicación (guardas)▫Parametrización y re-uso de reglas▫Detección y órden de aplicación
Éstas y otras características fueron documentadas
en el primer reporte técnico.
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Enfoques de transformación
•Manipulación directa•Operacional•Relacionales•Basados en transformaciones de grafos•Híbridos
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Enfoques de Transformación• Manipulación directa
▫Lenguaje de propósito general▫Representación de modelos adecuada al lenguaje.▫Ausencia de mecanismos dedicados a
transformaciones.▫Ejemplo: SiTra
• Operacional▫Similar a programación imperativa.▫ Incorpora mecanismos de trazabilidad, etc.▫Orden de ejecución explícito.▫Ejemplos: Kermeta, QVT-Operational
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Enfoques de Transformación
•Relacionales▫El concepto principal son relaciones
matemáticas entre modelo origen y destino.▫Alto nivel de abstracción (mayor
legibilidad)▫En general, no admite actualizaciones in-
place.▫Creación de elementos es implícita.▫Orden de ejecución no es explícito.
pero se puede condicionar mediante precondiciones
▫Ejemplos: Tefkat, QVT-Relations
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Enfoques de Transformación
•Basados en Transformaciones de Grafos▫Se utilizan grafos tipados, con atributos y
etiquetas.▫Reglas se componen de un lado izquierdo y
derecho.▫Propiedades matemáticas basadas en la
teoría subyacente (ej: alcanzabilidad de un nodo).
▫Ejemplos: AGG, AToM3, Viatra, MOLA
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Enfoques de Transformación• Híbridos
▫Combina enfoques anteriores para sumar ventajas.
▫QVT Estándar definido por OMG. Emplea OCL y MOF. Transformaciones modelo-modelo
▫ATL Sigue lineamientos de QVT RFP Transformaciones unidireccionales Modelo origen es read-only Modelo destino es write-only
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Verificación de Transformaciones de Modelos
Verificación de transformaciones•Relevamiento de trabajos actuales sobre
verificación▫Categorización▫Análisis de características, fortalezas y
debilidades
•Categorías▫Casos de prueba▫Model-checking▫Métodos deductivos
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Casos de prueba•Verificación dinámica a nivel de modelos•Se trabaja sobre un conjunto representativo
del dominio.•Pasos:
▫Generación Complejidad de exploración del espacio de
modelos▫Validación▫Ejecución
Cómo generar el resultado esperado? Cómo comparar resultados?
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Model-Checking• Verificación dinámica (modelos) o estática (transf.)• Prueba autómatica de propiedades sobre modelos
y/o transformaciones• Ambos deben ser expresados como grafos• Fortalezas:
▫Facilidad de uso▫No requiere asistencia del usuario
• Debilidades:▫Lenguaje restringido para asegurar automaticidad▫Complejidad crece exponencialmente con el tamaño
del modelo.
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Métodos Deductivos• Verificación estática a nivel de metamodelos• Centrado en la realización de pruebas formales• Especificaciones formales de los metamodelos y
transf.• Fortalezas:
▫ Brinda certeza absoluta▫ Lenguaje expresivo de propiedades▫ Generación de implementaciones de transformación
correctas• Debilidades:
▫ Verificación manual o semi-automática.▫ Requiere experiencia en lenguajes formales y/o
herramientas matemáticas
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Caso de Estudio
Caso de estudio
•Aplicación de conocimientos sobre transformaciones
•Enmarcado en una técnica de verificación que utiliza métodos deductivos.
•A continuación…▫Técnica de verificación▫Transformación desarrollada▫Diseño prototipo
Técnica de Verificación
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Especificación formal de
metamodelos en Coq
Traducción de reglas de transf. a fórmulas lógicas
Elaboración de prueba formal
Transformación del prototipo
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
refiererefiere
escribe
Metametamodelo KM3
Metametamodelo Coq
Definición de Transformació
n
Motor de Transformacion
es
Metamodelo destino en Coq
Metamodelo origen en KM3
conforma conformaejecuta
lee
KM3 – Coq
•KM3▫Lenguaje de metamodelado textual▫Sintaxis similar a Java▫Popular en comunidad de usuarios de ATL
•Coq▫Asistente de pruebas que permite :
Expresar modelos matemáticos complejos Expresar propiedades sobre los modelos Verificar propiedades
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Proceso de transformación
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Modelo origenMetamodelo UML en UML Metamodelo UML en KM3
package UML {abstract class Classifier {attribute name : String;}
class Class extends Classifier {
reference pack : Package
…}……
}
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Transformación ATL
•Especificación puramente declarativa (relacional).
•Relaciones:▫Clase => Tipo Inductivo (TI)▫Atributo/Referencia => Componente del TI▫Identidad de objetos => Componente oid▫Herencia => Componente del TI
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Transformación ATLrule AbstractClass2InductiveType {from
i: KM3!Class (i.isAbstract)to
o: COQ!InductiveType (isAbstract <- i.isAbstract,name <- i.name,hasComponents <- i.structuralFeatures,subTypes <- i.subclasses,superTypes <- i.supertypes
)}
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Transformación Xtext
•Basado en templates (Xpand)•Traducción a sintaxis Coq.•Genera funciones auxiliares para la
construcción de pruebas formales:▫Proyecciones▫Comparación de objetos▫Casting▫Chequeo de tipos
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
ResultadoModelo Origen Modelo Destino
package UML {abstract class Classifier {
attribute name : String;}
class Class extends Classifier {
reference pack : Package
…}……
}
Inductive Classifier : Set := | Build_Classifier (name :
string) (subClass : option Class)
withClass : Set := | Build_Class (oid : nat)
(pack : Package)……
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Conclusiones
Conclusiones…• Existe una gran diversidad de técnicas,
herramientas y lenguajes de transformación de modelos.
• El enfoque a utilizar depende de la naturaleza del problema y no existe uno que contemple todas las necesidades posibles.
• El primer reporte técnico presenta una taxonomía que permite clasificar los enfoques y seleccionar el más adecuado para un problema particular.
• Entornos y herramientas “inmaduros” y en permanente perfeccionamiento.
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Conclusiones…
•Las técnicas de verificación difieren en el grado de certeza que brindan.
•Trabajan en diferentes niveles de abstracción
•El segundo reporte técnico presenta una clasificación y descripción de técnicas de verificación.
•Las herramientas que asisten la verificación en gral. no se encuentran integradas a las de desarrollo.
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
Conclusiones
•Se implementó un prototipo para semi-automatizar una técnica de verificación basada en métodos deductivos.
Introducción – Enfoques – Verificación – Caso de Estudio – Conclusiones
GRACIAS