IMDEA Software

Iniciativa IMDEA

Inicio > Investigación > Líneas de investigación

Líneas de investigación

Dimensiones de la Investigación

Estas son algunas de las líneas de investigación actual o planificada en el Instituto Instituto IMDEA Software. No se pretende que la lista sea una enumeración exhaustiva de la visión y agenda del Instituto, sino más bien una presentación de algunos los esfuerzos actualmente en marcha. El orden de las líneas de investigación no es significativo.


Ver también la lista de temas e investigadores.


Modelado

Lenguajes de modelado con restricciones

Tradicionalmente, el modelado ha sido un sinónimo de producción de diagramas. La mayoría de modelos constan de una serie de gráficos con "burbujas y flechas" y algún texto explicativo. La información expresada por tales modelos tiende a ser incompleta, informal, imprecisa, y a veces, incluso inconsistente. Muchos de los errores en el modelado se deben a las limitaciones de los diagramas que se utilizan. Simplemente, un diagrama no puede expresar algún tipo de información esencial o una especificación rigurosa. Para especificar sistemas de software, la utilización de lenguajes formales en lugar de diagramas, presenta algunas ventajas claras. Los lenguajes formales no son ambígüos, y no pueden interpretarse de manera diferente por diferentes personas, por ejemplo, un analista y un programador. Los lenguajes formales construyen un modelo más preciso y detallado, y son apropiados para ser manipulados por herramientas automáticas con la finalidad de garantizar la correción y coherencia con otros elementos del modelo. Por otro lado, un modelo completamente escrito en un lenguaje formal a menudo no es fácil de entender.

El Lenguaje Unificado de Modelado (UML) utiliza una notación basada principalmente en diagramas. Sin embargo, para proporcionar los niveles de concisión y expresividad requeridos por algunos aspectos de un diseño, el estándar del UML define el Lenguaje de Restricciones de Objetos, OCL (siglas del inglés "Object Constraint Language"). OCL es un lenguaje textual con un estilo notacional similar al de los comunes lenguajes de programación orientados a objetos. En UML 1.1, OCL apareció como el estándar para especificar invariantes y pre/post condiciones. En UML 2.0, la idea es que no sólo se incluya la información de restricciones, sino que se deban incluir anotaciones más ricas en un modelo. OCL también se utiliza actualmente para definir consultas, referenciar valores, o establecer condiciones y reglas de negocio en un modelo. Aunque OCL fue inicialmente diseñado para ser un lenguaje formal, su definición no es lo suficientemente precisa, presenta ambigüedades e incoherencias, y existen expresiones con interpretaciones abiertas y circulares.

En los últimos años, el modelado ha evolucionado de tal manera que puede tratar aspectos como la definición de metamodelos específicos, transformación de modelos, comprobación de diseños de modelos, y validación de modelos y simulación. La mayoría de estas nuevas aplicaciones hacen un amplio uso de OCL y con frecuencia requieren extensiones no triviales de este lenguaje. En esta situación, una completa y no ambígüa especificación de OCL sería muy beneficiosa, como base de herramientas automáticas para sus muy variados usos.

Hemos propuesto una semántica para un subconjunto sifnificativo de OCL, basada en una novedosa asignación de teorías ecuacionales a modelos UML con expresiones OCL. Esta asignación se describe como una (meta)función que, dada una expresión OCL y un diagrama UML, genera un intérprete ecuacional para la expresión.

Por lo tanto, dicha función define una semántica para OCL que es formal a la vez que ejecutable. En esta línea de investigación tenemos previsto extender la mencionada semántica formal de OCL desde diagramas UML de clases y objetos, a diagramas de secuencias y estados. Esta extensión permite razonar sobre la realizabilidad de modelos UML. Los modelos constan típicamente de varios diagramas, cada uno con su propio conjunto de restricciones OCL, que modelizan diferentes puntos de vista de un sistema. En este contexto, la realizabilidad significa que existe al menos una instancia válida del modelo, lo que implica que el modelo es, en principio, implementable.

Pretendemos utilizar herramientas existentes para demostrar la terminación de operaciones OCL definidas por el usuario, a partir de la terminación de los intérpretes ecuacionales generados. Finalmente, implementaremos un intérprete de OCL basado en nuestra semántica formal. Nuestra herramienta proporcionará una solución rigurosa a la actual carencia de herramientas de soporte a la evaluación de OCL en enormes escenarios con posiblemente miles de elementos. Desarrollaremos dicha herramienta en colaboración con nuestros socios industriales. En este sentido, SAP AG ha mostrado interés inicialmente en esta investigación en el contexto de su infraestructura de modelado MOINE, una tecnología SAP que proporciona un repositorio de metamodelos basado en MOF así como integración OCL.

Seguridad basada en el modelado

El desarrollo basado en modelos (Model Driven Development) es prometedor como instrumento para reducir el tiempo de desarrollo y mejorar la calidad del resultado. Investigaciones recientes ilustran como las políticas de seguridad pueden integrarse en modelos de diseño del sistema, y que los modelos de diseño de seguridad resultantes pueden usarse como base para generar sistemas conjuntamente a su infraestructura de seguridad. Es más, cuando los modelos tienen una semántica formal, se pueden transformar y razonar sobre ellos. Por ejemplo, se puede responder a propiedades de los diseños y entender las consecuencias de todos los casos de las políticas que define. El lenguaje SecureUML es un lenguaje de modelado cercano al control de acceso basado en roles (Role Based Access Control). SecureUML puede combinarse con diferentes lenguajes de diseño, creando así lenguajes para formalizar modelos de diseño de seguridad que especifican diseños junto a los requisitos de seguridad, permitiendo la generación de la infraestructura de control de acceso desde estos modelos.

Los modelos de diseño de seguridad son objetos formales con una sintaxis concreta y una representación abstracta. El lenguaje de modelado para diseños de seguridad se puede describir con un metamodelo que formaliza la estructura de aquellos modelos y escenarios bien formados, que representan las posibles ejecuciones como estados concretos del sistema. En este contexto, las propiedades de seguridad pueden expresarse como fórmulas en OCL.

Este uso de OCL resulta en un lenguaje expresivo para la formalización de propiedades, utilizando todo el vocabulario presente en el metamodelo. Las propiedades expresables incluyen la relación entre los usuarios, sus roles, los permisos, acciones e incluso los estados del sistema. Por ejemplo, se puede expresar ``¿Hay dos roles de tal manera que uno incluye el conjunto de acciones del otro pero los roles no están en la misma jerarquía?'' Otro ejemplo, que incluye estados del sistema, es ``¿Qué roles se pueden asignar a un usuario de tal manera que le permitan realizar una acción en un recurso concreto en el contexto de un escenario dado?'' Estas propiedades pueden comprobarse evaluando las expresiones OCL correspondientes en las instancias del metamodelo que representan los modelos de diseño de seguridad o los escenarios considerados.

El uso de escenarios ofrece el soporte necesario para gestionar propiedades que involucren el estado del sistema. Extenderemos esta línea con soporte adicional para describir la existencia de estados que satisfagan una restricción o propiedades donde los estados mismos están cuantificados existencialmente. Por ejemplo, podemos considerar el diseño de un metamodelo que incluya acceso a la fechas del sistema, con peticiones como ``¿Qué operaciones son posibles en los días laborables pero imposibles en los fines de semana?'' Otro ejemplo, en un sistema bancario, un podría preguntar ''¿Qué acciones son posibles en cuentas bancarias en números rojos?'' Estas consultas no se pueden evaluar a menos que se pueda razonar acerca de las consecuencias de formulas OCL. Esto involucra el uso de demostradores de teoremas. Por el contrario, para la evaluación de fórmulas en modelos concretos uno sólo necesita determinar la satisfacibilidad de estas fórmulas.

En esta línea de investigación también estudiaremos el análisis de coherencia entre diferentes vistas del sistema. Se puede combinar SecureUML junto a lenguajes de modelado como ComponentUML y ControllerUML para tratar diferentes vistas de arquitectura multi-tier. En este contexto, el control de acceso debe ser implementado al nivel intermedio, por ejemplo para implementar un controlador para una aplicación de web, junto a un nivel persistente. Si las políticas para estos niveles están modeladas formalmente, podríamos responder a preguntas como ``¿Es posible que el controlador llegue a un estado en el que el nivel persistente lance una excepción de seguridad?'' Esta consulta requiere ser capaz de analizar la alcanzabilidad de estados, para lo que - nuevamente - es necesario el uso de demostradores de teoremas u otras formas de razonamiento deductivo tales como resolución de restricciones o búsqueda en espacio de estados.

Este trabajo se realizará en colaboración con el profesor David Basin y su grupo en ETH Zurich.

Seguridad de Software y Sistemas

Seguridad basada en lenguajes

Aunque la seguridad de software se ha enfocado tradicionalmente hacia mecanismos de protección de bajo nivel, como el control de acceso, la popularidad de los sistemas distribuidos ha incrementado en gran medida las vulnerabilidades de seguridad a nivel de aplicación. Estas vulnerabilidades son aprovechadas por programas maliciosos como los virus, los caballos de Troya, etc. Peor aún, en ocasiones, algunos programas bienintencionados, pero con errores, las exponen involuntariamente dando lugar a efectos desastrosos.

La área de seguridad basada en lenguajes (language-based security) trata de conseguir los objetivos de seguridad a nivel de lenguaje de programación, lo cual reporta el beneficio inmediato de neutralizar los ataques a nivel de aplicación. La seguridad a nivel de aplicación es atractiva para los programadores porque permite expresar políticas de seguridad y garantizar estas políticas en el propio lenguaje de programación, empleando técnicas que facilitan la especificación rigurosa y la verificación de las propias políticas.

Las técnicas basadas en lenguajes permiten garantizar un amplio conjunto de políticas de seguridad, incluyendo la confidencialidad, la integridad, la disponibilidad y combinaciones de ellas. Por el contrario, su empleo en la práctica no está muy extendido, en parte porque los mecanismos conocidos están restringidos a políticas muy simples como la no interferencia para garantizar confidencialidad. Dos retos importantes son la mejora de los mecanismos que garanticen políticas flexibles y adaptables, y métodos para extraer un análisis cuantitativo del nivel de seguridad. Hay muchos aspectos relativos a la evaluación cuantitativa de la seguridad de los programas, pero la criptografía demostrable matemáticamente es una fuente de inspiración. Es más, la seguridad basada en lenguajes debe considerar aspectos de bajo nivel del sistema.

Las técnicas basadas en lenguajes sacrifican con frecuencia generalidad y precisión en favor de la efectividad. Hay técnicas complementarias, basadas en la lógica, que heredan la precisión y generalidad de ésta. El código con demostración (proof carrying code) es un marco general para la seguridad del código móvil que emplea lógicas para garantizar que los programas se ajustan a criterios de seguridad. Los experimentos iniciales del código con demostración se llevaron a cabo para propiedades de seguridad, pero el alcance del método sólo se ha explorado preliminarmente. Existe el potencial de adaptar estas ideas a otras propiedades de interés, como políticas de gestión de recursos y flujo de información.

Un tema central en las técnicas basadas en lenguajes es que las técnicas de verificación usadas por el desarrollador para verificar la corrección del código pueden ser reproducidas por los usuarios del código. Estos usuarios no tienen por qué confiar en el código ni, en principio, en la demostración, y sólo permitirá la ejecución del código bajo garantías de que es inocuo. En este aspecto, nos centraremos en técnicas de verificación que se utilicen a nivel de usuario, y estudiaremos cómo usar certificados para transferir las evidencias desde el desarrollador al usuario.

Los métodos basados en lenguajes se han estudiado primeramente para código móvil y pocos métodos consiguen escalar a sistemas distribuidos. De hecho, hay realmente muy pocos mecanismos para garantizar criterios de seguridad en aplicaciones distribuidas, y usan una combinación de criptografía y métodos basados en lenguajes. En el Instituto IMDEA Software estudiaremos métodos para garantizar la seguridad de algoritmos de computación intensiva que ejecuten distribuidamente. Estos algoritmos realizan computaciones que no pueden ser ejecutadas de manera realista en un único procesador, al precio de generar resultados que deben ser validados independientemente. Para garantizar la seguridad, se confía en los certificados de resultado, que proveen la evidencia de que el resultado es correcto. Típicamente, estos resultados consisten en una combinación de datos -- testigos adicionales que se generan durante la computación y se usan para construir el resultado final -- y demostraciones -- que establecen alguna propiedad acerca de estos testigos o del resultado final. Llevado al extremo, el certificado es una traza de la computación y una demostración de que cada paso es correcto, pero muchos algoritmos permiten certificados más concisos. Por ejemplo, se han propuesto certificados concisos en criptografía para garantizar la primalidad de números grandes.

Criptografía

En esta línea de investigación utilizaremos lenguajes de programación convencionales para analizar algoritmos y sistemas criptográficos muy utilizados y garantizar su corrección respecto a la potencia criptográfica (cryptographic strength). Nuestro objetivo es demostrar, más allá de la duda razonable la seguridad de los sistemas criptográficos convencionales, algunos de los cuales tienen una larga historia de demostraciones incorrectas y errores ocultos que han dado lugar a ataques. Seguiremos la metodología de la seguridad demostrable, que sugiere una aproximación rigurosa basada en la teoría de la complejidad. En este caso, los objetivos se especifican de manera precisa, y la demostración de seguridad se realiza de manera formal, consiguiéndose que todas las suposiciones sean explícitas.

Una técnica muy útil para la demostración de corrección de esquemas criptográficos es el uso de la teoría de juegos, en la que la demostración criptográfica se construye como una secuencia de juegos probabilísticos. Ésta es una solución natural para lidiar con la complejidad de las demostraciones criptográficas. Las técnicas basadas en la teoría de juegos tienen una aplicación general, permiten el razonamiento tanto en el modelo estándar como en el modelo de oráculo aleatorio, y se han estudiado extensivamente para la demostración de propiedades criptográficas en multitud de esquemas y protocolos. Las técnicas basadas en código son un caso particular de las técnicas basadas en la teoría de juegos, y se han aplicado con éxito a algunos esquemas criptográficos modernos. Su característica más importante consiste en utilizar una visión centrada en el código tanto de los juegos como de las hipótesis de seguridad y suposiciones computacionales, que pueden expresarse mediante programas escritos en lenguajes imperativos con construcciones probabilísticas que ejecutan en tiempo polinomial. En esta visión, la transformación de juegos es simplemente transformación de programas, y se puede tratar rigurosamente utilizando argumentos semánticos. Por ejemplo, muchas transformaciones se pueden tratar como optimizaciones clásicas de programas (propagación de constantes, eliminación de subexpresiones comunes, etc.), y su justificación se basa en la demostración de que el programa original y el transformado son equivalentes. Aunque las demostraciones basadas en código son más fáciles de verificar y comprobar mecánicamente, necesitan teorías de equivalencia entre programas mucho más sofisticadas que las actuales, y necesitan un conjunto muy rico de principios de razonamiento adaptados de los campos de verificación formal, razonamiento algebráico, teoría de la probabilidad y teoría de la complejidad. En consecuencia, a pesar de los beneficios de la utilización de las técnicas basadas en código, las demostraciones son inherentemente muy difíciles de construir y verificar.

En esta línea de investigación desarrollaremos una plataforma para construir demostraciones basadas en código utilizando el asistente de demostraciones matemáticas Coq. Nuestro objetivo es utilizar esta plataforma para la demostración de corrección de construcciones criptográficas estándar como OAEP padding y triple DES. Este trabajo se realiza en colaboración con Benjamin Grégoire de INRIA Sophia-Antipolis.

Verificación y Validación

Depuración y verificación del uso de recursos

Tradicionalmente se ha entendido la corrección como la ausencia de errores, es decir, que todas las ejecuciones de los programas cumplen una especificación funcional (como la correción de tipos) o una especificación de comportamiento (como la terminación o posibles secuencias de acciones). Sin embargo, en una cantidad cada vez mayor de aplicaciones, el entorno juega un papel esencial. Por ejemplo, los sistemas empotrados deben controlar y reaccionar al entorno, el cual a su vez establece restricciones sobre el comportamiento del sistema respecto al consumo de recursos y tiempos de respuesta. Por tanto, para dichos sistemas, se hace necesario extender el criterio de corrección teniendo en cuenta nuevos aspectos que incluyen propiedades globales no funcionales tales como tiempo máximo de ejecución, uso de memoria, consumo de energía, u otros tipos de recursos.

Uno de los retos de esta línea de investigación es la extensión de las técnicas de depuración y verificación basadas en abstracciones para que puedan tratar con propiedades relacionadas con el uso de recursos no contempladas actualmente. Por ejemplo, para inferir de manera correcta el uso de recursos de una computación puede ser necesario determinar otro tipo de información más básica (tales como tamaños de datos, métricas apropiadas para calcularlos, patrones de llamada a los procedimientos, etc.). Por tanto, se necesitan nuevos marcos de análisis que puedan combinar en un único dominio abstracto de análisis diferentes dominios para dichas propiedades más básicas. En este desafío, se incluye además el estudio de nuevos dominios abstractos para determinadas propiedades no funcionales, o la mejora de los dominios existentes, para conseguir con ello aproximaciones semánticas más precisas.

Otro aspecto novedoso en la verificación de recursos consiste en que la comprobación estática de aserciones debe generar respuestas que van más allá de las clásicas (cierto/falso/desconocido). En efecto, para que las respuestas sean útiles deben incluir condiciones bajo las cuales se cumplen estas respuestas "clásicas". Dichas condiciones se pueden parametrizar respecto a ciertos atributos de los datos de entrada, tales como el tamaño de los mismos e intervalos para sus valores. Por ejemplo, sería posible afirmar que una aserción es cierta si los tamaños de los datos de entrada se encuentran en intervalos determinados.

Finalmente, otro desafío consiste en el desarrollo de un marco de depuración/verificación que realice la selección apropiada de información de análisis necesaria para comprobar una especificación determinada referente al uso de recursos, dependiendo del tipo de información expresada en dicha especificación. Esta información puede incluir por ejemplo cotas inferiores y superiores, incluso valores asintóticos del uso de recursos de una computación. La investigación en ésta línea también tendrá en cuenta el carácter necesariamente interactivo de la depuración de recursos y sus posibilidades de automatización (prestando especial atención a la diagnósis), lo que a su vez incluye el estudio de extensiones de técnicas de visualización existentes más allá de la detección de errores.

Verificación en tiempo de ejecución

La verificación en tiempo de ejecución es un área de investigación de métodos formales que intenta proveer una base más rigurosa para la prueba de sistemas software y la depuración. Al igual que en verificación estática, se parte de una especificación formal, escrita por ejemplo en lógica temporal. En cambio, mientras que en la verificación estática se trata de demostrar que todas las posibles trazas de ejecución del sistema cumplen la especificación (sin tener que ejecutar el sistema), en la verificación en tiempo de ejecución sólo se comprueba la traza generada por el sistema. De esta manera, la verificación en tiempo de ejecución sacrifica completitud por eficiencia. La verificación en tiempo de ejecución contribuye a la mejor elaboración y ejecución de comprobaciones ya que pueden especificarse propiedades más sofisticadas (incluyendo patrones temporales de comportamiento), y garantizarse que realmente se están comprobando. Dado que la prueba de sistemas es, por mucho, la actividad dominante de validación en ingeniería del software en la práctica, la verificación en tiempo de ejecución puede mejorar las garantías de la calidad en términos de cobertura, tiempo y coste. La verificación en tiempo de ejecución es un área de intensa investigación en la actualidad y la transferencia de tecnología promete ser rápida y aplicada.

Una faceta importante es el estudio de formalismos de especificación. Los primeros estudios de verificación en tiempo de ejecución utilizaban lógicas temporales lineales como lenguajes de especificación. Más tarde emergieron nuevos lenguajes, como especificaciones basadas en reglas, calculo de reescrituras o sistemas basados en flujos síncronos (synchronous streams), y aún hoy es un área de investigación. Un uso habitual de la verificación en tiempo de ejecución es la recolección de estadísticas de las trazas de ejecución, para lo que los tradicionales lenguajes basados en lógicas temporales no son apropiados. Otras propiedades a estudiar en los lenguajes de especificación es su poder expresivo, su concisión, la eficiencia de su evaluación y la usabilidad por parte de los ingenieros.

Un aspecto esencial es la estrategia de ejecución. Existen dos grandes clases de estrategias: monitorización en línea y fuera de línea. En la monitorización en línea se genera un monitor a partir de una especificación, que se ejecuta en paralelo con el programa dado. En la monitorización fuera de línea, la traza (o la parte relevante de ella) se almacena para su posterior análisis. La monitorización en línea ha permitido la aparición del paradigma de programación basada en monitores, en la que la violación de una propiedad temporal se refleja en el lenguaje y puede usarse para redirigir la ejecución a un código de reparación. La monitorización fuera de línea se puede usar para analizar propiedades más sofisticadas que necesiten varias pasadas a la traza, y para análisis post mórtem de programas.

Finalmente, la instrumentación es uno de los problemas más importantes a día de hoy. Las primeras implementaciones de verificadores en tiempo de ejecución consideraban el sistema como una caja negra que emite las señales relevantes para el monitor. La instrumentación consiste en hacer que el programa emita esas señales, o que ya incluya al monitor. En este aspecto, hay - potencialmente - una interacción muy beneficiosa entre la verificación estática y la realizada en tiempo de ejecución. Por un lado, cuando una propiedad no puede ser verificada estáticamente, la verificación en tiempo de ejecución permite comprobar estos casos particulares durante la ejecución. Por otro lado, el análisis estático puede mejorar drásticamente la calidad de la instrumentación permitiendo la distinción de los casos que pueden suceder y los que deben suceder.

Esta línea incluirá una fase de prototipado para lenguajes de programación realistas y sistemas industriales, así como la integración en plataformas existentes. Es especialmente interesante la aplicación de la verificación en tiempo de ejecución a los sistemas empotrados, y en particular a la monitorización del análisis de recursos.

Síntesis

La síntesis es la actividad de generar un sistema informático a partir de una especificación. El concepto teórico de síntesis es antíguo y se ha estudiado exhaustivamente para el caso de funciones computables. En la última década, la investigación se ha enfocado hacía la síntesis de sistemas reactivos, por ejemplo, controladores. Los resultados más importantes parten de lenguajes y lógicas clásicas, y utilizan la teoría de autómatas y la teoría de juegos para las soluciones algorítmicas. Hoy en día se conocen bien las aplicaciones y limitaciones de la síntesis automática a partir de especificaciones en diferentes formalismos.

Una área emergente de aplicación consiste en la síntesis parcial, en la cual se generan componentes específicos una vez conocido el resto de los subsistemas del sistema. En algunos casos, los demás componentes pueden haberse desarrollado con métodos convencionales. La corrección de la composición está garantizada, siempre y cuando los componentes se adhieran a la especificación que se usó para sintetizar el componente crítico. Esta especificación puede verificarse para cada componente por separado. Alternativamente, los subsistemas pueden analizarse extrayendo una especificación que luego se usa en el proceso de síntesis.

La síntesis parcial es especialmente útil para generar aquellos aspectos del sistema que son especialmente difíciles de obtener manualmente, y para los que no existen soluciones universales o son muy ineficientes. Algunos ejemplos son la síntesis de gestores de recursos específicos de aplicación, y los gestores de tareas para sistemas paralelos y distribuidos. Estas soluciones se basan en el análisis estático del sistema, seguido del proceso de síntesis. El análisis estático no pretende garantizar una propiedad o encontrar un error, sino extraer suficiente información para el proceso de síntesis. Aunque ya hay varios casos de aplicaciones que siguen esta idea, no existe aún una teoría general que explique la aplicabilidad y limitaciones de esta metodología.

Este uso de la síntesis puede entenderse como una aplicación práctica de la programación basada en abstracciones, tal y como se presenta más arriba.

Programación y Optimización

Programación basada en abstracciones

La técnica de la interpretación abstracta ha hecho posible el desarrollo de sofisticados análisis de programas que son demostrablemente prácticos a la vez que correctos. Los enfoques semánticos posibilitados por la interpretación abstracta se han aplicado también tradicionalmente a la optimización y transformación de programas en tiempo de compilación, además de a la verificación formal. Más recientemente, y en el contexto más general de desarrollo de programas, están emergiendo novedosas y prometedoras aplicaciones de la interpretación abstracta.

Una significativamente nueva clase de tareas de depuración, verificación y optimización se han posibilitado de una manera correcta gracias a los recientes avances en la interpretación abstracta. Ello está empezando a influenciar el diseño de entornos de desarrollo de programas que están empezando a mostrar a los programadores el potencial de los analizadores. El objetivo de tales entornos de programación basados en abstracciones es mejorar el proceso de desarrollo de software mediante la incorporación de certificación, depuración semática y optimización estáticas como parte integral de los compiladores. La capacidad de inferir propiedades no triviales sobre los programas permite que los compiladores comprueben que un determinado programa cumple con una especificación. Sin embargo, la mayoría de las propiedades de los programas que son interesantes en contextos de software intensivo o empotrado (tales como tiempo de ejecución, consumo de memoria, tamaños de datos dinámicos, terminación, ausencia de errores o excepciones) son indecidibles. Consecuentemente, las técnicas basadas en interpretación abstracta que proporcionan aproximaciones seguras son particularmente útiles en estos contextos.

En la práctica, durante el desarrollo de programas, pueden darse tres casos posibles como resultado de realizar aproximaciones seguras y utilizarlas para comprobar especificaciones de los programas. En primer lugar, si la aproximación inferida por el analizador es suficiente para demostrar que el programa se ajusta a la especificación, entonces el programa se ha certificado de manera efectiva y se ha demostrado su correción. El punto fijo calculado por el intérprete abstracto (o en su caso un subconjunto de él, si se aplica compresión de puntos fijos o reducción de certificados), es un certificado abstracto generado automáticamente, el cual puede utilizarse en escenarios de código con demostración (un enfoque también conocido como código con demostración). En segundo lugar, si la información inferida por el analizador contradice parte de la especificación entonces se ha encontrado un error semántico. Estos errores semánticos son similares a los errores de tipado, pero no sólo se refieren a tipos sino también a propiedades más complejas tales como las mencionadas anteriormente (tiempo de ejecución, consumo de memoria, tamaños de datos dinámicos, terminación, ausencia de errores o excepciones, etc.). La capacidad de detectar errores reales en tiempo de compilación se conoce como depuración abstracta. Un compilador que incorpore interpretación abstracta tiene el potencial de ayudar en la identificación de la naturaleza del error y la localización del origen del mismo (proceso conocido como diagnósis abstracta). Finalmente, si el compilador no es capaz de demostrar como cierta o falsa una parte determinada de la espeficicación, entonces puede generar automáticamente comprobaciones en tiempo de ejecución a partir de dicha parte de la especificación, e incluso generar casos de prueba para realizar una evaluación empírica.

El objetivo global de esta línea de investigación es conseguir que la interpretación abstracta se convierta en una pieza básica y fundamental de las herramientas y entornos de desarrollo de programas. Ello conlleva hacer que la certificación basada en abstracciones sea una tarea rutinaria en el desarrollo de aplicaciones, y que también lo sean la generación de comprobaciones semáticas, la depuración y diagnósis de errores basadas en interpetación abstracta. Las herramientas obtenidas como resultado del esfuerzo de investigación en esta línea integrarán otras herramientas y librerías (ya sean internas o externas), y a su vez quedarán disponibles para su uso en futuros marcos de herramientas de programación.

Optimización rigurosa, incluida la paralelización automática

El objetivo de la optimización rigurosa de programas consiste en transformar los programas para que se ejecuten lo más rápidamente posible y de la manera más eficiente en cuanto al uso de recursos, en la plataforma y condiciones de entorno en la que se encuentra desplegada la aplicación, pero manteniendo el comportamiento observable de los programas. Ello requiere desarrollar técnicas de transformación de programas y modelos de plataformas de ejecución y entornos que tengan una buena base formal.

Se persigue por tanto que los programas optimizados preserven los resultados observables, pero mejorando su rendimiento respecto a ciertas métricas, tales como el tiempo de ejecución y uso de memoria. Las diferentes técnicas varían desde métodos para ahorrar memoria y tiempo de procesamiento en procesadores secuenciales, hasta técnicas de paralelización automática y de reparto de tareas en sistemas paralelos y distibuidos. Entre otros objetivos más avanzados se incluye el reparto de tareas distribuido, la autoreconfiguración, y la adaptación automática a las condiciones del entorno.

El razonar a priori sobre los beneficios de la transformación de programas es todo un desafío, pero posible hasta cierto punto, gracias a técnicas tales como la interpretación abstracta, evaluación parcial, o combinaciones de ellas. Asímismo, las técnicas estáticas son especialmente efectivas cuando se combinan con algún tipo de soporte en tiempo de ejecución para conseguir los objetivos tales como autoadaptación, autoreconfiguración, resistencia, etc.

La paralelización automática es particularmente interesante dado que los procesadores paralelos masivos, a los que sólo se les prestó atención en la computación de alto rendimiento, poco a poco se han ido conviertiendo en la norma a seguir en computación. Actualmente, incluso los ordenadores portátiles estándar incorporan chips multinúcleo con hasta cuatro núcleos, y la tendencia es que estas cifras aumenten de manera consistente a corto plazo. Con las técnicas actuales de desarrollo de software, que típicamente mantienen sólo un hilo de ejecución ocupado no se podrá explotar todo este enorme potencial de rendimiento.

La alternativa consiste en producir programas paralelos o paralelizar los existentes. La programación paralela es una tarea tediosa y muy propensa a cometer errores, dificultando aún más la ya compleja tarea de desarrollo de software tradicional. Con las técnicas actuales, el requerir que los programadores paralelicen manualmente los programas para explotar dichas arquitecturas muitinúcleo inevitablemente conlleva un decremento importante de la productividad. En principio, una solución ideal a este problema consiste en aplicar técnicas de paralelismo automático, para que el compilador sea capaz de identificar regiones de código que son independientes y, por tanto, se ejecuten en paralelo.

El uso de lenguajes declarativos es instrumental en esta tarea, ya que son lenguajes que preservan gran parte del paralelismo intrínseco de las aplicaciones. Sin embargo, también es deseable desarrollar tecnología de paralelización automática para otros lenguajes de programación bastante extendidos actualmente. Por ello será necesario definir nuevas nociones de independencia y técnicas de análisis más avanzadas que puedan detectar el paralelismo en procesos complejos con patrones de acceso irregulares a datos ubicados dinámicamente, así como nuevas nociones de coherencia y sincronización de memorias que incorporan las nuevas arquitecturas multinúcleo.

Sin embargo será necesario paralelizar algunas partes manualmente con el fin de obtener el mejor rendimiento, ya que los compiladores paralelizantes actuales no son capaces de explotar al máximo el paralelismo con las descripciones algorítmicas convencionales. Serán esenciales por tanto los lenguajes paralelos y las extensiones de lenguaje, incluyendo patrones de diseño paralelo. Un enfoque prometedor debe combinar paralelización automática y manual. Los programadores pueden usar anotaciones para indicarle al compilador oportunidades de paralelización. Asimismo, los compiladores paralelizantes verificantes podrán corregir paralelizaciones erróneas de los programadores.

Al mismo tiempo, será necesario investigar en sistemas en tiempo de ejecución, incluyendo máquinas abstractas paralelas. Entre otras, la monitorización y soporte general para distribución de tareas o adaptación a diferentes condiciones de carga y disponibilidad de recursos serán nuevas característas. El análisis de recursos proporcionará resultados útiles con potencial aplicabilidad a la optimización de programas, y en particular a la paralelización automática.

Finalmente, el proceso de paralelización no debe limitarse a detectar independencias sino que debe tener en cuenta que en la práctica existen una serie de costes asociados con la ejecución paralela de tareas, como por ejemplo, los costes de la creación y gestión de tareas, posible migración de tareas a procesadores remotos, costes de comunicación, etc. Dichos costes pueden dar lugar a que la ejecución de los programas paralelos sea más lenta que la de los secuenciales, o al menos, limitar la ganancia debida al paralelismo introducido. Por ello es necesario estimar eficientemente el coste de las tareas (respecto a ciertos recursos como número de instrucciones o tiempo necesario para su ejecución completa) y utilizarlo para limitar el paralelismo, de forma que se controle el efecto de los costes mencionados anteriormente. En particular, es importante realizar tanto trabajo como sea posible en tiempo de compilación para reducir la carga de trabajo del control del consumo de recursos realizado en tiempo de ejecución. Todavía queda mucho trabajo por hacer en esta área para desarrollar metodologías y herramientas realmente potentes, prácticas y escalables que realicen control del consumo de recursos adaptativo automático.

Preveemos que la evolución de los compiladores paralelizantes sea similar a la de la tecnología de compilación tradicional. En los orígenes de la compilación y optimización los "programadores reales" a menudo codificaban grandes partes cruciales de los sistemas en lenguaje ensamblador por motivos de eficiencia. Actualmente, incluso los sistemas críticos se programan haitualmente utilizando lenguajes de alto nivel. De manera similar, los avances en paralelización automática deberían ir reduciendo la necesidad de paralelización manual.

Diseño de lenguajes de programación inspirado en análisis estático

Los lenguajes de programación son el instrumento principal para el desarrollo de software. Los paradigmas de programación de más alto nivel de abstracción permiten que los programadores no tengan que preocuparse por los detalles de bajo nivel, lo que facilita el desarrollo de software con funcionalidades más complejas.

Una nueva tendencia interesante es la influencia de la interpretación abstracta y otras técnicas correctas de análisis estático en el diseño de los lenguajes de programación, que van más allá de las aplicaciones estándar para depuración, verificación, y optimización. Por ejemplo, la inferencia de definiciones de tipos (formas) y muchas otras propiedades relacionadas con los datos y el control, permite que los lenguajes no tipados hereden - y en algunos casos incluso mejoren - algunas características de los lenguajes fuertemente tipados. Los diseñadores de lenguajes pueden desviar su atención de los sistemas de tipos y de comprobación de tipos hacia al ámbito más general de lenguajes de aserciones e inferencia y comprobación de aserciones.

Este enfoque implica una estrecha integración entre la programación y los lenguajes de especificación, en el espíritu del diseño por contrato. Proponemos investigar diseños de lenguajes donde se mezclen juntos y se unifiquen los lenguajes de programación y los de especificación, pudiéndose definir así muchas propiedades en el código fuente. En este caso, algunos usos de la verificación en tiempo de ejecución surgen naturalmente como la comprobación de aserciones que no se han resuelto en tiempo de compilación.

El lenguaje de aserciones debería permitir expresar especificaciones de forma precisa, así como proporcionar soporte a la interoperabilidad basada en la semántica, y permitir la descripción de las propiedades en diferentes niveles de abstracción. El lenguaje de aserciones también sirve como vehículo de comunicación entre un programador y un compilador interactivo. Además, un único lenguaje potencialmente permite que el programador documente, pruebe, modifique, mantenga y componga componentes, siendo por tanto útil durante todo el proceso de desarrollo de software.

Otro efecto del diseño de lenguajes de programación basado en la interpretación abstracta es que el desarrollador puede activar a voluntad la realización de optimizaciones exhaustivas correctas. Por ejemplo, el código genérico no incurre necesariamente en problemas de rendimiento. En lugar de ello, la información obtenida mediante análisis global puede permitir una especialización y posterior optimización que reduce el coste debido a instanciaciones genéricas.

Otra aplicación de este principio es el desarrollo de lenguajes que combinan el poder de varios paradigmas. Esto permite estudiar cómo interactúan las diferentes características de estos paradigmas. Ejemplos de ello son la mejora de las aplicaciones que requieren concurrencia o la resolución de problemas complejos, que se han resuelto de diferentes maneras con diferentes paradigmas. Como un ejemplo más concreto, la resolución de restricciones se ha mostrado particularmente útil en aplicaciones que incluyen optimización, análisis de programas, o la coordinación de servicios, y también se ha demostrado que el hecho de que los lenguaje de programación tengan una estrecha relación con la resolución de restricciones puede dar lugar a muy compactas, potentes y eficientes codificaciones de problemas complejos.

Muchos lenguajes de programación modernos no se limitan a una sintaxis y semántica fijas, sino que más bien están constituidos por núcleos altamente extensibles, de manera que tanto el diseñador del lenguaje como el programador pueden crear nuevas abstracciones. Este enfoque simplifica enormemente el desarrollo de lenguajes de aplicación específicos adaptados para una aplicación, área o dominio particulares.

En esta línea de investigación nos centraremos en el desarrollo de un marco de herramientas en el que poder experimentar con nuevas características y combinaciones de paradigmas, así como poder desarrollar tecnología de implementación. Naturalmente, este marco - que es flexible y extensible - se beneficiará del hecho de ser código abierto para constituir una comunidad de programadores que contribuyan y de usuarios.