logo-polimi
Loading...
Risorse bibliografiche
Risorsa bibliografica obbligatoria
Risorsa bibliografica facoltativa
Scheda Riassuntiva
Anno Accademico 2019/2020
Tipo incarico Dottorato
Insegnamento 055042 - AUTOMATED VERIFICATION AND MONITORING OF TIMED SYSTEMS
Docente Bersani Marcello Maria
Cfu 5.00 Tipo insegnamento Monodisciplinare

Corso di Dottorato Da (compreso) A (escluso) Insegnamento
MI (1380) - INGEGNERIA DELL'INFORMAZIONE / INFORMATION TECHNOLOGYAZZZZ055042 - AUTOMATED VERIFICATION AND MONITORING OF TIMED SYSTEMS
055207 - AUTOMATED VERIFICATION AND MONITORING OF TIMED SYSTEMS

Programma dettagliato e risultati di apprendimento attesi

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, 


Note Sulla Modalità di valutazione

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


Intervallo di svolgimento dell'attività didattica
Data inizio
Data termine

Calendario testuale dell'attività didattica

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


Bibliografia
Risorsa bibliografica facoltativaC. Baier, J.P. Katoen, Principles of Model Checking, Editore: MIT press, Anno edizione: 2008
Risorsa bibliografica facoltativaM. Bersani, M. Rossi, P. San Pietro, An SMT-based Approach to Satisfiability Checking of MITL, Information and Computation, Editore: Elsevier, Anno edizione: 2015 http://dx.doi.org/10.1007/s00236-015-0229-y
Risorsa bibliografica facoltativaM. Bersani, M. Rossi, P. San Pietro, A tool for deciding the satisfiability of continuous-time metric temporal logic, Acta Informatica, Editore: Springer, Anno edizione: 2015 http://dx.doi.org/10.1007/s00236-015-0229-y
Risorsa bibliografica facoltativaC. A. Furia, D. Mandrioli, A. Morzenti, M. Rossi, Modeling Time in Computing, Editore: Springer, Anno edizione: 2012

Mix Forme Didattiche
Tipo Forma Didattica Ore didattiche
lezione
25.0
esercitazione
0.0
laboratorio informatico
0.0
laboratorio sperimentale
0.0
progetto
0.0
laboratorio di progetto
0.0

Informazioni in lingua inglese a supporto dell'internazionalizzazione
Insegnamento erogato in lingua Inglese

Note Docente
schedaincarico v. 1.6.1 / 1.6.1
Area Servizi ICT
18/02/2020