Métodos Formales para la Síntesis y Verificación de Tolerancia a Fallas en Sistemas Concurrentes

En este proyecto se propone el desarrollo de métodos y herramientas automáticas con fundamentosformales para la verificación y construcción de programas tolerantes a fallas, es decir, aquellos programas que pueden continuar operando de una forma aceptable aún bajo la ocurrencia de fallas y/o errores. En particular, se utilizarán lógicas temporales, deónticas y probabilistas para la especificación de sistemas tolerantes a fallas. Por una parte, las lógicas temporales permiten especificar sistemas concurrentes y reactivos, en cuanto las lógicas deónticas hacen posible distinguir las ejecuciones correctas de un sistemas de aquellas incorrectas, a la vez que los operadores probabilistas son necesarios para conocer con precisión el grado de tolerancia a fallas exhibidos por un sistema. El principal objetivo del proyecto es desarrollar herramientas de software, y sus fundamentos, que permitan, por un lado, verificar propiedades automáticamente sobre sistemas, y por otro lado, obtener programas desde sus especificaciones, es decir, sintetizar programas. El grupo responsable del proyecto ha desarrollado trabajos preliminares (que son detallados en el reporte técnico) en estos tópicos, se pretende en este proyecto continuar en esta líneas de investigación, produciendo las herramientas necesarias, y los marcos teóricos correspondientes, para poder utilizar estos formalismos en la práctica.

Financiamiento :

Área temática:

Ultimas novedades