Attenzione: Il corso di MVS non sarà erogato nell'Anno Accademico 2013/14, ma sarà erogato regolarmente nell'A.A. 2014/15.
Docente: Andrea Corradini
| Corso | Giorno | Ora | Aula |
|---|---|---|---|
| Lezione | Martedì | 14-16 | C |
| Lezione | Giovedì | 14-16 | |
Ricevimento: su appuntamento via email (andrea [at] di [dot] unipi [dot] it)
| N | Data | Argomento | Slide | Altro |
|---|---|---|---|---|
| 1 | 19-02-2013 | Introduzione al corso | lec1.pdf | Schema Model Checking |
| 2 | 21-02-2013 | Sistemi di transizione, Program graphs | lec2.pdf | Def. Transition System, TS per Circuiti Sequenziali, Def. Program Graph, Semantica TS di Program Graphs, Sintassi di GCL |
| 3 | 28-02-2013 | Composizione parallela di sistemi, Channel systems | lec3.pdf, lec4.pdf fino a pag. 51 | Def. Interleaving di TS, Mutua esclusione con semaforo, Algoritmo di Peterson, Message-passing sincrono, Def. Channel System, Regole SOS per message-passing asincrono, Regole SOS per message-passing sincrono |
| 4 | 5-03-2013 | Alternating Bit Protocol, Composizione sincrona | lec4.pdf | Esercizi proposti |
| 5 | 12-03-2013 | Proprietà Linear Time | lec5.pdf fino a pag. 159 | |
| 6 | 14-03-2013 | Invariant and Safety Properties | lec5.pdf e lec6-safety.pdf | |
| 7 | 19-03-2013 | Liveness Properties | lec7.pdf fino a pag. 44 | |
| 8 | 21-03-2013 | Fairness | lec7.pdf | |
| 9 | 26-03-2013 | Model Checking Regular Safety Properties | lec08.pdf | |
| 10 | 28-03-2013 | Omega Regular Properties | lec09_10.pdf fino a pag. 179 | Esercizi proposti |
| 11 | 9-04-2013 | Generalized Büchi Automata, Model Checking with Büchi Automata | lec09_10.pdf, lec11.pdf | |
| 12 | 11-04-2013 | Linear Time Logic | lec12_13.pdf fino a pag. 242 (escluso Fairness) | |
| 13 | 16-04-2013 | Esercitazione | Correzione esercizi del 28-03-2013 | |
| 14 | 18-04-2013 | SPIN: Introduzione all'ambiente e PROMELA | mvs-spin-01.pdf, mvs-spin-02.pdf fino a pag. 24 | |
| 15 | 23-04-2013 | Fairness e LTL; SPIN: Introduzione all'ambiente e PROMELA | lec12_13.pdf, mvs-spin-02.pdf fino a pag. 29 | Esercizi suggeriti su SPIN/PROMELA: http://spinroot.com/spin/Man/Exercises.html |
| 16 | 30-04-2013 | LTL Model Checking | lec14_15.pdf, escluso dimostrazione finale | |
| 17 | 2-05-2013 | SPIN: Costrutti di controllo di PROMELA | mvs-spin-02.pdf, mvs-spin-03.pdf | |
| 18 | 7-05-2013 | Complessità di LTL model checking | lec16.pdf | |
| 19 | 9-05-2013 | Specifica di proprietà in PROMELA: asserzioni, end/progress/accept states, never claims | mvs-spin-04.pdf, mvs-spin-2013-05.pdf fino a pag. 11 | |
| 20 | 14-05-2013 | PROMELA: cenni su trace/notrace assertions, temporal logic patterns, LTL vs ω-regular expressions, semantica operazionale, algoritmi di ricerca, complessità | mvs-spin-2013-05.pdf, mvs-spin-2013-06.pdf | Semantica operazionale di Promela: caltech14.pdf. NB: aggiunti lucidi con nuova sintassi per LTL, da Spin v6, e possibilità di inserire formule LTL inline, senza generare never-claims (vedi MVS-05 p. 17, 18 e 25) |
| 21 | 16-05-2013 | Esercitazione su PROMELA e SPIN | ||
| 22 | 21-05-2013 | Lezione di Alberto Lluch Lafuente | mvs-spin-2013-07-optimization.pdf | Lucidi di Holzmann su Model Extraction da C code caltech18.ppt. http://spinroot.com/modex/ |
| 23 | 23-05-2013 | Overview su CTL e CTL*, Presentazione progetto | lec17-ctl-ctlstar-summary-2013.pdf |