Fundamentos, Algoritmos y Herramientas 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, eficiente, haciendo un buen uso de los recursos 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. Las técnicas formales proveen un enfoque matemático para modelar, comprender y analizar sistemas en las diversas etapas del desarrollo de éstos, desde el análisis de requerimiento y la especificación hasta la construcción del programa y el testing del software producido. Más aún, el estudio fundamental de los lenguajes de programación y los lenguajes de especificación y su interpretación a través de dominios matemáticos, garantizan la posibilidad del análisis rigurosos de los sistemas, a partir de la implementación o de la especificación de alto nivel de tales sistemas.
El programa dirige la atención a la producción de técnicas 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 de manera tal que sean eficientes no solo en la resolución del problema sino también en el uso de los recursos, y sus aplicaciones a casos de estudio.

Cinco de los seis 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. El sexto proyecto se enfoca en la producción de algoritmos masivamente paralelos supereficientes en el cómputo y en el uso de sus recursos, en particular la energía, enfocándose en algoritmos numéricos. Este tipo de soluciones son la base para el desarrollo de herramientas eficientes, sobre todo aquellas que requieren de grandes cálculos numéricos como los model checkers probabilista o las técnicas de síntesis asociadas a diagnosis con probabilidad o con tiempo
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 y ya comenzó a tener sus frutos con el programa pasado. Esperamos con este programa poder potenciar estos primeros esfuerzos y crear nuevos lugares de intercambio de conocimiento.

Los proyectos que conforman este programa son:

  • Fundamentos y Técnicas para el Análisis de Fiabilidad de Sistemas Distribuidos y Estocásticos (Director: Pedro R. D’Argenio).
  • Semántica de Lenguajes de Programación (Director: Daniel Fridlender).
  • Computación Heterogénea de Alto Desempeño (Director: Nicolás Wolovick).
  • Meta-teoría e implementación de un lenguaje con tipos dependientes (Director: Miguel Pagano).
  • Generación de modelos abstractos de comportamiento basados en habilitación (Director: Matías D. Lee).
  • Diagnosticabilidad y testing de sistemas distribuidos (Director: Laura Brandán Briones).

Este programa es la continuación del programa SeCyT-UNC 05/BP02 (2012-2013) y es financiado por la Universidad Nacional de Córdoba. Comenzó en el 2014 y se extiende por dos años.