Presentación del grupo 7041 - 2010-1.

Temario. Introducción a Métodos Formales.

Para la materia:
Horario:
Miguel Carrillo Barajas. http://geocities.com/miguel_carrillob

Objetivos Generales.

Introducir a la técnicas formales de especificación y verificación formal. El curso se concentra en la técnica de model-checking, con referencias puntuales a la técnica de demostración automática. Se introduce al conocimiento básico de dos sistemas de especificación y verificación formal: NuSMV y Alloy. Dependiendo de la velocidad del curso y del interés del grupo, se estudian otros sistemas de especificación y verificación formal.

Requisitos.

Es recomendable tener interés por la aplicación de métodos formales (Matemáticas) en computación y conocimientos básicos de: sintaxis y semántica de una lógica; sistemas formales; estructuras de datos. El curso combina teoría y práctica; está dirigido a estudiantes de Ciencias de la Computación y de Matemáticas.

Temario
1. Introducción
1.1 Especificación formal.
1.2 Necesidad de verificación/demostración.
1.3 Métodos formales. El enfoque lógico.
1.4 Lógica. Expresividad vs complejidad.
2. Elementos de model checking. NuSMV
2.1 Modulación con sistemas de transición de estados.
2.2 Especificación con Lógica temporal. CTL, LTL, CTL*.
2.3 Un algoritmo para CTL-model-checking.
2.4 Problema de la explosión de estados. BDDs.
2.5 Ventajas y desventajas de NuSMV.
3. Especificación/verificación con Alloy.
3.1 Especificación con Signaturas.
3.2 Verificación con Lógica relacional de 1er. orden.
3.3 Fundamentos de Alloy. Solucionadores de SAT.
3.4 Ventajas y desventajas de Alloy.
4*. Otros sistemas de especificación y verificación formal.
4.1 El sistema Maude. Lógica de reescritura.
4.2 Especificación de Estructuras de datos en Maude.
4.3 Demostrador inductivo de teoremas (ITP).
4.4 Ventajas y desventajas de Maude.

La profundidad de los temas del punto 4* dependen de la velocidad del curso.

Bibliografía

- M. Huth M, M. Ryan. "Logic in computer science: modelling an reasoning about systems". 2004.
- E. Clarke, O. Grumberg, D. Peled. Model Checking. MIT press 2000.
- WWW. "Model Checking at CMU", http://www-2.cs.cmu.edu/~modelcheck/. 2007.

- D. Jackson. Software Abstractions: Logic, Language, and Analysis. 2006.
- WWW. The Alloy Analyzer. http://alloy.mit.edu/. 2007.

- N. Martí, M. Palomino, A. Vallejo. A tutorial on specifying data structures in Maude. 2005.
- WWW. The Maude System. http://maude.cs.uiuc.edu/. 2007.

- The Formal Semantics of Programming Languages: an introdution. G. Winskel. MIT press 1993.