Master in Software and Systems

Formal Methods for Concurrent and Reactive Systems

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

Semester

Second semester

Credits

4 ECTS

Outline

Reactive systems, such as concurrent programs, communication protocols and control systems, are characterized by their non-terminating behavior and their persistent interaction with their environment. This course introduces the theory and practice of formal methods for the design and analysis of reactive systems. The emphasis is on the underlying logical and automata-theoretic concepts, the algorithmic solutions, and heuristics to cope with the high computational complexity.

Learning Goals

Syllabus

  1. Background
    1. Automata
    2. Decidability
    3. Complexity
    4. Logics (syntax and semantics)
    5. Decision Procedures
  2. Models and semantics of reactive systems
    1. State transition systems
    2. Finite vs infinite state spaces
    3. Non-determinism
    4. Concurrency
    5. Synchrony vs. asynchrony
    6. Safety vs. liveness
    7. Refinement
    8. Real-time and hybrid systems
    9. Open systems
    10. Specification languages
    11. Temporal logics
  3. Verification algorithms
    1. Temporal logic model checking
    2. Theory of omega automata
    3. Games
    4. Reachability
    5. State explosion
  4. Verification techniques
    1. Deductive vs. algorithmic techniques
    2. Symbolic model checking
    3. State space reduction methods
    4. Compositional and hierarchical reasoning
    5. Over-approximation, under-approximation and refinement

Website

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

Prerequisites

Assessment Method

Tuition Language

English

Subject-Specific Competences

More information:

This table shows the code, description and proficiency level for each subject-specific competence

Code Competence Proficiency Level
SSC1 Examination of the state of the art to identify research problems related to the design, construction, use and evaluation of complex software-intensive sociotechnical systems S
SSC5 Contribution of solutions to open problems related to software verification and validation applications and methods, techniques and tools A

Learning Outcomes

More information:

This table shows the code, description and proficiency level for each subject learning outcome

Code Learning Outcome Associated competences Proficiency level
RA-AV-1 Familiarity with the idea of design and implementation requirement SSC1,SSC5 S
RA-AV-4 Knowledge of techniques for proving code correctness SSC1,SSC5 A

Learning Guide

Subject learning guide for Formal Methods for Concurrent and Reactive Systems