Enumeración breve de objetivos

A continuación se incluye una descripción clara, precisa y realista (según se exige en el impreso oficial) de los objetivos concretos que se persiguen en este proyecto. Con idea de que se puedan establecer conexiones con la finalidad del proyecto descrita anteriormente. Los objetivos se enumeran atendiendo a las tres áreas en las que se pretenden desarrollar las actividades:

Descripción semántica de componentes de software

  1. Desarrollo de mecanismos de composición y establecimiento de inconsistencias de sistemas basados en múltiples vistas multiparadigma. En particular nos centraremos en los casos de RM-ODP y UML, y utilizaremos Maude como formalismo.
  2. \item Desarrollo de un entorno de edición de interfaces de componentes, en el que la información proporcionada por los lenguajes de descripción de interfaces es complementada con información sobre los protocolos de interacción. Se pretende integrar esta herramienta en un entorno de desarrollo de componentes. En particular, la EPO Microsoft Research ha mostrado su interés en que se exploren estas posibilidades sobre .Net.
  3. Definición de un sistema de tipos y efectos para un lenguaje funcional, donde puedan expresarse propiedades de consumo de recursos. Desarrollo de un compilador-certificador que traduzca el lenguaje fuente y sus tipos anotados al lenguaje de una máquina abstracta similar a la de Java. Desarrollo de algoritmos de comprobación de que el código generado es consistente con sus anotaciones.
  4. Desarrollo de métodos de análisis de la terminación de programas Maude y Haskell, y estudio de la complejidad/eficiencia de los cómputos. Con relación a los aspectos de coordinación se propone el análisis modular de propiedades (de aplicación 'interna', dentro de un programa modular o basado en componentes) y, desde una perspectiva más global, abierta a la utilización de las técnicas desarrolladas en entornos accesibles mediante Internet, también la incorporación de herramientas en entornos de desarrollo globales como .NET.

Verificación y depuración de software

  1. Desarrollo de un entorno asistido por computador para la verificación de propiedades (CAPA --- Computer Aided Property Analysis---) sobre componentes. El entorno será modular y estará compuesto por tres núcleos fundamentales: un núcleo de verificación (en el que se integrarán técnicas de model checking e interpretación abstracta), un módulo semántico (que incluirá un motor de inferencia definiendo la semántica operacional del formalismo utilizado para expresar el protocolo de comportamiento de las componentes a analizar) y un módulo de propiedades (que permitirá la descripción de propiedades en alguna lógica).
  2. Desarrollo de tecnología declarativa para la extracción, evaluación y combinación de modelos comprensibles del conocimiento a partir de modelos modelos igualmente precisos pero poco inteligibles.
  3. Desarrollo de técnicas híbridas de verificación y depuración para sistemas de software complejos que combinan la depuración algorítmica, síntesis de programas, analisis estático y model checking

Optimización de programas declarativos multiparadigma

  1. Una implementación de alto nivel de un lenguaje declarativo multiparadigma mediante su compilación a Prolog, capaz de gestionar el paralelismo implícito del programa original e integrar, en tiempo de compilación, optimizaciones de código inspiradas en las técnicas de transformación de programas.
  2. Integrar la noción de ''fuzziness'' en el marco de los lenguajes declarativos multiparadigma y estudiar técnicas de transformación basadas en ''reglas+estrategias'' y evaluación parcial para este nuevo tipo de lenguajes.
  3. Desarrollo de técnicas para identificar aquellos elementos de control programables (e.g., estrategias) que pueden ser adecuadamente `sintonizados' para conseguir mejoras concretas en el comportamiento del programa (en el caso de Maude y Elan). También se investigará la mejora de las estrategias fijas utilizadas en el lenguaje Haskell.
La investigación que se propone en este proyecto se adecúa perfectamente a las prioridades del Programa Nacional de Tecnologías Informáticas (TIN), especialmente en la prioridad temática Fiabilidad y calidad de sistemas de software, y cubre diversos aspectos de los siguientes objetivos prioritarios de la línea temática Tecnologías de soporte y desarrollo de software del anexo de la convocatoria:
  1. Técnicas de análisis y certificación de código.
  2. Teorías, lenguajes y herramientas de especificación, síntesis y verificación de software.
  3. Teorías, lenguajes y herramientas que den soporte automatizado al análisis, simulación y prueba de componentes.
También existe una conexión directa con la línea temática Ingeniería del Software de ese mismo anexo, pues se pretende abordar el objetivo prioritario:
  • Reutilización de software desde las etapas iniciales. Arquitecturas de software. Componentes comerciales y de código abierto. Metodologías ágiles.