Fundamentos, algoritmos y herramientas para el desarrollo de sistemas distribuidos confiables

Los sistemas de computación son cada vez más ubicuos. La mayoría de éstos están integrados en sistemas físicos con comportamientos de altísima complejidad. Los podemos encontrar en electrónica de consumo, como controladores en sistemas industriales, en maquinarias agrícolas, en equipos médicos, en aviónica y satélites, a bordo de automóviles y otros sistemas de transportes, etc. Hoy en día también se busca que estos sistemas computacionales sean eficientes en el consumo de energía dado que se espera gran autonomía (por ejemplo en redes de sensores inalámbricas o en dispositivos computacionales móviles para auxilio de discapacitados o ancianos). Por consiguiente dependemos fuertemente del funcionamiento apropiado de estos sistemas. Necesitamos que estos dispositivos brinden servicios correctos, confiables, seguros, y que estén continuamente disponibles.

Dado que la mayoría de estos sistemas se integran con un entorno físico complejo, su modelado requiere de herramientas matemáticas mucho más poderosas y expresivas que las lógicas bivaluadas y los modelos discretos habituales. Dada la presencia de parámetros de tiempo real y requerimientos continuos como voltajes, intensidad de corriente, temperaturas, presión, etc., que necesitan ser cuantificados de diversas maneras, inclusive estocásticamente, los modelos matemáticos y las lógicas para la descripción de sistemas son inherentemente intratables. Por consiguiente, la verificación y análisis directo de estos tipos de modelos y lógicas es inviable, por lo que se requieren técnicas de abstracción, aproximación o simulación.

Dos ingredientes son esenciales para el modelado de estos sistemas: (a) el no-determinismo, que representa de manera abstracta tanto la concurrencia entre procesos paralelos o distribuidos como las decisiones locales en una componente, y (b) la probabilidad, que permite cuantificar localmente la ocurrencia de eventos tales como el tiempo de arribo o la probabilidad de la ocurrencia de una falla. Además, ambos deben poder modelar el dominio continuo.

El objetivo de este proyecto es contribuir con las herramientas necesarias para la verificación y análisis de eficiencia y confiabilidad en general de modelos de sistemas distribuidos con características continuas y aleatorias. Se pretende contribuir en los tres aspectos de este área: fundamentos matemáticos, algoritmos, y la construcción de herramientas de verificación y análisis.

El objeto de estudio de este trabajo serán los Procesos de Decisión de Markov (PDM) ya sea en un dominio discreto o continuo. Los PDM, también llamados autómatas probabilistas o sistema de transiciones probabilistas, son objetos que combinan elecciones no-deterministas (como en los autómatas o los sistemas de transiciones) y transiciones probabilistas o kernels de Markov (como en las cadenas de Markov). A continuación detallamos los cuatro objetivos específicos que abordaremos en este proyecto.

  1. Estudio de las semántica de procesos probabilistas y no-deterministas.
  2. Estudio de técnicas de discretización de modelos continuos mediante abstracciones y aproximaciones.
  3. Construcción de herramientas para la verifiación de sistemas distribuidos probabilistas bajo observación parcial.
  4. Contribución al desarrollo de model checkers estadísticos.

Este proyecto se ejecuta bajo el financiamiento del FONCYT (ANPCyT). Comenzará en 2013 y tiene tres años de duración.

Grupo responsable
Pedro R. D'Argenio (Director)
Pedro Sánchez Terraf
Nicolás Wolovick
Otros Investigadores
Damián Barsotti
Matías D. Lee
Silvia Pelozo
Carlos E. Budde

Raúl Monti
Carlos S. Bederián
Laura Brandán Briones
Ricardo Corin