| Support | |
 |
 |
Especificación y verificación
Verificación de programas y sistemas.
Nuestro referente ha sido la definición de lenguajes de aserciones para describir el consumo esperado de recursos, así como el diseño e implementación de herramientas automáticas para comprobar si los resultados del análisis garantizan dicho consumo.En este período hemos consolidado y extendido trabajo anterior de generación de casos de prueba permitiendo su aplicabilidad a programas de código de bytes de Java reales. En primer lugar propusimos una extensión para tratar con programas orientados a objetos, abordando la generación de estructuras de datos alojadas dinámicamente, las excepciones, la compartición de memoria, la herencia y el polimorfismo. Este enfoque fue posteriormente mejorado mediante un modelo composicional de ejecución simbólica que permite ejecutar simbólicamente de forma independiente diferentes partes del programa y componer los resultados, lo que permite tratar con código nativo y favorece la escalabilidad del enfoque.
Este esquema ha sido implementado en el sistema PET. También hemos desarrollado un esquema para la realización de pruebas automáticas de diferentes versiones de programas concurrentes en sistemas empotrados que permite obtener certificados que indican potenciales errores en versiones nuevas del programa.
Asimismo, hemos realizado contribuciones en el campo de la especificación con lógica temporal, en dos direcciones. La primera de ellas se refiere una nueva lógica, RLTL, que extiende LTL con construcciones para el pasado y que además puede expresar todos los lenguajes omega-regulares, con complejidad óptima. A través de la segunda presentamos un procedimiento de decisión que permite comprobar automáticamente las condiciones de verificación generadas durante la verificación formal de propiedades temporales de libreríaas concurrentes que mantienen una lista dinámica en la memoria global (o "heap").
En el campo de la verificación de programas multitarea hemos diseñado y probado experimentalmente un algoritmo de refinamiento basado en contraejemplos que mejora sustancialmente el tiempo de ejecución y gasto de memoria de los existentes hasta ahora. Además, hemos estudiado la composicionalidad de especificaciones independientes de hilos de ejecución, la complejidad teórica de la verificación de programas multitarea cuyas interacciones están definidas mediate patrones de expresiones regulares sobre las interacciones entre los hilos de ejecución, el problema de la verificacion de programas mutitarea asíncronos y hemos diseñado un nuevo algoritmo para comprobar una propiedad básica (la vacuidad) de autómatas alternantes. Contamos además con dos contribuciones más teóricas: una demostración sumamente simplificada de un teorema que relaciona lenguajes independientes del contexto y lenguajes dependientes del contexto y una construcción de subaproximaciones acotadas de lenguajes dependientes del contexto aplicable a la verificación de programas concurrentes.
En el contexto de la especificación y verificación heterogéneas, hemos mostrado cómo integrar el lenguaje Maude en el lenguaje HETS de manera que las herramientas de demostración automática ya disponibles en el segundo pueden utilizarse para analizar especificaciones de Maude. Este trabajo forma parte de la tesis doctoral de Adrián Riesco (junio de 2011) en la que, además, se ha construido un depurador declarativo para Maude.
También ha defendido su tesis doctoral Ángel Herranz, en la que se ha aislado un núcleo del lenguaje SLAM-SL suficientemente sencillo como para permitir un análisis formal de su semántica y las transformaciones que soportan la metodología asociada, al que se ha denominado Clay.
Interpretación abstracta.
Hemos aplicado técnicas de interpretación abstracta para estudiar el consumo de recursos y la terminación de programas, y trabajado en mejorar la escalabilidad, modularidad, incrementalidad y eficiencia en tiempo y memoria de los métodos de interpretación abstracta. Además, pretendemos continuar desarrollando, implementando y evaluando el marco de código con abstracciones.Hemos avanzado en la aplicación de técnicas de interpretación abstracta en casos realistas, para una larga clase de programas. En un plano más teórico, hemos estudiado una propuesta que busca un equilibrio entre dos tipos de implementaciones de analizadores abstractos y, en el campo de la implementación, una estructura de datos que permite codificar de forma económica disyunciones lógicas que pueden aparecer durante la ejecución del análisis.
Monitorización y comprobación de modelos.
En este paquete de trabajo hemos continuado el desarrollo de McErlang, una herramienta de comprobación de modelos (model checking) para programas escritos en el lenguaje de programación Erlang. La principal ventaja de utilizar McErlang en comparación con otros comprobadores de modelos como, por ejemplo, Spin, es que permite comprobar programas muy expresivos, que pueden hacer uso de todas las características de Erlang: funciones de orden superior, generación dinámica de procesos, estructuras de datos ilimitadas, primitivas para programar tolerancia a fallos, y patrones de diseño proporcionados por las libreríaas de Erlang/OTP. Dar soporte a este formalismo de especificación y programación con las características arriba mencionadas reduce el esfuerzo para desarrollar modelos verificables.Hemos evaluado McErlang en colaboración con la empresa española de desarrollo LambdaStream. Por otra parte, y como un primer paso en nuestro objetivo de integrar la comprobación de modelos con monitorización y simulación, permitiendo así la comprobación de modelos sobre sistemas con espacios de búsqueda demasiado grandes para las técnicas tradicionales, hemos realizado una comparación exhaustiva con la herramienta de comprobación de modelos ETOMCRL.
Semánticas de procesos y no-determinismo.
Hemos continuado investigando, en un marco unificador, las propiedades de comportamiento de los procesos concurrentes y el poder discriminatorio de diferentes semánticas para ellos, al tiempo que estudiamos una jerarquía de semánticas para programas no-deterministas basados en reescritura de términos, y su composicionalidad y abstracción plena, objeto de la tesis de Juan Rodríguez (junio 2010).En el trabajo de fin de máster de David Romera se ha completado la labor de unificación de las semánticas del espectro del tiempo lineal y tiempo ramificado, iniciada anteriormente en el grupo, extendiéndola al campo de las semánticas lógicas. También hemos continuado con el estudio de las simulaciones covariantes-contravariantes y "conformance": hemos construido sus caracterizaciones lógicas así como las caracterizaciones axiomáticas tanto de los preórdenes de la simulación como de sus equivalencias inducidas, resultados que hemos utilizado para demostrar que la equivalencia inducida por el preorden covariante-contravariante no es finitamente axiomatizable en presencia de acciones bivariantes.
Hay que destacar la colaboración establecida a través del programa de movilidad NILS con la Universidad de Reikiavik, traducida en tres artículos. En ellos se estudia, por un lado, la relación entre la noción de simulación covariante-contravariante con los sistemas modales y la bisimulación parcial; de otro, la axiomatización de semánticas débiles para las nociones de simulación, simulación completa y simulación "ready".
