Descripción
Los algoritmos distribuidos funcionan sobre redes de ordenadores o modelan el comportamiento del hardware. El análisis de su corrección es sutil. La asignatura introduce a la investigación moderna sobre métodos de análisis matemático de estos algoritmos. Comprende: notaciones de modelado, lógicas para la expresión de propiedades y métodos de verificación formal de las propiedades. También introduce herramientas software de verificación.
Tipo asignatura
Optativa
Semestre
Primero
Créditos
5.00
Conocimientos previos

Lógica, programación

Objetivos

1.- Describir varios algoritmos distribuidos.

2.- Formar en las nociones fundamentales necesarias para entender la investigación moderna en
verificación formal de algoritmos distribuidos:

2.1.- Sistemas de modelado.
2.2.- Lógicas para expressar propiedades de los modelos.
2-3.- Métodos para verificar que el modelo satisface las propiedades:
verificación interactiva y verificación con model checkers.

3.- Aplicar las nociones y métodos anteriores sobre algoritmos distribuidos concretos, tanto en
redes de computadors como en hardware digital.

4.- Introducir herramientas software actuales para la verificación automática: SPIN y UPAAL.

Contenidos

Introducción a la verificación: Modelado formal con máquinas de trasiciones finitas. Aplicación de la lógica
de primer orden para expresar propiedades. Método inductivo bàsico de verificación d'invariantes.
Verificación interactiva de algoritmos con infinitos estados con el método de Manna-Pnueli: Modelado con
FTS's, justicia fuerte i débil. Notación SPL con paralelismo explícito y primitivas de comunicación.
Notación PADD.Semántica sobre FTS's. Lógica temporal LTL.
Expresión de propiedades de seguridad.
Métodos concretos de verificación. Aplicación a varios ejemplos: asignadores de recursos
distribuidos, con árbitro central i en anillo, algoritmos de exclusión mútua.
Verificación automática con model checkers: Estructuras de Kripke. Autómatas de palabras
infinitas, autómatas de Büchi. Conversión a autómatas de Büchi de estructuras de Kripke. Verificación
como problema de contenimiento de lenguajes. Expresión de propiedades con lógica de árboles de
computación, CTL. Verificación de modelos local i global. Introducción al verificador SPIN
Verificación de sistemes de tiempo real: Autómatas temportzados. Palabras infinites temporizadas.
Aceptación. Autómats Zeno. Modelado y expressión de propiedades con autómatas temporizados. Grafo
infinito de transiciones. Composición en paralelo de autómatas temporizados. Conversión a autómata de
regiones finitas y verificación de modelos temporizados. Introducción al verificador UPAAL. Ejemplos
de verificación de propiedades de sistemes distribuidos en tiempo real.
Verificación con reglas formales de eliminación de comunicaciones internas: Equivalencia de interfaz. Leyes
de equivaléncia de notaciones del tipo SPL i PADD. Leyes propies de eliminación de comunicaciones.
Algoritmo de eliminación formal de comunicaciones. Demostraciones de secuencialización formal de
sistemas distribuidos. Aplicación a un modelo del procesador DLX-MIPS.

Metodología

Clases magistrales. Trabajos asignados periodicamente. Trabajo final.

Evaluación

Participación en clase. Trabajos.

Criterios evaluación

Calidad de las contribuciones orales en clase.
Corrección y creatividad mostrada en la resolución de los trabajos.

Bibliografía básica

Z. Manna, A. Pnueli, The temporal logic of reactive and concurrent systems. Springer 1991.

Z. Manna, A. Pnueli, Temporal verification of reactive systems. Springer 1995.

E. Clarke, O. Grumberg, D. A. Peled, Model checking, E.Clarke et. al. technologies 1999.

Material complementario

Artículos citados en clase.