logo-polimi
Loading...
Risorse bibliografiche
Risorsa bibliografica obbligatoria
Risorsa bibliografica facoltativa
Scheda Riassuntiva
Anno Accademico 2019/2020
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
  • Theory and practice of specification and verification of real-time systems,with particular focus on transition systems, timed automata, model checking and temporal logic;
  • Hoare’s method for program specification and verification;

Prerequisiti

It is assumed a basic knowledge of Software Engineering (sw life cycle, requirements specification, verification and validation) and  of Theoretical Computer Science (automata and formal languages, computability, computational complexity, mathematical logic).


Modalità di valutazione

Students are expected to give a public presentation of a paper or of a tool, on the topics of the course, to be discussed with the instructor and other students.

The presentation can be prepared in groups of 1-3 students.   

Additionally, a 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.

Students who cannot give the presentation or prepare the homework, will have to give an oral exam. 

The oral will deal with theory and exercises ob the topics of the course.  


Bibliografia
Risorsa bibliografica obbligatoriaChristel Baier, Joost-Pieter Katoen, Kim G. Larsen, Principles of Model Checking, Editore: Mit Press, Anno edizione: 2008, ISBN: 978-0262026499
Note:

Main reference book. It covers model checking and timed automata. Chapters 1-7 and 9.

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).

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
Note:

Additional material in temporal logic and automata.


Forme didattiche
Tipo Forma Didattica Ore di attività svolte in aula
(hh:mm)
Ore di studio autonome
(hh:mm)
Lezione
32:00
48:00
Esercitazione
9:00
13:30
Laboratorio Informatico
0:00
0:00
Laboratorio Sperimentale
0:00
0:00
Laboratorio Di Progetto
9:00
13:30
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
08/12/2019