Ciencias de la Computación (plan 1994) 2014-1

Grupo 7023, 20 lugares. 5 alumnos.

 

Métodos Formales. 2014-1, de agosto a diciembre de 2013

Profesor Miguel Carrillo Barajas. miguel_carrillob@yahoo.com

Temario. Métodos Formales.

Descripción General.

El objetivo principal es introducir a las 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, haciendo énfasis 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, semántica, y deducción formal. Conocimientos generales de ciencias de la computación: tipos de datos, decidibilidad, complejidad. Dado que el curso combina teoría (fundamentos de las herramientas automatizadas) y práctica (uso de las herramientas), es recomendable a estudiantes de ciencias con interés en el conocimiento y uso de métodos formales.

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 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.

5. Aplicaciones

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.

- J.P. Katoen, C. Baier. "Principles of Model Checking". MIT Press 2008.

- H. A. Gabbar (editor) . "Modern Formal Methods and Applications". Springer 2006.

- 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.