Métodos y Fundamentos para el Análisis de Corrección y Desempeño de Programas Concurrentes y Aleatorios

Se pretende estudiar y desarrollar técnicas y herramientas para analizar la corrección y desempeño (performance) de sistemas concurrentes con características aleatorias. Los factores aleatorios pueden presentarse o bien como parte del algoritmo o como comportamiento probailístico del medio (ej: perdida de mensajes, fallas externas, etc.) El tipo de propiedades a considerar son las llamadas cuantitativas que permiten expresar requerimientos probabilísticos (ej: "todo mesaje enviado se recibe en el futuro con un 99% de probabilidad"). Dentro del marco de este proyecto, definiremos y estudiaremos fundamentos que nos permitan evolucionar hacia esas técnicas y herramientas. A la vez intentaremos ir desarrollando y poniendo en práctica tales fundamentos mediante las implementaciones que fueran necesarias. Se trabajará bajo dos enfoques técnicos distintos: verificación automática mediante model checking y verificación asistida mediante asistentes de demostraciones o demostradores de teoremas.

Este proyecto fue financiado por el CONICET. Comenzó en el año 2006 y se extendió por 2 años.

Participantes