Métodos Formales de la Ingeniería del Software

(unmaintained)

Nombre: Métodos Formales de la Ingeniería del Software
Semestre: 5A
Código: MFI
Créditos: 6 (3 Teoría + 3 Prácticas)
Profesores: María Alpuente, Santiago Escobar

Objetivos Siguiendo un enfoque moderno, que tiene en cuenta los tres elementos de la trilogía del software -programas, datos y propiedades-, estudiamos los procesos formales que transforman dichas componentes automáticamente, en particular los de mayor impacto industrial. Esto incluye, entre otros, los siguientes mecanismos: síntesis de programas, aprendizaje automático de programas, prototipado, model-checking, diagnóstico declarativo, evaluación parcial de programas, síntesis de escenarios, generación de oráculos.

A diferencia de otros métodos formales más convencionales (y a la vez poco prácticos), que fomentan la formalización excesiva mediante el empleo de lenguajes demasiado expresivos y que requieren una formación matemática poco habitual en los usuarios finales, proponemos una aproximación lightweight, basada en la aplicación selectiva y focalizada de los métodos formales, que resulta más efectiva y rentable en la práctica.

Syllabus

Análisis, especificación, depuración, verificación, certificación, síntesis, aprendizaje, transformación y optimización de programas (multiparadigma).

Temario

Introducción: La trilogía del desarrollo del software.
Procesos formales en el desarrollo del software:

De programas a propiedades: Verificación automática del Sofware: Model-checking, Herramientas industriales de verificación automática. Especificación y prototipado.

De propiedades a programas: Síntesis de programas. Programación automática.

De datos a programas: Aprendizaje automático de programas

De programas a programas:

Especialización y Transformación

Programación móvil. Transformación automática y verificación de código Java.

Prácticas

Se realizarán dos grupos de prácticas: 1) Modelización y verificación automática con SMV y SPIN;
2) El entorno Maude

Bibliografía

D. Le Metayer et al. Exploring the Software Development Trilogy. IEEE Software, Diciembre 1998
E. Clarke, O. Grumberg, D. Peled. Model Checking. MIT Press, 1999.
N.D. Jones and C.K. Gomard and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs, NJ, 1993.
P. Julián. Evaluación Parcial y sus Aplicaciones. Novática 163:40-46, 2003

Evaluación

Examen de teoría + prácticas, que consiste en un test de respuesta múltiple de 30 preguntas (aprox.), de caracter 'no tecnico',
sino de comprension global de conceptos y con un peso del 90% de la nota final

El otro 10% se obtiene a través de una participación más activa en la asignatura, mediante una de las siguientes posibilidades:
* explorar la literatura, eligiendo un tema de entre un conjunto de temas teóricos propuestos,
realizando una breve presentación en clase (aprox. 10-15 minutos).
* profundizar en las prácticas, realizando un trabajo relacionado con alguno de los bloques trabajados en el laboratorio.