Métodos Formales de la Ingeniería del Software

English version (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

  1. Introducción: La trilogía del desarrollo del software.
  2. Procesos formales en el desarrollo del software:
    1. De programas a propiedades: Verificación automática del Sofware: Model-checking, Herramientas industriales de verificación automática. Especificación y prototipado.
    2. De propiedades a programas: Síntesis de programas. Programación automática.
    3. De datos a programas: Aprendizaje automático de programas
    4. De programas a programas:
    5. Especialización y Transformación de Programas, Generación automática de compiladores. Diagnóstico racional
  3. 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

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.