Una semántica formal ejecutable para ocl y sus aplicaciones al análisis y a la validación de modelos

Resumen

Una práctica estándar en la ingeniería del software es la construcción de "modelos", Tres son las razones principales que avalan la metodología de desarrollo de software (MDA): en primer lugar, si los modelos se construyen en las fases iniciales d e análisis de requisitos y de diseño, es posible detectar errores antes de implementar el sistema; en segundo lugar, los modelos pueden servir como especificaciones que guíen las fases siguientes de desarrollo del sistema; en tercer lugar, si los modelos son suficientemente formales, es posible utilizarlos como punto de partida para un proceso riguroso de refinamiento que culmine en la generación (al menos parcial) del código que implemente el sistema. Este ha sido el contexto de la inves tigación presentada en esta tesis, a saber, el desarrollo de métodos y herramientas formales que permitan la aplicación rigurosa de la metodología MDA. El presente documento recoge los principales resultados científicos, tecnológicos y de transfe rencia de conocimientos a la industria que se han obtenido. La evolución de los lenguajes de modelado fue constante hasta la aparición de UML (Unified Modeling Language), convertido en la actualidad en el lenguaje estándar para el modelado de sistemas software. Dentro de este estándar, OCL (Object Constraint Language) es el lenguaje utilizado por los modeladores para expresar restricciones que añaden información a los diagramas UML y precisan su significado. OCL es, además, un lenguaje para realizar consultas (queries) sobre la información contenida en los modelos. En teoría, los modeladores pueden utilizar OCL para analizar y validar sus propios modelos, por tanto, no tienen que pasar esta tarea a otros ingenieros con una pre paración más intensa en matemáticas o en lógica formal. Sin embargo, en la práctica los modeladores sólo utilizarán OCL cuando se les proporcionen las herramientas adecuadas: sin ellas, el esfuerzo y la creatividad necesarios para analizar y vali dar sus modelos son incluso superiores a los requeridos para construir estos modelos. Actualmente son escasas las herramientas que proporcionan soporte al lenguaje OCL y una de las razones de esta situación es la falta de una semántica formal para el lenguaje OCL que está pacíficamente aceptada por todos los actores dentro de la comunidad UML. El objetivo principal de esta tesis es la elaboración de una semántica ecuacional para los diagramas de clase UML con restricciones OCL que permi