Falluto2.0 un model checker para la verificación automática de sistemas tolerantes a fallas

Abstract

Los sistemas computacionales juegan roles determinantes en muchas áreas de nuestra vida cotidiana. En algunos casos la dependencia hacia estos sistemas es crítica, y el mal funcionamiento de los mismos puede acarrear grandes pérdidas económicas o hasta de vidas humanas. Las fallas en el diseño del sistema, como así también aquellas fallas causadas por el entorno de ejecución, pueden llevar a un comportamiento erróneo del mismo. Los sistemas tolerantes a fallas son capaces de lidiar con la presencia de fallas y sobrellevar estas situaciones que en otros casos llevarían al mal funcionamiento de los mismos. Dar la capacidad de tolerar fallas a un sistema computacional no es sencillo y es muy propenso a introducir nuevos errores. La verificación de la corrección de estos sistemas es entonces de vital importancia. El model checking es una técnica formal que se encarga de verificar exhaustivamente que el modelo de un sistema cumpla con un conjunto de propiedades. En este trabajo se presenta un lenguaje para el modelado de sistemas tolerantes a fallas y la especificaci´on de propiedades sobre los mismos. Se provee además la herramienta de verificación Falluto2.0, construida como front-end para el model checker simbólico NuSMV, la cual utiliza el lenguaje descripto. Se analiza la simplicidad y practicidad del lenguaje como así también su corrección. Por último se observa el uso de la herramienta sobre dos casos particulares de modelado de sistemas tolerantes a fallas.