FALLUTO : Un model checker para la verificación de sistemas tolerantes a fallas / Edgardo E. Hames.
Detalles de publicación: [S.l. : s.n. ], 2009. Descripción: 113 p. : il. ; 30 cm. + 1 CDTema(s): Nota de disertación: Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2009. Resumen: Muchos equipos informáticos de nuestra vida cotidiana necesitan aplicaciones de alta disponibilidad y otros operan en lugares de difícil acceso. Estos sistemas están sujetos a una variedad de fallas potenciales que pueden corromper o degradar su rendimiento. El model checking es una técnica de verificación formal que, dado un modelo de un sistema y una propiedad requerida, permite decidir automáticamente si la propiedad es satisfecha o no. Este trabajo presenta 1) un lenguaje declarativo para el modelado de fallas, 2) Falluto, una herramienta de model checking para la verificación de sistemas tolerantes a fallas, 3) un método de verificación para dichos sistemas y 4) su aplicación a dos casos de estudios reales en sistemas distribuidos, haciendo uso del lenguaje y la herramienta.Tipo de ítem | Biblioteca actual | Signatura | Copia número | Estado | Notas | Fecha de vencimiento | Código de barras | Reserva de ítems |
---|---|---|---|---|---|---|---|---|
Trabajo Especial de Grado | FaMAF Secc. Tesis y Trabajos especiales | Trabajo Especial Computación CAJA 10 - 20088 | 1 | Disponible | 20088 | |||
CD/DVD de datos | FaMAF Secc. Tesis y Trabajos especiales | TE C HAM | 1 | No para préstamo (Acceso restringido) | Copia de resguardo | 20088CD | ||
Trabajo Especial de Grado | FaMAF Depósito Interno | TE C HAM ej.2 | 2 | Disponible | 20089 | |||
CD/DVD de datos | FaMAF Depósito Interno | TE C HAM ej.2 | 2 | Disponible | 20089CD |
Incluye CD.
Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2009.
Bibliografía: p.11-114.
Muchos equipos informáticos de nuestra vida cotidiana necesitan aplicaciones de alta disponibilidad y otros operan en lugares de difícil acceso. Estos sistemas están sujetos a una variedad de fallas potenciales que pueden corromper o degradar su rendimiento. El model checking es una técnica de verificación formal que, dado un modelo de un sistema y una propiedad requerida, permite decidir automáticamente si la propiedad es satisfecha o no. Este trabajo presenta 1) un lenguaje declarativo para el modelado de fallas, 2) Falluto, una herramienta de model checking para la verificación de sistemas tolerantes a fallas, 3) un método de verificación para dichos sistemas y 4) su aplicación a dos casos de estudios reales en sistemas distribuidos, haciendo uso del lenguaje y la herramienta.