Lògica, Programació.
1.- Descriure algorismes distribuïts diversos.
2.- Formar en les nocions fonamentals necessàries per entendre la recerca moderna en
verificació formal d'algorismes distribuïts:
2.1.- Sistemes de modelat.
2.2.- Lògiques per expressar propietats dels models.
2-3.- Mètodes per verificar que el model satisfà les propietats:
verificació interactiva i verificació amb model checkers.
3.- Treballar les nocions i mètodes anteriors sobre algorismes distribuïts concrets, tan en el camp
de les xarxes de computadors com en el del hardware digital.
4.- Introduïr eines software actuals per verificació automàtica: SPIN i UPAAL.
Introducció a la verificació: Modelat formal amb màquines de trasicions finites. Aplicació de la lògica
de primer ordre per expressar propietats. Mètode inductiu bàsic de verificació d'invariants.
Verificació interactiva d'algorismes amb infinits estats amb el mètode de Manna-Pnueli: Modelat amb
FTS's, justicia forta i feble. Notació SPL amb paral.lelisme explícit i primitives de comunicació.
Notació PADD.Semàntica sobre FTS's. Lògica temporal LTL. Expressió de propietats de seguretat.
Mètodes específics de verificació. Aplicació a exemples diversos: assignadors de recursos
distribuïts, amb àrbitre central i en anell, algorismes d'exclusió mútua.
Verificació automàtica amb model checkers: Estructures de Kripke. Autòmats de paraules
infinites, autòmats de Büchi. Conversió a autòmats de Büchi d'estructures de Kripke. Verificació
com a problema de conteniment de llenguatges. Expressió de propietats amb lògica d'arbres de
computació, CTL. Verificació de models local i global. Introducció al verificador SPIN
Verificació de sistemes de temps real: Autòmats temporitzats. Paraules infinites temporitzades.
Acceptació. Autòmats Zeno. Modelat i expressió de propietats amb autòmats temporitzats. Graf
infinit de transicions. Composició en paral.lel d'autòmats temporitzats. Conversió a l'autòmat de
regions finites i verificació de models temporitzats. Introducció al verificador UPAAL. Exemples
de verificació de propietats de sistemes distribuïts de temps real.
Verificació amb regles formals d'eliminació de comunicacions internes: Equivalència d'interfície. Lleis
d'equivalència de notacions tipus SPL i PADD. Lleis pròpies d'eliminació de comunicacions.
Algorisme d'eliminació formal de comunicacions. Demostracions de sequencialització formal de
sistemes distribuits. Aplicació a un model del processador DLX-MIPS.
Classes magistrals. Treballs assignats periòdicament. Treball final.
Participació a classe. Treballs.
Qualitat de les contribucions orals a classe.
Correctesa i creativitat mostrada en la resolució dels treballs.
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.
Articles diversos referits a classe.