logo-polimi
Loading...
Risorse bibliografiche
Risorsa bibliografica obbligatoria
Risorsa bibliografica facoltativa
Scheda Riassuntiva
Anno Accademico 2018/2019
Scuola Scuola di Ingegneria Industriale e dell'Informazione
Insegnamento 088882 - FORMAL METHODS FOR CONCURRENT AND REAL-TIME SYSTEMS (UIC 545)
Docente San Pietro Pierluigi
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 (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)

Obiettivi dell'insegnamento

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. 


Risultati di apprendimento attesi

 

Dublin Descriptors

Expected learning outcomes

Knowledge and understanding

Students will learn the principles and paradigms that guide the specification, design and verification of modern real-time, safety-critical systems.

Applying knowledge and understanding

At the end of the course students will be able to identify the critical issues in real-time systems design, and to apply the specification and verification techniques they learnt to solve them.

Making judgements

At the end of the course students will be able to evaluate and compare the various alternatives in specifying and verifying a distributed system.

Communication

Students will learn how to describe important topics in the filed, including recent scienftific research, and how to present their own results.

Learning skills

At the end of the course students will be able to autonomously learn new specification and verification techniques, together with selecting and using new verification toolkits. 

 


Argomenti trattati
  • Hoare’s method for program specification and verification;
  • theory and practice of specification and verification of real-time systems,with particular focus on timed automata, model checking and temporal logic;
  • case studies based on industrial projects.

Prerequisiti

It is assumed a basic knowledge of the topics covered by the course Theoretical computer science or by the course "Algoritmi e principi dell'Informatica" (Algorithms and Principles of Computer Science): automata and formal language theory, computability, computational complexity, mathematical logic.


Modalità di valutazione

There will be a public presentation of a homework, to be discussed with the instructor and other students.

The homework will be assigned to be completed either individually or, preferably, in small groups. The final score will be given in 30ths for the Politecnico and in American grades (A through D), for the students who participate to the Politecnico-UIC program.

UIC students must complete the exam within June, but it is suggested the same also for the other students.


Bibliografia
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 facoltativaFuria, C.A., Mandrioli, D., Morzenti, A., Rossi, M., Modeling Time in Computing, Editore: Springer, Anno edizione: 2012, ISBN: 978-3-642-32332-4
Risorsa bibliografica facoltativaChristel Baier, Joost-Pieter Katoen, Kim G. Larsen, Principles of Model Checking, Editore: Mit Press, Anno edizione: 2008, ISBN: 978-0262026499
Note:

It covers model checking and timed automata

Risorsa bibliografica facoltativaDino Mandrioli, Carlo Ghezzi, Theoretical foundations of Computer Science, Editore: Wiley, Anno edizione: 1993, ISBN: 978-0894647987
Note:

It covers Hoare Logic to prove program correctness (Chapter 5 only).


Forme didattiche
Tipo Forma Didattica Ore di attività svolte in aula
(hh:mm)
Ore di studio autonome
(hh:mm)
Lezione
32:30
48:45
Esercitazione
17:30
26:15
Laboratorio Informatico
0:00
0:00
Laboratorio Sperimentale
0:00
0:00
Laboratorio Di Progetto
0:00
0:00
Totale 50:00 75:00

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
18/02/2020