Metodi formali

A.A. 2019/2020
Insegnamento per
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.
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.

Struttura insegnamento e programma

Edizione attiva
Responsabile
INF/01 - INFORMATICA - CFU: 6
Lezioni: 48 ore
STUDENTI FREQUENTANTI
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.
Informazioni sul programma
Consultare i siti:

- http://users.mat.unimi.it/users/ghilardi/didattica/logica2.html per la prima parte del corso

- Ariel (metodi formali)
Propedeuticità
logica matematica
Prerequisiti e modalità di esame
L'esame 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.
Metodi didattici
Prima parte:
- lezioni frontali
- esercitazioni in laboratorio col il software illustrato a lezione.

Seconda parte:
- lezioni frontali
- esercitazioni in laboratorio con Coq
Materiale didattico e bibliografia
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
- Ivan Bratko:PROLOG Programming for Artificial Intelligence, 4th edition, Addison-Wesley, 2012.
STUDENTI NON FREQUENTANTI
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 modalità di esame
L'esame 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.
Materiale didattico e bibliografia
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
- Ivan Bratko:PROLOG Programming for Artificial Intelligence, 4th edition, Addison-Wesley, 2012.
Periodo
Primo semestre
Periodo
Primo semestre
Modalità di valutazione
Esame
Giudizio di valutazione
voto verbalizzato in trentesimi
Siti didattici
Docente/i
Ricevimento:
venerdì alle 11,30
Dipartimento di Matematica, via C. Saldini 50
Ricevimento:
venerdì 14.30--16
4009