Máster Universitario en Software y Sistemas

Desarrollo Riguroso de Software

Profesor (Coordinador):
Manuel Carro
mcarro@fi.upm.es
Profesor:
Julio Mariño
jmarino@fi.upm.es

Semestre

Primer semestre

Créditos

4 ECTS

Resumen

El Software se está volviendo paulatinamente más y más complejo y se está ocupando de controlar tareas críticas. Por tanto, cualquier tecnología que se dirija a asegurar la fiabilidad y calidad del mismo se va a convertir en más y más relevante.

Hay muchos modos de aproximarse a la consecución de ese objetivo. El enfoque declarativo se basa en el uso de lenguajes y lógicas con un sólido fundamento matemático. Esto incluye los lenguajes de especificación (VDB, Z, OBJ, B...), los lenguajes de programación funcional (Haskell, Erlang, cálculo lambda...) y los lenguajes lógicos (Prolog, CLP...).

Objetivos

Programa

  1. Introducción
    1. Visión global, motivación y retos del desarrollo rigoroso del software
    2. Repaso de los antecedentes: lógica formal, pruebas...
  2. Corrección por construcción
    1. Event-B: Teoría y métodos de desarrollo.
    2. Event-B: la herramienta Rodin
  3. Verificación
    1. Verificación clásica de programas
    2. La herramienta Dafny
    3. La herramienta Alloy
  4. Especificaciones
    1. Especificaciones algebraicas
    2. El lenguaje de especificación algebraica Maude

Bibliografía

Página Web

http://lml.ls.fi.upm.es/rsd/

Prerrequisitos:

Método de Evaluación

Según el número de alumnos, se obtendrán la nota final a partir de:

En su conjunto, los ejercicios de cada una de las unidades tendrán el mismo peso relativo en la nota final, aunque cada ejercicio individual de la unidad puede tener asociado un peso distinto.

Idioma en que se imparte

Inglés.

Competencias Específicas

Más información:

Esta tabla muestra el código, la descripción y el 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

Más información:

Esta tabla muestra cada el código, la descripción, las competencias asociadas y el 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 de la asignatura: Desarrollo Riguroso de Software