logo-polimi
Loading...
Risorse bibliografiche
Risorsa bibliografica obbligatoria
Risorsa bibliografica facoltativa
Scheda Riassuntiva
Anno Accademico 2015/2016
Tipo incarico Dottorato
Insegnamento 098887 - AUTOMATED VERIFICATION OF TIMED SYSTEMS
Docente Rossi Matteo Giovanni
Cfu 5.00 Tipo insegnamento Monodisciplinare

Corso di Dottorato Da (compreso) A (escluso) Insegnamento
MI (1380) - INGEGNERIA DELL'INFORMAZIONE / INFORMATION TECHNOLOGYAZZZZ098887 - AUTOMATED VERIFICATION 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:

  • Timed Automata: definition, properties, model checking
  • The Uppaal tool
  • Variants of Timed Automata

Logic-based approaches

  • MTL (and variants) over continuous time: definitions, properties
  • Constraint LTL over clocks: definitions, properties, satisfiability checking
  • Automated satisfiability checking of MTL: the Zot tool

Beyond Timed Automata

 

Teachers: Matteo Rossi, Pierluigi San Pietro, Marcello Bersani 


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
 

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
28.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
Disponibilità di materiale didattico/slides in lingua inglese
Disponibilità di libri di testo/bibliografia in lingua inglese
Possibilità di sostenere l'esame in lingua inglese
Disponibilità di supporto didattico in lingua inglese

Note Docente
Tentative schedule: Mon., Feb. 22nd, 9-13; Wed., Feb. 24th, 9-13; Fri., Feb. 26th, 9-13; Mon., Feb. 29th, 9-13; Wed., Mar. 2nd, 9-13; Fri., Mar. 4th, 9-13; Fri., Mar. 18th, 9-13
schedaincarico v. 1.6.6 / 1.6.6
Area Servizi ICT
29/07/2021