Verificación de Sistemas Críticos


Docente a Cargo
Pedro R. D'Argenio
Novedades
3-Ago Rreunión el 11 de octubre para coordinar clases (horario a definir)
3-Ago Este año (el 2004, para los distraidos) el curso comenzará la semana del 11 de octubre. Eso nos deja sólo 6 o 7 semanas de clases, asi que el curso será intensivo. Habrá 3 clases por semanas, y cada clase será de entre 2 a 3 horas. El resto del curso se organizará según se indica mís abajo. [Metodología]

Metodología del Curso

Habrá (en principio) cuatro trabajos prácticos que se hará en grupos de a dos. Cada uno de ellos estará organizado temáticamente como sigue:

1er Práctico LTL - Autómata de Büchi - Model checking LTL - Spin
2do Práctico CTL - Model checking CTL - Desarrollo de un pequeño model checker
3er Práctico TCTL - Autómatas temporizados - Model checking TCTL - Alcanzabilidad usando zonas - Uppaal
4to Práctico PCTL - Autómatas probabilisticos - Model checking PCTL

El programa tentativo del curso puede encontrarse en este link.


Cronograma Tentativo
11 de octubre
 Reunion para coordinar clases (horario a definir)

El resto todavía no está definido.
Prácticos
*
Primer práctico
*
Segundo práctico
*
Tercer práctico
*
Cuarto práctico

Punteros a model checkers

Los que nos interesan en el curso

Nombre Características
* Spin LTL - Orden Parcial
Bajar Spin en formato rpm (Gracias Damián por armarlos)
  spin-3.4.7-1.i386.rpm         spin-3.4.7-1.i586.rpm
  spin-3.4.7-1.i486.rpm         spin-3.4.7-1.i686.rpm
  spin-3.4.7-1.src.rpm
* SMV CTL - BDDs
* NuSMV CTL - BDDs
* Uppaal Autómatas temporizados - Zonas - Alcanzabilidad
* Kronos TCTL - Autómatas temporizados - Simbólico

Otros Más

Nombre Características
* CADP LOTOS - Sistemas de Transiciones Etiquetadas -
* The Concurrency Workbench NC CCS - mu-Calculus - Álgebra de Procesos - Bisimulación
* The Edinburgh Concurrency Workbench CCS - mu-Calculus - Álgebra de Procesos - Bisimulación
* LTSA CSP - Propiedades expresadas como procesos
* The Mobility Workbench pi-caclulus - mobilidad - mu-calculus
* RED Automatas Temporizados - Region-Encoding Diagram - Alcanzabilidad
* HyTech Automatas Hibridos - Simbólico - Alcanzabilidad - Safety - Paramétrico
* RAPTURE Sist. de Trans. Probabilisticas - Alcanzabilidad cuantificada - MTBDD - Abstracción
* PRISM Sist. de Trans. Probabilisticas - PCTL - MTBDD
* ETMCC Cadenas de Makov - CSL
* Bandera Java - LTL - CTL - Abstración

Bibliografía
*
Concepts, Algorithms, and Tools for Model Checking. J-P. Katoen. Friedrich-Alexander Universit at Erlangen-Nurnberg. 1999.
*
Model Checking. E.M. Clarke, O. Grumberg, y D. Peled. MIT press, 1999.
*
Simple on-the-fly automatic verification of linear temporal logic. R. Gerth, D. Peled, M. Y. Vardi, y P. Wolper. In Proc. 15th Work. Protocol Specification, Testing, and Verification. North-Holland, 1995.
*
The Temporal Logic of Reactive and Concurrent Systems: Specification. Z. Manna and A. Pnueli. Springer-Verlag, 1992.
*
Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice. Paul Pettersson. PhD Thesis, Uppsala University. Technical Report DoCS 99/101. February 1999. (Part II-A: Automatic Verification of Real-Time Communicating Systems by Constraint-Solving.)
Pedro R. D'Argenio /