INGENIERÍA DEL SOFTWARE AUTOMÁTICA
Postgrado Informática
Master ISMFSI (Módulo M2, Semestre A, 5 Créditos)

María Alpuente - Salvador Lucas- Santiago Escobar
DSIC, U. Politécnica de Valencia, España

PRESENTACIÓN DEL CURSO:

Los sistemas informáticos desempeñan un papel esencial en la Sociedad de la Información. A medida que la sociedad se implica más en tales sistemas, crece su dependencia hacia ellos y se hace patente la necesidad de asegurar la corrección de su comportamiento. Los usuarios de las nuevas tecnologías, trabajando en un contexto global donde cada vez más gente y organizaciones entran en contacto, cooperan y comercian, encuentran cada vez más frustrantes las consecuencias derivadas de los fallos de software (como el tener que reiniciar el equipo para recuperar un comportamiento estable del sistema), por no hablar de las repercusiones que pueden tener estos fallos en las áreas donde la seguridad es crítica.

La necesidad de ofrecer un nivel de prestaciones adecuado (corrección, seguridad, etc.) hace que los sistemas software modernos sean de una complejidad tal que su desarrollo, uso diario y mantenimiento exigen la utilización, durante las distintas etapas de su vida útil, de técnicas y herramientas de asistencia automáticas. Por su naturaleza, dichas técnicas deben descansar en fundamentos sólidos que permitan al usuario de los mismos (ingeniero de requisitos, programador,  o gestor) confiar en la aplicacion bajo cualquier circunstancia. Esta es la perspectiva que guía la aplicacion de los métodos formales en la ingeniería del software. Para mejorar los resultados de la aplicacion de los metodos formales, nuestro enfoque apuesta por una aproximacion ágil -lightweight- que, en contraste con otros métodos más tradicionales que promueven una formalización excesiva y que requiere una formación matemática poco habitual en los usuarios finales, se basa en una seleccion precisa y focalizada de los métodos y notaciones, que integra una variedad de lenguajes, técnicas formales y herramientas automáticas que resulta más beneficiosa en la práctica.

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 (modeling)
  • Verificación (model-checking)
  • Certificación (proof-carrying code)
  • Síntesis (machine learning)
  • Optimización (análisis y transformación)
  • Depuración (diagnóstico y corrección)
    •
    Utilizamos los lenguajes declarativos multiparadigma como instrumento tangible para soportar una aproximación ágil. Presentamos también algunas lógicas de bajo coste con capacidad para soportar (modelar y mecanizar) diferentes áreas de especialización en software: lógica clausal, ecuacional, dinámica, temporal, lineal, etc.

    PROGRAMA: 

    Introducción a la Ingeniería del Software Automática (introducción)

    • La trilogía del desarrollo del software.
    • Métodos formales, la aproximación lightweight.
    • Optimización (análisis y transformación basadas en la semántica)
    • Lógicas para aplicaciones software

    Procesos formales y tecnología ágil

    - Análisis y especificación
           * Sistemas de reescritura de términos y programación funcional (S. Lucas)
                   Propiedades de los Sistemas de Reescritura; Sistemas de Reescritura
           * Herramientas de especificación y verificación automática (M. Alpuente)
           * Integración de la programación lógica y funcional (M.  Alpuente)
    - Verificación (model-checking)
    - Depuración (diagnóstico y reparación)
    - Certificación (proof-carrying code)

    BIBLIOGRAFÍA  (Básica y Complementaria)

    PRÁCTICAS:

    Se realizarán tres grupos de prácticas:

    1. Análisis de terminación
    2. Modelización y verificación automática con SMV;  El entorno Maude
    3. Programación multiparadigma: El lenguaje Curry, Modelización en Curry

    EVALUACIÓN:

    La asignatura se evalúa mediante la resolución de cuestiones de caracter teórico-práctico, con dos partes separadas:

    A) Sistemas de reescritura de términos (S. Lucas): cuestiones cortas
    B) Métodos ágiles (M. Alpuente):     test de respuesta múltiple de 20 preguntas (aprox.)

    El peso de cada parte es del 50%, necesitándose una nota umbral de 4 (en cada parte)
    para promediar. En ambas partes se evaluan tanto los
    contenidos teóricos como los prácticos.

    Para la parte B se estudiará, de forma alternativa y particularizada a cada caso, la posibilidad
    de realizar una presentación o un desarrollo práctico.

    Aquí se pueden encontrar algunos boletines de problemas
    ejercicios aula, trabajo personal