Ing Ind - Inf (Mag.)(ord. 270) - MI (473) AUTOMATION AND CONTROL ENGINEERING - INGEGNERIA DELL'AUTOMAZIONE
*
A
ZZZZ
088882 - FORMAL METHODS FOR CONCURRENT AND REAL-TIME SYSTEMS (UIC 545)
Ing Ind - Inf (Mag.)(ord. 270) - MI (481) COMPUTER SCIENCE AND ENGINEERING - INGEGNERIA INFORMATICA
*
A
ZZZZ
088882 - 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
Heitmeyer C., Mandrioli D., Formal Methods for Real-Time Computing, Editore: JohnWiley, Anno edizione: 1996 Disponibile in http://home.dei.polimi.it/mandriol/Didattica/sitofms.htmlFuria, C.A., Mandrioli, D., Morzenti, A., Rossi, M., Modeling Time in Computing, Editore: Springer, Anno edizione: 2012, ISBN: 978-3-642-32332-4
Christel 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
Dino 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
Inglese