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
  7. De la deducción automática a la programación con lógica
  8. Semántica y características avanzadas
  9. CLP y verificación mediante interpretación abstracta

Bibliografía

  • Notas de clase de Lawrence Paulson
  • Logic in Computer Science (Huth & Ryan)
  • http://wiki.event-b.org/ - el sitio central de Event-B
  • Modeling in Event-B: System and Software Engineering. Jean-Raymond Abrial. Cambridge University Press.
  • https://ciao-lang.org/ - sitio web del sistema Ciao
  • An overview of Ciao and its design philosophy - a description of the design principles behind the Ciao Prolog system (Hermenegildo, Bueno, Carro, López-García, Mera, Morales, Puebla)

Prerrequisitos:

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

Método de Evaluación

Dependiendo del número de estudiantes, se optará por:

  • Hasta cinco ejercicios / prácticas individuales que valgan el 60% de la nota final y un proyecto de curso a realizar en grupos y presentado al resto de la clase que valga el restante 40%
  • Hasta cinco ejercicios / prácticas individuales que valgan el 60% de la nota final y un examen individual que valga el restante 40% de la nota final

Aula

A-6306

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
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-1 Familiaridad con la idea de requisito de diseño y de implementación. CEM1, CEM5 P
RA-AV-2 Familiaridad con diversas técnicas de desarrollo formal. CEM1, CEM5 C
RA-AV-3 Conocimiento de varios lenguajes que facilitan la aplicación de las técnicas antedichas. CEM1, CEM5 A
RA-AV-4 Conocimiento de técnicas de demostración de corrección de código. CEM1, CEM5 A
RA-AV-5 Uso efectivo de técnicas de construcción rigurosa de software. CEM1, CEM5 P


Guía de Aprendizaje

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