OFFBEAT : una extensión de PRISM para el análisis de sistemas temporizados tolerantes a fallas

Abstract

Los sistemas tolerantes a fallas son aquellos que son capaces de seguir operando luego de la ocurrencia de una o más fallas. Una falla puede provocar cambios no deseados en el estado interno del sistema, y para que el sistema tolere la falla, deberá ser capaz de soportar estos cambios y continuar operando de la manera esperada. Los sistemas tolerantes a fallas son comunes en casos donde una falla no es aceptable, ya que la misma puede derivar grandes pérdidas, tanto económicas como de vidas humanas. Otra técnica para garantizar que un sistema funcione de la manera que corresponde es el model checking, una técnica de verificación automática que permite determinar se el modelo de un sistema cumple una propiedad determinada. En caso de que el sistema no satisfaga la propiedad, el model checker generalmente proporciona un contraejemplo de ayuda para determinar la fuente del error. En el presente trabajo se detallan los modelos e ideas usadas para la construcción de un model checker probabilista temporizado, pensado para la verificación de sistemas tolerantes a fallas. Se describirá el proceso de inyección de fallas en los modelos formales, la sintaxis del lenguaje de la herramienta, el proceso de traducción del mismo al lenguaje de PRISM (el model checker sobre el cual se provee la capa de abstracción), y la aplicación de la herramienta desarrollada a dos casos de estudio.