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
- Introducción a los métodos formales: pruebas de corrección de programas
- Fundamentos: especificación, lógica de primer orden, pruebas, programas
- Fundamentos de Event-B; la herramienta Rodin
- Sistemas secuenciales
- Event-B: fundamentos matemáticos y sus aplicaciones
- Sistemas reactivos: concurrencia y distribución
- De la deducción automática a la programación con lógica
- Semántica y características avanzadas
- 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 | 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 | 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