Metodi formali

A.A. 2020/2021
6
Crediti massimi
48
Ore totali
SSD
INF/01
Lingua
Italiano
Obiettivi formativi
L'insegnamento intende esplorare le tecniche formali per migliorare l'affidabilità del software, con un focus particolare sulla specifica e dimostrazione di proprietà del software. Gli strumenti scelti sono i model checker simbolici e la della dimostrazione assistita dal calcolatore.
Risultati apprendimento attesi
Lo studente sarà in grado di modellare e dimostrare la correttezza di semplici proprietà del software usando un insieme di tools presentati nelle ore di laboratorio.
Programma e organizzazione didattica

Edizione unica

Responsabile
Periodo
Primo semestre
Parte A
Metodi didattici:
Lezioni a distanza in modalità sincrona con Microsoft Teams, basate su slides, scrivendo su tavoletta quello che non c'è nelle slides per rispondere a domande; saranno assegnati esercizi da svolgere in simultanea col PC. Gli studenti dovranno essere pronti a partecipare attivamente alle lezioni negli orari stabiliti, con un PC su cui sia installato il software del corso

Materiali di riferimento:
Il programma e il materiale di riferimento non subiranno variazioni

Modalità di verifica dell'apprendimento: esame scritto finale in presenza

Parte B

Metodi didattici:
le lezioni verranno effettuate in modalità sincrona con la piattaforma Teams durante l'orario previsto. Verranno registrate e rese disponibili per la durata del semestre.

Materiali di riferimento:
Il programma e il materiale di riferimento non subiranno variazioni
.
Modalità di verifica dell'apprendimento:
ogni 3/4 lezioni verrà effettuata una prova in itinere via Teams/Zoom. Come prova finale è prevista (se possibile) un breve esame scritto in presenza e un semplice progetto/presentazione in gruppi di due. Queste modalità sono soggette a cambiamento a seconda del numero di studenti e della situazione contingente.
Programma
il corso è suddiviso in due tronconi paralleli che affrontano diverse tematiche legate alla verifica formale

Parte A: Model Checking e Logiche Temporali

· Motivazioni: il model-checking come strumento totalmente automatico per la verifica del comportamento di sistemi reattivi e concorrenti.
· La logiche temporali LTL e CTL: sintassi e semantica, confronto di espressività, assiomatizzazione (cenni), forme normali negative.
· Model-checking: introduzione al problema con esempi tratti dai corsi di sistemi operativi e reti (mutua esclusione, produttore/consumatore, cena dei filosofi, ecc.).
· Automi su parole infinite: automi di Buchi e linguaggi omega-regolari, automi vuoti e chiusura booleana.
· Soddisfacibilità e model-checking esplicito in LTL: insiemi di Hintikka, formule e automi, tableaux per LTL.
· Punti fissi di operatori monotoni: teorema di Knaster-Tarski, applicazione agli operatori di CTL.
· Model-checking simbolico in CTL: macchine a stati finiti, OBDD (`ordered binary decision diagrams'), simulazione simbolica dell'approssimazione dei punti fissi.
· Model-checking limitato: la riduzione a SAT e l'utilizzo dei SAT-solver nel model-checking.
· Model-checking per sistemi a stati infiniti: well-structured systems e algoritmi di raggiungibilità a ritroso; la tecnica del modello approssimato e il modello `stopping failures';
· Model-checking per sistemi a stati infiniti: sviluppi recenti per un approccio dichiarativo tramite SMT-solvers.; array-based systems; esempi tratti da protocolli di mutua esclusione, protocolli di cache coherence, canali con perdita di informazione, fault-tolerant systems, automi temporizzati parametrici.
· Supporto software: introduzione alla sintassi dei sistemi NuSMV (per sistemi a stati finiti) e MCMT (per sistemi a stati infiniti).

Parte B:
In questa parte esploreremo delle tecniche formali per migliorare
l'affidabilità del software, concentrandoci in particolare sulla
specifica e dimostrazione di proprietà del software.

La particolarità di questa parte è di essere costruita interamente
all'interno di Coq, uno dei proof assistant (p.a.) più maturi ed
usati. Un p.a. è uno esempio di dimostratore di teoremi interattivo,
che cioè automatizza gli aspetti più di routine della dimostrazione ma
dipende dall'utente per la strategia dimostrativa. Il corso,
esercizi ed esame compresi, va quindi (e)seguito come una sessione
interattiva con il sistema.
(http://www.seas.upenn.edu/~cis500/current/sf/index.html)

Gli argomenti principali che svilupperemo saranno:

(1) (Ri)esame di alcuni strumenti basi logici per la specifica e
dimostrazione delle proprietà di interesse (induzione, ricorsione,
riscrittura).

(2) Uso dei p.a. nella costruzione di argomenti logici rigorosi.

(3) La programmazione funzionale sia come metodologia di
programmazione che come ponte con la logica.

(4) Tecniche formali per il ragionamenti sulle proprietà di programmi
specifici (terminazione di un loop, dimostrazione che una funzione di
sorting soddisfa la sua specifica) e

(5) per la dimostrazione di proprietà di tutti i programmi di un certo
linguaggio, attraverso l'uso di sistemi di tipi.
Prerequisiti
E' richiesta la conoscienza di nozioni basi di logica, meglio se superando l'esame di logica magistrale.
Metodi didattici
Lezioni frontali e laboratorio (online)
Materiale di riferimento
Sito web:

https://amomiglianol2.ariel.ctu.unimi.it/v5/home/Default.aspx

Parte A:
dispense disponibili sul sito del corso;
- Clarke, Grumberg, Peled, Model Checking, MIT Press, 2000.
- materiali vari disponibili sui siti di NuSMV e MCMT.

Parte B:
Una selezione dei quattro volumi a: https://softwarefoundations.cis.upenn.edu/
Modalità di verifica dell’apprendimento e criteri di valutazione
L'esame (valutato in trentesimi) si divide in due parti, corrispondenti alle due parti in cui è diviso il corso.
Per entrambe le parti sono previste due modalità:
- progetto/tesina di approfondimento su un argomento concordato col docente
- prova di laboratorio, in cui si usano gli strumenti software spiegati a lezione e nelle esercitazioni.
INF/01 - INFORMATICA - CFU: 6
Lezioni: 48 ore
Siti didattici
Docente/i
Ricevimento:
venerdì alle 11,30
Dipartimento di Matematica, via C. Saldini 50
Ricevimento:
Venerdì, 16:30 --18
4009, Celoria 18