Herramientas y mecanismos formales para el tratamiento de la tolerancia a fallas | Tesis del Doctorado en Ciencias de la Computación

Tribunal Especial

Titulares:

Dr. Silvio Miguel GONNET (CONICET - UTN, Santa Fe)

Dr. Raúl Alberto FERVARI (FAMAF)

Dr. Valentín CASSANO (UNRC)

Google meet: meet.google.com/nzb-zecq-jfj

Resumen: La confiabilidad es uno de los atributos de calidad más importantes asociados al desarrollo de software, y la corrección de software (es decir, en qué grado el software cumple con el propósito para el cual fue desarrollado) es, tal vez, el factor más importante asociado a la confiabilidad. Además de los defectos de software tradicionales (bugs) que afectan a la corrección del software, existen en numerosos casos eventos externos, fuera del control directo del software, que pueden provocar comportamiento anómalo, o indeseado. Algunos ejemplos concretos son los correspondientes a fallas en dispositivos de hardware, cortes de energía eléctrica, fallas de comunicación, entre otros. Todo análisis de confiabilidad, especialmente para sistemas críticos, es decir, sistemas en los cuales el mal funcionamiento del software o hardware pueden llevar a drásticas consecuencias (sistemas de control de plantas nucleares, vehículos espaciales, etc.), necesita poder razonar acerca de los efectos de estos eventos y cómo el software los tolera, o reacciona ante los mismos; el área general que estudia mecanismos para responder a fallas, y razonar sobre sus consecuencias, es el área de sistemas tolerantes a fallas. En esta tesis abordamos la tolerancia a fallas desde una perspectiva formal. Analizamos y diseñamos herramientas formales generales para contribuir al proceso de construcción y razonamiento sobre sistemas tolerantes a fallas, desde etapas tempranas del proceso de desarrollo. Estas herramientas nos permiten capturar conceptos fundamentales de la tolerancia a fallas, incluyendo sus intuiciones, clasificaciones y técnicas de tolerancia, desde una mirada formal, y definir herramientas lógicas para la especificación y verificación de sistemas tolerantes a fallas. En particular, diseñamos lenguajes lógicos para la captura de la tolerancia a fallas, y traducciones de éstos a mu-cálculo, para verificación automática.