Ingeniería del Software Automática
U. Nacional de San Luis, Argentina
Octubre 31 - Noviembre 2, 2006



María Alpuente
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:

    1. Ingeniería del Software Automática (Slides del curso)

      • La trilogía del desarrollo del software.
      • Métodos formales, la aproximación lightweight.
      • Lógicas para aplicaciones software

    2. Procesos formales y tecnología ágil
    3. Herramientas de especificación y verificación automática  
    4. Temas avanzados (programación multi-paradigma)

    BIBLIOGRAFÍA COMPLEMENTARIA

    PRÁCTICAS:

    Aquí se pueden encontrar algunos ejercicios
    Ejercicios aula, Trabajo personal