Lógica, programación
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.
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.
Clases magistrales. Trabajos asignados periodicamente. Trabajo final.
Participación en clase. Trabajos.
Calidad de las contribuciones orales en clase.
Corrección y creatividad mostrada en la resolución de los trabajos.
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.
Artículos citados en clase.