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:
- 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
- Procesos formales y tecnología ágil
- Herramientas de especificación y verificación automática
- Temas avanzados (programación multi-paradigma)
