Verificación automática de programas probabilistas y no-deterministas utilizando probadores de teoremas

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. Hoy en día es casi inevitable la interacción cotidiana con sistemas basados en implementaciones de algoritmos aleatorios. La masificación de los mismos puede verse con mayor claridad en implementaciones de protocolos de comunicación a nivel hardware y soluciones probabilistas a problemas distribuidos, ambos utilizados en sistemas de comunicación como parte indispensable de sistemas mayores (aviones, autos, controladores de diversos tipos de tráfico, equipo médico, etc.). Estos algoritmos se encuentran generalmente embebidos en mecanismos de hardware producidos en serie, por lo que un error en los mismos puede llegar a producir un efecto multiplicador de sus efectos nocivos, que van desde una molestia en el usuario hasta situaciones que pueden poner en peligro la vida humana o inclusive generar serias catástrofes.

Las componentes aleatorias se suelen utilizar de dos maneras diferentes. Una posibilidad es introducirlas en el modelado de sistemas distribuidos para representar, por ejemplo, ruido en la comunicación, pérdida de mensajes, fallas de componentes de sistema o la disponibilidad de un recurso. Otra posibilidad es emplearlas para lograr soluciones mejores y más eficientes, usualmente brindando un trade-off entre precisión y velocidad de respuesta. Notablemente existen algoritmos que al incorporar aleatoriedad logran soluciones inexistentes en el dominio de los algoritmos tradicionales.

El hecho de considerar probabilidades dentro del comportamiento de los sistemas implica que el conjunto de propiedades asociadas se sale de la lógica usual. En este ámbito, no tiene sentido verificar que una propiedad del programa se cumple. Lo que se verifica es si la propiedad se cumple con cierta probabilidad. Actualmente el mayor esfuerzo se lleva a cabo en el estudio y desarrollo de herramientas denominadas chequeadores de modelos probabilistas. En las mismas, dado un modelo finito del sistema estocástico, se obtienen varias medidas de performance en forma automática.

Los métodos asercionales, como la lógica de Hoare o el cálculo de weakest precondition, permiten el razonamiento sobre programas directamente sin la consideración explícita de los estados y abstrayendo los pasos de ejecución. Esto posibilita, en contraposición a la técnica de chequeo de modelos, trabajar con modelos infinitos y resolver el problema de la explosión del espacio de estados que poseen aquellas técnicas. Además, para el caso de los métodos asercionales se utiliza lógica de primer orden y alto orden, las cuales son más expresivas que las utilizadas en los chequeadores de modelos. El problema que surge al intentar utilizar estos métodos es que necesitan de la intervención humana al momento de desarrollar las pruebas de corrección sobre los programas. En este sentido, se ha venido trabajando en su automatización mediante el uso de probadores de teoremas.

Existen métodos asercionales para el análisis de programas probabilistas. Morgan et al. definieron un cálculo de weakest preespectation (pGCL) que generaliza el cálculo de weakest precondition de Dijkstra. El objetivo de este proyecto es estudiar las posibilidades en este área, sin descuidar la automaticidad de las técnicas a desarrollar. En este último sentido entra en juego el uso de las herramientas asercionales denominadas SMT solvers. Las mismas están orientadas a la verificación automática de propiedades escritas en lógica proposicional donde los términos pueden pertenecer a distintas teorías (aritmética lineal, funciones no interpretadas, arreglos, etc.) e incluyen la posibilidad de expresar cuantificaciones de primer orden.

El objetivo de este proyecto es estudiar y desarrollar técnicas y métodos para el análisis estático de programas probabilistas y no-deterministas de propósito general utilizando herramientas deductivas automáticas.

Participantes

Damián Barsotti (Director)
Nicolás Wolovick (Co-director)