Subproyecto 2: Universidad de Valencia

Módulo M-2.1: Análisis, Optimización y Coordinación de Componentes de Software
    Los sistemas de reescritura son útiles para modelar los cómputos de los programas de lenguajes funcionales reales como Maude, Elan, Haskell, etc., cuyo mecanismo operacional básico es la reducción de expresiones. Sin embargo, a diferencia de los sistemas de reescritura, los programas funcionales pueden incorporar elementos expresivos tales como:

    • Reglas condicionales, cuya parte condicional puede incluir no sólo ecuaciones, sino también expresiones de tipificación, de ajuste a patrones, etc.
    • Tipos / Subtipos / Sorts.
    • Polimorfismo / Sobrecarga
    • Orden superior
    • Operadores asociativos, conmutativos, idempotentes, etc.
    • Estrategias, tanto implícitas como explícitamente definidas por el programador (mediante lenguajes de estrategias).
    • Módulos (posiblemente paramétricos) / Tipos abstractos de datos / Clases.

    Esta variedad expresiva hace que el análisis formal de los programas funcionales sea mucho más laborioso, tanto desde el punto de vista del modelado como en cuanto al diseño y uso de técnicas de análisis y optimización. Esto se refleja, desde el punto de vista lógico que subyace a los lenguajes declarativos, en la necesidad de considerar lógicas capaces de modelar estas características avanzadas y permitir razonar sobre ellas. Ejemplos concretos son la Rewriting Logic o la Membership Equational Logic

    El objetivo del módulo es desarrollar técnicas formales de análisis y optimización que sean aplicables a los programas de los lenguajes funcionales anteriores, teniendo en cuenta para ello toda la complejidad expresiva y estructural de los programas que éstos permiten definir. Todas las tareas propuestas, por tanto, deberán tratar (totalmente o en parte, pero de forma conjunta) los aspectos anteriores con el fin de obtener herramientas utilizables con lenguajes reales.

    1. En lo que respecta a los aspectos de análisis y verificación se propone:
      • el análisis de terminación de programas Maude y Haskell.
      • el estudio de la complejidad / eficiencia de los cómputos de programas Maude y Haskell.
    2. En lo tocante a la optimización de componentes se propone desarrollar 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.
    3. 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.

Módulo M-2.2: Técnicas declarativas para la extracción de reglas

    En este módulo nos proponemos investigar y desarrollar técnicas para la extracción de conocimiento en forma de reglas más potentes y expresivas, explotando completamente las características declarativas que se desprenden del uso de los formalismos lógicos en computación, como las lógicas integradas para entornos multi-paradigmas, el orden superior o la recursión. Otra cuestión de gran importancia por sus repercusiones en la sociedad en general es la aplicabilidad y utilidad de los modelo extraídos. Obviamente, no sólo se deben extraer patrones de los datos, sino que éstos deben ser comprensibles para que los usuarios de los mismos puedan usarlos, por ejemplo como ayuda a la toma de decisiones. Asimismo, la aplicabilidad de una técnica concreta también depende de que permita abordar problemas de alta complejidad estructural (en especial documentos XML y páginas web) o problemas donde el uso de la información de contexto (costes, p.ej.) es fundamental, y que esto sea posible con grandes volúmenes de datos para aplicarse de una manera habitual en la minería de datos. Además, la inducción declarativa no puede dar la espalda a nuevas técnicas, como los métodos ensemble y la combinación. Sin embargo, estas nuevas técnicas conllevan una pérdida de comprensibilidad (una de las grandes ventajas de la inducción declarativa), requieren muchos recursos, o no están diseñadas para minimizar muchos de los costes que hemos resaltado.

    Parece necesario aprovechar las posibilidades del análisis semántico que permiten los lenguajes declarativos, en particular los lenguajes integrados, para estudiar las posibilidades para la extracción de modelos comprensibles a partir de modelos combinados, a través de estudios de simplificación de modelos, la equivalencia aproximada de programas, etc. Por ello, en este módulo también nos proponemos desarrollar nuevos métodos de extracción de patrones comprensibles a partir de modelos precisos pero poco inteligibles.

Módulo M-2.3: Verificación y Depuración de Software

    En los últimos años, la demanda de software fiable y de calidad ha crecido mucho más rápido que la tecnología necesaria para su producción. La complejidad y el tamaño de los programas actuales exigen el uso de herramientas formales ágiles que aseguren la construcción de software fiable y correcto. Asimismo, con el crecimiento explosivo de la ``tecnología de la información'', cobran enorme relevancia los análisis y demostraciones de propiedades de seguridad, que pueden ayudar a evitar, por ejemplo, graves errores en protocolos de comunicación y servicios web. Los lenguajes utilizados en este ámbito (XML, HTML, etc.) plantean el reto de adaptar convenientemente las técnicas clásicas de verificación, depuración, etc., para abordar este tipo de problemas.

    Las técnicas de verificación de programas permiten demostrar que un programa satisface sus especificaciones. La comprobación de modelos (o model checking) es una aproximación específica para la verificación eficiente de propiedades de sistemas concurrentes y reactivos que tiene especial aplicación en el área de los sistemas de estados finitos. Este tipo de técnicas son, pues, especialmente adecuadas para abordar los problemas planteados por los sistemas anterioremente mencionados. La verificación de la corrección de un sistema de software puede verse oportunamente acompañada por el intento de corregir cualquier posible anomalía detectada. Las técnicas de depuración de programas permiten detectar las causas que introducen discrepancias entre el comportamiento real y el comportamiento que se espera de un programa ayudando a corregir, en su caso, las disfunciones encontradas (incorporando por ejemplo técnicas de aprendizaje inductivo de programas). Puesto que tanto la verificación como la depuración de programas necesitan considerar algún tipo de representación computable de la semántica de los sistemas considerados, la interpretación abstracta, como marco general que permite diseñar, aproximar y comparar semánticas de programas que expresan varios tipos de propiedades observables aporta una componente esencial que añadir a las técnicas de verificación y depuración. En el marco de la interpretación abstracta pueden inferirse propiedades que pueden usarse para certificar condiciones de seguridad, además del uso tradicional que se hace en los compiladores para optimizar el código generado estáticamente. Por supuesto, existen muchas similitudes entre todas estas técnicas en cuanto a sus objetivos y dominios de aplicación. Con la creciente necesidad de métodos formales ágiles para el desarrollo correcto de software cada vez más complejo (sistemas abiertos, con un número infinito de estados y/o empotrados), cobran especial relevancia los métodos híbridos que combinan las distintas técnicas. Así pues, el principal objetivo de este módulo es el desarrollo de técnicas híbridas de verificación y depuración que combinan la depuración algorítmica, la síntesis de programas, el analisis estático basado en la interpretación abstracta y las técnicas de model checking.