Fundamentos, Algoritmos, Métodos 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 se sostiene sobre los cuatro aspectos necesarios que para lograr la producción y adopció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. Estos aspectos son:

  • Aspectos Fundamentales: definen y estudian las bases matemáticas y lógicas de las técnicas y herramientas para el análisis de sistemas computacionales. Definen el marco formal para la especificación y modelado de propiedades y sistemas, alcanzando tanto a los lenguajes (sintaxis) y la interpretación de los modelos y propiedades (semántica).
  • Aspectos Algorítmicos: son las bases conceptuales sobre los que se paran las herramientas de especificación, verificación y análisis. Establecen los métodos efectivos para llevar a cabo los diversos análisis. Dentro de este aspecto se busca comprender los alcances de efectivamente llevar a cabo el análisis (decibilidad) y en tal caso de hacerlo de manera eficiente (complejidad).
  • Aspectos Tecnológicos: se enfocan en la construcción de las herramientas de manera tal de optimizar su desempeño, no solo en la resolución del problema sino también en el uso de los recursos, y sus aplicaciones a casos de estudio. Esto incluye la adopción de estructura de datos apropiadas, la paralelización de los algoritmos, la comprensión y uso de tecnologías para computación de alto desempeño, incluyendo clusters y GPGPU.
  • Aspectos Educativos: ataca fundamentalmente el problema de la adopción. La reticencia por parte de la industria al uso de métodos y técnicas formales para el análisis de sistemas computacionales se debe fundamentalmente al desconocimiento de estas y de su efectividad.
    Cada uno de los proyectos que conforman este programa está orientado a atacar fuertemente al menos uno de estos aspectos, sin descuidar su conexión con la necesidad de los otros aspectos.

Cada uno de los proyectos que conforman este programa está orientado a atacar fuertemente al menos uno de estos aspectos, sin descuidar su conexión con la necesidad de los otros aspectos.
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)
  • Interacciones entre Matemática y Computación Teórica (Director: Pedro Sánchez Terraf)
  • Computación Heterogénea de Alto Desempeño (Director: Nicolás Wolovick)
  • Integración de Herramientas y Métodos para la Enseñanza de la Programación (Director: Damián Barsotti)
  • Diagnosis & Diagnosticabilidad de Sistemas y su Relación con Testing & Testabilidad (Directora: Laura Brandán Briones)

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