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.

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