Diseño de Sistemas Correctos por Construcción

Profesor (Coordinador):
Manuel Carro
mcarro@fi.upm.es
Profesor:
Manuel Hermenegildo
herme@fi.upm.es

Semestre

Segundo semestre

Créditos

6 ECTS

Resumen

El software es cada vez más complejo y está a cargo de tareas críticas. Toda la tecnología destinada a garantizar la fiabilidad y calidad del software se está volviendo cada vez más relevante, si no completamente necesaria.

Solo los enfoques rigurosos (es decir, matemáticamente bien fundados) pueden certificar que el software cumple con los estándares de seguridad más altos. Estos enfoques incluyen, entre otros, el uso de lenguajes de especificación, lenguajes de programación de alto nivel (incluidos los lenguajes ecuacionales, funcionales y lógicos), el uso de verificación deductiva y basada en modelos, y enfoques de seguridad basados en las propiedades de los lenguajes que a menudo interactúan con demostradores de teoremas.

Objetivos

  • En este curso se dará una introducción, con un gran peso práctico, a los sistemas de desarrollo que siguen la filosofía de "desarrollo de sistemas correctos por construcción".
  • Aunque este curso no tiene una gran carga teórica, se espera que los alumnos tengan una buena comprensión de la lógica de primer orden y abundante experiencia de programación. Se explorarán varias metodologías que tienen diferentes bases, pero que comparten una idea central: desarrollar programas mientras se asegura que algunas propiedades no triviales que expresan requisitos de alto nivel sobre corrección, equitatividad y, a veces eficiencia, se respetan a lo largo de todo el desarrollo.

Programa

  1. Introducción a los métodos formales: pruebas de corrección de programas
  2. Fundamentos: especificación, lógica de primer orden, pruebas, programas
  3. Fundamentos de Event-B; la herramienta Rodin
  4. Sistemas secuenciales
  5. Event-B: fundamentos matemáticos y sus aplicaciones
  6. Sistemas reactivos: concurrencia y distribución

Bibliografía

Prerrequisitos:

  • Programación declarativa, lógica de primer orden, experiencia en programación (dos años mínimo), pruebas formales, métodos de razonamiento de la corrección de algoritmos.

Idioma en que se imparte

Inglés

Competencias Específicas

Código, descripción y nivel de cada una de las competencias específicas de la asignatura
Código Competencia Nivel
CEM1 Identificar, a partir del estado de la cuestión, la presencia de problemas de investigación relacionados con la concepción, la construcción, el uso y la evaluación de sistemas sociotécnicos complejos que hagan un uso intensivo de software. S
CEM4 Analizar y evaluar los diferentes paradigmas y enfoques de ingeniería de construcción y gestión de sistemas basados en software P
CEM5 Aportar soluciones a aquellos problemas abiertos relacionados con el ámbito de aplicación y los métodos, técnicas y herramientas de Verificación y Validación de Software A

Resultados de Aprendizaje

Código, descripción, competencias asociadas y nivel de adquisición de cada uno de los resultados de aprendizaje de la asignatura
Código Resultado de Aprendizaje Competencias asociadas Nivel de Adquisición
RA-AV-8 Ser capaz de usar herramientas existentes para la verificación formal de programas CEM4, CG7 C
RA-AV-11 Ser capaz de realizar especificaciones formales de los resultados esperados de un programa CG7 A
RA-AV-12 Comprender, al nivel del usuario, las técnicas de demostración automáticas más utilizadas en las herramientas de verificación de programas CEM1, CG13 C
RA-AV-91 Familiaridad de los requisitos de diseño e implementación CEM5 P
RA-AV-92 Familiaridad con diversas técnicas de desarrollo formal de software CEM4 P
RA-AV-93 Conocimiento de lenguajes que facilitan la aplicación de las técnicas antedichas CEM4, CG7 C
RA-AV-94 Uso efectivo de técnicas de construcción rigurosa de software CEM4 P
RA-AV-96 Familiaridad de la formalización de la sintaxis de lenguajes de programación CG7 P
RA-AV-97 Familiaridad de la formalización de la semántica de lenguajes de programación CG7 C
RA-AV-98 Habilidad para razonar sobre la recursividad y realizar pruebas por inducción CG13 A


Guía de Aprendizaje

Guía de aprendizaje: Diseño de Sistemas Correctos por Construcción