Herramientas desarrolladas

Uno de los objetivos principales del Programa es el desarrollo y prefeccionamiento de herramientas que permitan cristalizar los avances del proyecto, desarrolando casos de estudios de alto impacto social y aprovechando la amplia red de colaboraciones industrialesdel Programa para maximizar la transferencia de tecnología.

La oferta de estas herramientas que el Programa pone a disposición de la comunidad científica, se plasma en el catálogo de las mismas:

• Action-GUI: Es una metodología de desarrollo basada en modelos para aplicaciones web que garantiza la gestión segura de información. La herramienta incluye herramientas como editores para modelar los datos, la seguridad, y las interfaces gráficas, que son capaces de generar automáticamente aplicaciones web. El desarrollo y la comercialización de ActionGUI se lleva a cabo conjuntamente por el Instituto IMDEA Software y ETH Zurich, en los términos establecidos en un acuerdo firmado en diciembre de 2012.
• Ciao:Ciao es un sistema de programación multiparadigma con un entorno de desarrollo que incluye un sofisticado sistema (CiaoPP) para la optimización, y el análisis y verificación de un abanico muy amplio de propiedades funcionales y no funcionales. Se ha mejorado y optimizado la comprobación de aserciones en tiempo de ejecución, mediante simplificación parcial de aserciones con información de análisis estático, el diseño e implementación de la técnica de shallow runtime checking y el algoritmo de comprobación basado en el almacenado en caché de propiedades. Respecto al componente CiaoPP, se ha mejorado la precisión y funcionalidad de Ciao con resolutores de ecuaciones en recurrencia avanzados, mejoras de la precisión de los análisis de tamaño de datos y el analisis de programas a nivel ISA y código intermedio (LLVM IR). También se ha progresado en la escalabilidad de los análisis mediante algoritmos de punto fijo modular e incrementales. El sistema Ciao se ha utilizado en la implementación de las siguientes herramientas en el marco de este proyecto: s(CASP), RAHFT, LHornSolver, DeepFind y SPECTECTOR, Rfuzzy y FleSe. FleSe es una herramienta creada para poder hacer búsquedas flexibles (combinando criterios difusos, relaciones de similaridad y conceptos nítidos) sobre bases de datos convencionales (nítidas). Se ha mejorado la herramienta para poder aceptar diferentes formatos para la entrada de datos como son Json, MySQL, CSV, Prolog, xls y xlsx. Estas mejoras han sido publicadas en [7]. El artículo fue galardonado con el premio a mejor paper de la conferencia y aparecerá próximamente publicado por Springer Nature en su serie de Lecture Notes in Electrical Engineering (LNEE).
• DES: DES es un sistema de bases de datos deductivas interactivo, multiplataforma y portable. Hemos extendido DES con un comprobador semántico para detectar sentencias SQL que, aún siendo sintácticamente correctas, pueden mostrar síntomas de un mal diseño, y desarrollado una versión del lenguaje Fuzzy Datalog en el que los programas y consultas se compilan al lenguaje nuclear Datalog de DES. Hemos adaptado la unificación y la resolución SLD débiles a este marco y lo hemos extendido para permitir reglas con anotaciones de grados de aproximación. También hemos añadido lenguajes del cálculo relacional a DES y hemos implementado una transformación fuente a fuente de programas Datalog basada en análisis estático para la optimización de consultas.
• EasyCrypt: Es una plataforma para analizar la seguridad de construcciones criptográficas, basada en utilizar análisis de lenguajes de programación para manejar la complejidad y rigor del análisis de construcciones criptográficas. EasyCrypt ha ayudado a identificar errores en análisis previos de estándares muy difundidos, como PKCS.
• Leap: Es un sistema moderno de verificación de sistemas parametrizados concurrentes que manipulan tipos de datos complejos en memoria dinámica. Leap está basado en la separación entre el razonamiento sobre trazas de ejecución y sobre los datos compartidos, para lo cual se usan procedimientos de decisión específicos para estos datos.
• Maude: Al principio del proyecto extendimos Maude con soporte para: (i) unificación de géneros ordenados módulo asociatividad, conmutatividad e identidad, (ii) generación de variantes, (iii) unificación de géneros ordenados módulo una teoría variante finita, y (iv) alcanzabilidad simbólica módulo una teoría variante finita. Recientemente hemos incorporado en Maude 2.7.1 la capacidad de realizar unificación asociativa, que es infinitaria, esto es, existen problemas de unificación con un conjunto minimal de unificadores infinito. El algoritmo garantiza la terminación con un conjunto finito para una clase muy amplia de problemas de unificación; para los restantes, devuelve un conjunto finito junto con un aviso de que tal conjunto podría no ser completo. Otras funciones de razonamiento simbólico tales como (i) generación de variantes; (ii) unificación de variantes; y (iii) análisis de alcanzabilidad basado en estrechamiento han sido extendidas para tener en cuenta la asociatividad.
• Smack: Un obstáculo importante para la transferencia de la investigación en fiabilidad de software es lo costoso de desarrollar una infraestructura que soporte software industrial en toda su complejidad. SMACK persigue reducir drásticamente estos costes a través de la conexión entre el lenguaje intermedio de compilación de LLVM y lenguajes intermedios de verificación como Boogie y Why3, lo que permite reusar esfuerzos para muchos lenguajes fuente diferentes como C/C++, Haskell o Erlang.
• JsonGen: JsonGen es una herramienta que facilita la realización de pruebas complejas del comprtamiento de servicios web que se comunican por medio del formato de datos JSON. Partiendo de una definición de los datos manejados por el servicio expresada en el lenguaje JSON Schema, JsonGen es capaz de generar datos de manera pseudoaleatoria con los que probar las diferentes transacciones del servicio. Además, proporciona un patrón de máquina de estados que facilita crear pruebas de secuencias de acciones complejas. Ambas funcionalidades se llevan a cabo mediante la infraestructura de testing basado en propiedades de Erlang QuickCheck. Desde la publicación de JsonGen en 2014 hemos trabajado en perfeccionar y extender la herramienta. Por un lado, se ha aumentado el conjunto de construcciones de JSON Schema soportado para la generación automática de datos. También, se manejan ahora cabeceras HTTP y se hace un mejor tratamiento de los códigos de error usados habitualmente en los servicios web. Finalmente, se ha mejorado mucho la capacidad de realizar pruebas de escenarios complejos.
• Averist Averist es una herramienta para el análisis de estabilidad de sistemas híbridos. Averist implementa algortimos para el desarrollo de un método para sintetizar controladores que estabilizan una familia de sistemas lineales. Implementa un algoritmo que, dado un conjunto de sistemas dinámicos y un conjunto de superficies poliédricas, define una estrategia que asigna a cada superficie un sistema lineal con el fin de obtener un sistema de conmutación que sea estable. El algoritmo construye un grafo de juego finito, donde los nodos existenciales corresponden con los superficies, y los nodos universales representan los sistemas dinámicos. La estrategia que proveé el sistema de conmutación estable se obtiene reduciendo el juego a un juego de energía, que es un problema conocido y resuelto.
• Umerl: Es una aplicación para ejecutar y verificar sistemas especificados en UML. Las especificaciones son, esencialmente, redes de máquinas de estado que se comunican asíncronamente. El objetivo de Umerl es anticipar errores en las especificaciones y el diseño de sistemas críticos antes de su implementación. Para ello Umerl introduce una semántica precisa, no ambigua, y al mismo tiempo amigable con la filosofía UML. La aplicación consiste en un intérprete implementado en Erlang capaz de ejecutar un sistema descrito en UML mediante diagramas de estados, diagramas de clase y diagramas de objeto. Dicha ejecución es validada mediante testing dirigido por propiedades y también verificada utilizando McErlang.