Métodos para la Verificación de Programas Concurrentes con aspectos Aleatorios y Temporizados
La interacción cotidiana con sistemas basados en computadoras es hoy un hecho inevitable. Podemos encontrar microprocesadores en electrónica de consumo (ej. TVs, reproductoras de video o CD), medios de transporte (ej. aviones, autos, controladores de diversos tipos de tráfico), sistemas de comunicación, plantas industriales, redes de computadoras, equipo médico, etc. El funcionamiento incorrecto de cualquiera de estos sistemas tiene una diversidad de consecuencias que varían desde una molestia en el usuario hasta situaciones que pueden poner en peligro la vida humana o inclusive generar serias catástrofes. Para la mayoría de tales sistemas, es crucial que ellos provean un servicio correcto y eficiente.
Los algoritmos aleatorios, en particular, presentan, en muchas ocasiones, soluciones más veloces que los algoritmos tradicionales y en otras, soluciones que no serían posibles dentro del dominio de lo algoritmos tradicionales. De particular interés, son los algoritmos aleatorios concurrentes y/o distribuidos tales como los protocolos de elección de líder o los de acuerdo bizantino. Consideraremos también la posibilidad de que estos algoritmos deban incluir características temporales introducidas por el algoritmo mismo (como los timeouts) o por el contexto (ej. demora en transmisiones).
Model checking es una técnica de verificación del tipo push-button, en el sentido de que dado el modelo del sistema bajo estudio, y la propiedad requerida sobre este, la técnica permite decidir automáticamente si la propiedad es satisfecha por este modelo o no.
Es nuestra intención el desarrollar técnicas y herramientas basadas en model checking para analizar la corrección de programas concurrentes temporizados con características aleatorias.
En particular, proponemos atacar el problema de la explosión de estados. Este problema, bien conocido y atacado en model checking, se magnifica en el ámbito de model checking cuantitativo (i.e. model checking de propiedades cuantificadas probabilísticamente). Los algoritmos de model checking cuantitativo, además de almacenar los estados en memoria deben resolver un sistema de optimización lineal donde cada variable esta asociada a un estado, y cada desigualdad a una transición probabilística. Asimismo planeamos implementar las técnicas estudiadas dentro en un model checker. Nos enfocaremos en extender el model checker Rapture.
Este fue un proyecto de mobilidad financiado por el CONICET (AR) y el CNRS (FR). Comenzó en el año 2005 y duró 2 años.
Participantes