Verificación de modelos independientes de la plataforma : un caso de estudio

Tesina (Licenciatura en Informática) - Universidad Nacional de La Plata. Facultad de Informática, 2017.

1. Introducción -- 2. Desarrollo de software dirigido por modelos -- 2.1 Introducción -- 2.2 Características -- 2.3 Modelos -- 2.3.1 Transformaciones de modelos -- 2.4 Metamodelos -- 2.5 La arquitectura dirigida por modelos (MDA) -- 2.6 El lenguaje MOF -- 2.7 Resumen -- 3. El lenguaje OCL -- 3.1 Introducción -- 3.2 Restricciones en OCL -- 3.2.1 Invariantes -- 3.2.2 Pre y post condiciones -- 3.2.3 Expresión Body -- 3.2.4 Valores iniciales y derivados -- 3.2.5 Paquetes -- 3.3 Tipos y valores básicos -- 3.3.1 Valores inválidos -- 3.3.2 Ajuste de tipos -- 3.3.3 Expresiones Let -- 3.3.4 Expresiones de definición -- 3.4 Colecciones -- 3.4.1 Operaciones de colecciones -- 3.5 Objetos y propiedades -- 3.5.1 Propiedades: Atributos -- 3.5.2 Propiedades: Operaciones -- 3.5.3 Propiedades: Extremos de asociación y navegación -- 3.5.4 Propiedades predefinidas en todos los objetos -- 3.6 Resumen -- 4. El lenguaje JML -- 4.1 Introducción -- 4.2 Características principales -- 4.2.1 Precondiciones y postcondiciones -- 4.2.3 Modelo y fantasma -- 4.2.4 Especificación de comportamiento excepcional -- 4.2.5 Cuantificadores -- 4.2.6 Especificación de ciclos -- 4.3 ¿por qué usar JML? -- 4.4 Resumen -- 5. Herramientas utilizadas -- 5.1 Eclipse Modeling Framework (EMF) -- 5.2 El lenguaje ATL -- 5.2.1 Módulos ATL -- 5.2.2 Semántica de la ejecución de un módulo -- 5.3 Acceleo -- 5.3.1 Características del lenguaje -- 5.4 Plugin OCL -- 5.4.1 Classic OCL -- 5.4.2 Complete OCL -- 5.4.3 Metamodelo unificado o Pivot -- 5.5 MoDisco -- 5.6 OpenJML -- 5.7 Resumen -- 6. Traducción de OCL a JML -- 6.1 Motivación -- 6.2 Comparación de los lenguajes -- 6.2.1 diferencias semánticas -- 6.3 Función de traducción -- 6.3.1 Invariantes, precondiciones y postcondiciones -- 6.3.2 Tipos simples -- 6.3.3 Operadores y expresiones -- 6.3.4 Pseudovariables y operaciones predefinidas -- 6.3.5 Colecciones -- 6.3.6 Atributos y operaciones definidos -- 6.3.7 Expresión de cuerpo de operación -- 6.3.8 Valores iniciales y atributos derivados -- 6.3.9 Expresiones let -- 6.4 Resumen -- 7. Herramienta desarrollada -- 7.1 Diseño -- 7.2 Metamodelo JML -- 7.2.1 Elementos específicos de JML -- 7.3 Biblioteca de colecciones JML -- 7.4 Casos de estudio -- 7.4.1 Modelo Royal and Royal -- 7.4.2 Biblioteca -- 7.5 Traducción de modelo OCL a modelo JML -- 7.6 Traducción de modelo JML a código Java+JML -- 7.7 Ejecución de la herramienta -- 7.7.1 Modelo Royal and Loyal -- 7.7.2 Modelo de la biblioteca -- 7.8 Resumen -- 8. Trabajos relacionados -- 8.1 A Library-based Approach to Translating OCL contraints to JML Assertions for Runtime Checking -- 8.2 Desarrollo de una herramienta para la derivación automática de especificaciones OCL a JML -- 8.3 Pattern-based Mapping of OCL Specifications to JML contracts -- 8.4 Bidirectional Translation between OCL and JML for Round-trip Engineering -- 8.5 Lengujes formales y derivación automática de código de pruebas a partir de modelos de software con restricciones OCL -- 8.6 Aportes -- 9. Conclusiones y trabajos futuros -- 9.1 Conclusiones -- 9.2 Trabajos futuros -- 10. Bibliografía