Mission and Goals

The goal of this course is to present the state-of-the-art techniques and tools for the automated formal verification of real-time systems, in particular those requiring a continuous notion of time. These techniques are especially useful for the formal analysis of sfatey-critical embedded and cyber-physical systems.
The course provides the theoretical foundations of the formal verification of real-time systems, and demonstrates some of the state-of-the-art tools in this field.

Syllabus

Automata-based approaches:

1. Timed Automata: definition, properties, model checking

2. The Uppaal tool

3. Variants of Timed Automata

Logic-based approaches

1. MTL (and variants) over continuous time: definitions, properties

2. Constraint LTL over clocks: definitions, properties, satisfiability checking

3. Automated satisfiability checking of MTL: the Zot tool

4. Automated verification of Timed Automata with MITL: the TACK tool

5. Automated monitoring of MTL variants and extensions

Beyond Timed Automata

Intended learning outcomes:

After successful completion of the course, the students will:

1. know the main theoretical means for modeling a real-time system and its properties

2. know different classes of logics for capturing continuous time behaviors

3. learn how to interpret logic formulae over dense time behaviors

4. extend the vocabulary required to understand technical papers and reports in the area of Formal verification

5. learn various state-of-the-art tools supporting formal verification of real-time systems

Teachers: Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro, 

Each student will be asked to study and report on a scientific work related to the topics of the course.

February 3,5,7 (9:00-12:30): Automata-based approaches

February 10,12,14 (9:00-12:30): Logic-based approaches

March 2,4 (9:00-11:00): Final evaluation