Verificación de restricciones de modelo, estáticas y dinámicas, en entornos atómicos para lenguajes orientados a objetos

  1. Fernández Álvarez, Alberto Manuel
Dirixida por:
  1. Daniel Fernández Lanvín Director
  2. Raúl Izquierdo Castanedo Co-director

Universidade de defensa: Universidad de Oviedo

Fecha de defensa: 27 de novembro de 2015

Tribunal:
  1. Juan Manuel Cueva Lovelle Presidente/a
  2. José Baltasar García Pérez-Schofield Secretario
  3. Beatriz Pérez Valle Vogal

Tipo: Tese

Teseo: 397828 DIALNET

Resumo

Una parte fundamental de la fase de análisis en cualquier proyecto de desarrollo de software es descubrir y documentar el dominio. De entre todas las posibles estrategias o técnicas que se pueden aplicar para esta actividad, destaca la basada en la construcción y representación gráfica de un modelo de ese dominio. El modelo representa un mapa conceptual relacionando los conceptos fundamentales del dominio, y establece un lenguaje común a todos los participantes del desarrollo. Los elementos principales de ese modelo son las entidades, sus relaciones y también las restricciones que les afectan. En esta fase del desarrollo es habitual describir las restricciones en lenguaje natural o bien con algún lenguaje orientado a ese propósito, por ejemplo Object Constraint Language (OCL) en el estándar UML. Sin embargo, trasladarlas posteriormente al modelo de implementación de forma correcta presenta diversas cuestiones que deben ser resueltas manualmente por el desarrollador: cómo traducirlas, cuándo chequearlas, sobre qué instancias, qué hacer en caso de incumplimiento de alguna y cómo hacerlo de forma eficiente son quizá las más acuciantes. En este trabajo se propone una solución automatizada que libera al programador de esas responsabilidades y que es aplicable a los lenguajes orientados a objetos más populares, no fuerza el diseño natural de las aplicaciones, ofrece un rendimiento aceptable, es integrable con sistemas que provean atomicidad y da soporte a restricciones estáticas y dinámicas. La solución se basa en el empleo de técnicas de chequeo incremental de restricciones y generación de código de instrumentación y verificación. Partiendo de una de las técnicas analizadas en el estado del arte se presentan dos extensiones que permiten abarcar toda la gama de restricciones objetivo así como las de naturaleza recursiva. La eficiencia se comprueba sobre prototipos que integran la solución en varios entornos de ejecución con y sin atomicidad (grafo en memoria, grafo virtual con mapeadores objeto relacional y grafo en sistemas de memoria transaccional software).