Herramientas y mecanismos formales para el tratamiento de la tolerancia a fallas

Abstract

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.

In this thesis we approach fault tolerance from a formal perspective. We analyze and design formal tools for reasoning about fault-tolerant systems, mainly focusing on the early stages of the development process. The formal tools we study capture fundamental concepts of fault tolerance, including some founding intuitions, classifications, and tolerance techniques. Furthermore, we define logical tools for the specification and verification of fault-tolerant systems, in particular logical languages for expressing fault tolerance. We also construct translations from these logics into mu-calculus, for automatic verification.