Verificación de modelos independientes de la plataforma

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