Fundamentos de Ingeniería del Software Automática (FSA)

Módulo: Especialización

Materia: Técnicas de Soporte para el modelado, desarrollo y explotación de sistemas software (TSS)

Código: 32574     Créditos:   3 (2.5 teoría + 0.5 prácticas)     Semestre:   A



Profesores:

María Alpuente
Santiago Escobar
Salvador Lucas (responsable)


Objetivos:

El curso se centra en el estudio de métodos formales, y las técnicas y herramientas automáticas asociadas, para dar soporte sistemático y racional al desarrollo del software.  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 de forma automática, en particular los de mayor impacto industrial. Esto incluye, entre otros, los siguientes mecanismos: Análisis y especificación, Verificación, Certificación, Síntesis, Optimización y Depuración. Su formulación mediante el empleo de lenguajes lógicos para los cuales existen algoritmos de decisión o aproximaciones decidibles permite pasar de la pura formulación teórica al uso práctico mediante la implementación de dichos algoritmos. El uso de herramientas con una adecuada interfaz para el usuario (a menudo push and wait) permite a éste desentenderse de las complicaciones derivadas de su resolución manual.


Temario:

  1. Introducción a la Ingeniería del Software Automática
    1. La trilogía del desarrollo del software
    2. Métodos formales, la aproximación lightweight
    3. Lógicas para aplicaciones software
  2. Procesos formales y su tratamiento automático
    1. Análisis y especificación
      1. Sistemas de reescritura de términos
      2. Extensiones de los sistemas de reescritura
      3. Razonamiento ecuacional
    2. Verificación automática de propiedades
      1. Confluencia y determinismo
      2. Liveness y safety
      3. Reachability
    3. Certificación
  3. Herramientas automáticas para el desarrollo de software
    1. El entorno Maude
    2. Herramientas de análisis y certificación automática de propiedades computacionales

 

Metodología de enseñanza y aprendizaje

Clases de teoría, resolución de problemas, y prácticas de laboratorio.


Criterios y procedimientos de evaluación:

La asignatura se evalúa mediante la resolución de cuestiones y problemas de carácter teórico-práctico.


Bibliografía:

[BN98] Franz Baader and Tobias Nipkow. Term Rewriting and all That. Cambridge University Press, 1998.

[CDEL+07] Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott. All About Maude - A High-Performance Logical Framework. Lecture Notes in Computer Science, volume 4350, Springer-Verlag, 2007.

[MNR98] Daniel Le Metayer, Valèrie-Anne Nicolas, and Olivier Ridoux. Exploring the Software Development Trilogy, IEEE Software 15(6):75-81, 1998.

[Ohl02] Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002.