Máster Universitario en Software y Sistemas

Métodos Formales para Sistemas Concurrentes y Reactivos

Profesor (Coordinador):
Manuel Carro
mcarro@fi.upm.es
Profesor:
César Sánchez
Cesar.sanchez@imdea.org

Semestre

Segundo semestre

Créditos

4 ECTS

Objetivos

Programa

  1. Antecedentes
    1. Autómatas
    2. Decidibilidad
    3. Complejidad
    4. Lógicas (sintaxis y semántica)
    5. Procedimientos de decisión
  2. Modelos y semántica de sistemas reactivos
    1. Sistemas de transición de estados
    2. Espacios de estados finitos vs. infinitos
    3. No determinismo
    4. Concurrencia
    5. Sincronía vs. asincronía
    6. Seguridad vs. vivacidad
    7. Refinamiento
    8. Sistemas en tiempo real y híbridos
    9. Sistemas abiertos
    10. Lenguajes de especificación
    11. Lógicas temporales
  3. Algoritmos de verificación
    1. Comprobación de modelos mediante lógica temporal
    2. Teoría de autómatas omega
    3. Juegos
    4. Alcanzabilidad
    5. Explosión de estados
  4. Técnicas de verificación
    1. Deductivas vs. algorítmicas
    2. Comprobación simbólica de modelos
    3. Métodos de reducción del espacio de estados
    4. Razonamiento composicional y jerárquico
    5. Sobreaproximación, subaproximación y refinamiento

Web de la Asignatura

http://www.software.imdea.org/graduateschool

Prerrequisitos

Método de Evaluación

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 inforamció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 S
RA-AV-4 Conocimiento de técnicas de demostración de corrección de código. CEM1,CEM5 A

Guía de Aprendizaje

Guía de aprendizaje de la asignatura: Métodos Formales para Sistemas Concurrentes y Reactivos