EICAR, Electrónica, Informática, Comunicaciones, Automática y Robótica para la producción de bienes y servicios (Programa de ModernizaciónTecnológica III I-P - PAE 2006)

El presente proyecto denominado “EICAR, Electrónica, Informática, Comunicaciones, Automática y Robótica para la Producción de Bienes y Servicios” asocia estratégicamente a un importante grupo de instituciones del sector científico-tecnológico, privado y gobierno con el objetivo de formar recursos humanos altamente capacitados, desarrollar conocimiento y tecnología de punta, en el campo convergente de la electrónica, informática y computación industrial, comunicaciones y automática, y su transferencia para el desarrollo activo de sectores estratégicos del país, a través de la ejecución de seis Programas: 1) Desarrollo de sistemas inteligentes para eficientizar el uso racional de la energía; 2) I+D para el desarrollo de sistemas complejos de aeronáutica y aeroespacio; 3) Desarrollos para la plataforma de TV Digital y su integración a Internet; 4) Trazabilidad de productos agropecuarios y agroindustriales; 5) Elaboración de un plan estratégico para el desarrollo de infraestructura en TICs del Corredor Bioceánico del Centro basado en sistemas GPS y Proyecto Galileo; 6) Monitoreo de las tendencias tecnológicas de los Programas propuestos.

Métodos para el análisis de programas probabilistas y no-deterministas utilizando probadores de teoremas. Methods for the analysis of probabilistic and nondeterministic programs using theorem provers.

La verificación y el análisis de programas con características probabilistas es una tarea necesaria del quehacer científico y tecnológico actual. El éxito y su posterior masificación de las implementaciones de protocolos de comunicación a nivel hardware y soluciones probabilistas a problemas distribuidos hacen más que interesante el uso de agentes estocásticos como elementos de programación. En muchos de estos casos el uso de agentes aleatorios produce soluciones mejores y más eficientes; en otros proveen soluciones donde es imposible encontrarlas por métodos tradicionales. Estos algoritmos se encuentran generalmente embebidos en múltiples mecanismos de hardware, por lo que un error en los mismos puede llegar a producir una multiplicación no deseada de sus efectos nocivos.Actualmente el mayor esfuerzo en el análisis de programas probabilísticos se lleva a cabo en el estudio y desarrollo de herramientas denominadas chequeadores de modelos probabilísticos. Las mismas, dado un modelo finito del sistema estocástico, obtienen de forma automática varias medidas de performance del mismo. Aunque esto puede ser bastante útil a la hora de verificar programas, para sistemas de uso general se hace necesario poder chequear especificaciones más completas que hacen a la corrección del algoritmo. Incluso sería interesante poder obtener automáticamente las propiedades del sistema, en forma de invariantes y contraejemplos.En este proyecto se pretende abordar el problema de análisis estático de programas probabilísticos mediante el uso de herramientas deductivas como probadores de teoremas y SMT solvers. Las mismas han mostrado su madurez y eficacia en atacar problemas de la programación tradicional. Con el fin de no perder automaticidad en los métodos, trabajaremos dentro del marco de "Interpretación Abstracta" el cual nos brinda un delineamiento para nuestro desarrollo teórico. Al mismo tiempo pondremos en práctica estos fundamentos mediante implementaciones concretas que utilicen aquellas herramientas.