Fundamentos, Algoritmos y Herramienta para la Construcción de Programas Confiables

Los sistemas de computación se están haciendo cada vez más ubicuos. Interactuamos continuamente con ellos, de manera directa o indirecta. Los ejemplos abundan: servicios web, sistemas médicos, dispositivos móviles, automóviles, aviones, electrónica de consumo, redes de comunicación, e inclusive la tan omnipresente red eléctrica. Por consiguiente, la vida moderna depende más que nunca del funcionamiento correcto de estos sistemas.

De esta manera, necesitamos que los sistemas de computación provean el servicio para el cual fueron creados de manera correcta, confiable, segura, respetando la confidencialidad e integridad de los datos y, además, que se encuentre disponible en el momento que requerimos de ellos.

Las garantías para la satisfacción de tales características solo pueden estar fundadas en técnicas de especificación y análisis rigurosas que se apliquen tanto a la funcionalidad requerida del sistema como al comportamiento de éste. Los métodos formales proveen un enfoque matemático para modelar, comprender y analizar sistemas en las diversas etapas del desarrollo de estos, desde el análisis de requerimiento y la especificación hasta la construcción del programa y el testing del software producido.

Los proyectos que conforman este programa dirigen la atención a la producción de métodos formales que permitan la construcción de software correcto, seguro y eficiente, teniendo en cuenta tanto parámetros cualitativos como cuantitativos.

Nuestro objetivo es cubrir todos los aspectos de los métodos formales:

  • aspectos fundamentales, que describen las bases matemáticas y lógicas de las técnicas producidas;
  • aspectos algorítmicos, que son las bases conceptuales sobre los que se paran las herramientas de especificación, verificación y análisis; y
  • aspectos prácticos, que se enfocan en la construcción de tales herramientas y su aplicación en casos de estudio.

Los diversos proyectos que conforman este programa se enfocan en distinto grado en estos aspectos, haciendo uso de diversas técnicas, las cuales incluyen técnicas asercionales asistidas con demostradores de teoremas, model checking, técnicas basadas en teoría de tipo, SAT y SMT así como testing y diagnosticabilidad.

Se espera que el programa fortalezca la interacción de los distintos equipos de trabajo y enriquezca la cooperación transversal. Esta interacción tiene como valor agregado la ampliación del campo de conocimiento de los recursos humanos que se forman en este contexto.

Los proyectos que conforman este programa son:

  • Construcción y verificación automática de programas utilizando herramientas deductivas (Director: Javier Blanco).
  • Fundamentos y Técnicas para el Análisis de Fiabilidad de Sistemas Distribuidos y Estocásticos (Director: Pedro R. D’Argenio).
  • Métodos y Herramientas para Desarrollo de Software de Calidad (Director: Daniel Fridlender).
  • Testing, Diagnosticabilidad y Verificación Formal de Seguridad y Funcionalidad en Implementaciones de Protocolos Criptográficos y Sistemas Distribuídos (Director: Ricardo Corin)
  • Verificación automática de programas probabilistas y no-deterministas utilizando probadores de teoremas (Director: Damián Barsotti)

El programa es financiado por la Universidad Nacional de Córdoba. Comenzó en el 2012 y se extiende por dos años.