logo-polimi
Loading...
Risorse bibliografiche
Risorsa bibliografica obbligatoria
Risorsa bibliografica facoltativa
Scheda Riassuntiva
Anno Accademico 2014/2015
Scuola Scuola di Ingegneria Industriale e dell'Informazione
Insegnamento 088882 - FORMAL METHODS FOR CONCURRENT AND REAL-TIME SYSTEMS (UIC 545)
Docente Mandrioli Dino
Cfu 5.00 Tipo insegnamento Monodisciplinare

Corso di Studi Codice Piano di Studio preventivamente approvato Da (compreso) A (escluso) Insegnamento
Ing Ind - Inf (Mag.)(ord. 270) - MI (434) INGEGNERIA INFORMATICA* AZZZZ088882 - FORMAL METHODS FOR CONCURRENT AND REAL-TIME SYSTEMS (UIC 545)
Ing Ind - Inf (Mag.)(ord. 270) - MI (436) INGEGNERIA DELL'AUTOMAZIONE* AZZZZ088882 - FORMAL METHODS FOR CONCURRENT AND REAL-TIME SYSTEMS (UIC 545)
Ing Ind - Inf (Mag.)(ord. 270) - MI (473) AUTOMATION AND CONTROL ENGINEERING - INGEGNERIA DELL'AUTOMAZIONE* AZZZZ088882 - FORMAL METHODS FOR CONCURRENT AND REAL-TIME SYSTEMS (UIC 545)
Ing Ind - Inf (Mag.)(ord. 270) - MI (481) COMPUTER SCIENCE AND ENGINEERING - INGEGNERIA INFORMATICA* AZZZZ088882 - FORMAL METHODS FOR CONCURRENT AND REAL-TIME SYSTEMS (UIC 545)

Programma dettagliato e risultati di apprendimento attesi

Obiettivo del corso
Il corso ha lo scopo di fornire capacità nell’analisi, il progetto e la verifica di sistemi critici (con particolare attenzione ai sistemi in tempo reale), sfruttando metodi formali.

Gli argomenti principali trattati nel corso sono:

Il metodo di Hoare per la specifica e verifica del software.

Linguaggi e modelli per la specifica di sistemi in tempo reale, con particolare riferimento alle reti di Petri temporizzate e alla logica temporale.

Analisi e prove di proprietà di sistemi safety-critical.

Studi di caso basati su progetti industriali.
Prerequisiti
Il programma del corso assume la conoscenza degli argomenti trattati negli insegnamenti di Informatica Teorica (oppure di Algoritmi e principi dell'Informatica) e di Algebra e Logica Matematica.

 

 

 

Formal methods for concurrent and real-time systems

Course description

The goal of the course is to develop skills in the analysis, design, and verification of critical systems (with particular emphasis on real-time aspects), by exploiting formal methods.
The main topics are: Hoare’s method for program specification and verification; specification languages for real-time systems, with particular focus on timed Petri nets and temporal logic; case studies based on industrial projects.
Prerequisites
It is assumed a basic knowledge of the topics covered by the course "Informatica teorica" (Theoretical computer science) or by the course "Algoritmi e principi dell'Infromatica" (Algorithms and Principles of Computer Science): automata and formal language theory, computability, computational complexity, mathematical logic.


Note Sulla Modalità di valutazione

Verranno svolte una o due prove in itinere durante il corso. Verrà inoltre assegnato un progetto da svolgere come "homework" individualmente o preferibilmente in piccoli gruppi. La sintesi delle varie prove formerà il giudizio finale.

There will be one or two midterm tests. Furthermore, a homework will be assigned to be completed either individually or, preferably, in small groups. The integration of the evaluations of midterm tests and of the homework will produce the final score, which will be given both in 30ths, for the Politecnico, and in American grades (A through D), for the students who participate to the Politecnico-UIC program (see the Teacher's notes below).


Bibliografia
Risorsa bibliografica obbligatoriaDino Mandrioli, Carlo Ghezzi, Theoretical Foundations of Computer Science, Editore: John Wiley & Sons, Anno edizione: 1987
Risorsa bibliografica obbligatoriaEmanuele Ciapessoni, Alberto Coen-Porisini, Ernani Crivelli, Dino Mandrioli, Piergiorgio Mirandola, Angelo Morzenti, From formal models to formally-based methods: an industrial experience, Editore: ACM, Anno edizione: 1999, Fascicolo: TOSEM, Vol. 8, N.1 Disponibile in http://home.dei.polimi.it/mandriol/Didattica/sitofms.html
Risorsa bibliografica obbligatoriaHeitmeyer C., Mandrioli D., Formal Methods for Real-Time Computing, Editore: JohnWiley, Anno edizione: 1996 Disponibile in http://home.dei.polimi.it/mandriol/Didattica/sitofms.html
Risorsa bibliografica obbligatoriaFelder M., Mandrioli D., Morzenti A, Proving Properties of Real-Time Systems through Logical Specifications and Petri Net Models, Editore: IEEE, Anno edizione: 1994, Fascicolo: 2 Disponibile in http://home.dei.polimi.it/mandriol/Didattica/sitofms.html
Risorsa bibliografica facoltativaFuria, C.A., Mandrioli, D., Morzenti, A., Rossi, M., Modeling Time in Computing, Editore: Springer, Anno edizione: 2012, ISBN: 978-3-642-32332-4

Mix Forme Didattiche
Tipo Forma Didattica Ore didattiche
lezione
30.0
esercitazione
20.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
schedaincarico v. 1.6.1 / 1.6.1
Area Servizi ICT
08/12/2019