Presentación del grupo 7043 - 2012-1.

Profesor Miguel Carrillo Barajas. Ayudante Laura Leonides

miguel_carrillob@yahoo.com

Temario. Métodos Formales.

Introducir a la técnicas formales de especificación y verificación mediante el uso de herramientas automatizadas. El curso ofrece un panorama representativo, de los métodos formales basados en lógica, delineado con los aspectos de expresividad-complejidad y semántica-deducción. Se introduce al uso básico de herramientas automatizadas de especificación y verificación formal: NuSMV, Alloy, Prover9 y Maude. Se muestran las tendencia recientes en el área de métodos formales y una perspectiva de su desarrollo resaltando las dificultades conocidas.

Requisitos.

Interés por la aplicación de métodos formales. Conocimientos básicos de lógica: sintaxis y semántica; sistemas formales de deducción. Conocimientos generales de ciencias de la computación: tipos de datos; decidibilidad, complejidad. El curso combina teoría (fundamentos de las herramientas automatizadas) y práctica (uso de las herramientas). Está dirigido a estudiantes de Ciencias de la Computación y de Matemáticas.

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 Métodos semánticos y métodos sintácticos.

1.5 Expresividad vs complejidad.

2. Métodos basados en lógica temporal.

2.1 Modelación con sistemas de transición de estados.

2.2 Especificación con Lógica temporal. CTL, LTL, CTL*.

2.3 Un verificador para CTL y LTL. NuSMV

2.4 Un algoritmo para CTL-model-checking.

2.5 Ventajas y desventajas de NuSMV. Extensiones de CTL.

3. Métodos basados en lógica de primer orden. Alloy. Prover9

3.1 Lógica de primer orden (FO). Alcances y limitaciones.

3.2 Signaturas relacionales (FO_R) y extensiones de FO (FO+TC, FO+LFP).

3.3 Especificación con FO_R+TC.

3.4 Un buscador de modelos. Alloy.

3.5 Especificación con FO (contraste con FO+TC)

3.6 Un demostrador automático para FO. Prover9

4. Métodos basados en otras lógicas.

4.1 Lógica de reescritura.

4.2 Especificación de Estructuras de datos en Maude.

4.3 Un demostrador inductivo de teoremas (ITP).

4.4 Herramientas automatizadas basadas en Maude.

Bibliografía

- M.Huth M, M.Ryan. "Logic in computer science: modelling and 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/. 2009.

- WWW. NuSMV: a new symbolic model checker. http://nusmv.irst.itc.it/. 2010

- D. Jackson. Software Abstractions: Logic, Language, and Analysis. 2006.

- WWW. Alloy Community. http://alloy.mit.edu/. 2009.

- WWW. Prover9 and Mace4. http://www.cs.unm.edu/~mccune/prover9/ 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.