Strumenti Utente

Strumenti Sito


magistraleinformatica:mvs:start

Metodi per la Verifica del Software (A.A. 2012/13)


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 N1 B

Ricevimento: su appuntamento via email (andrea [at] di [dot] unipi [dot] it)

Materiale Didattico

  • Slide delle lezioni, che verranno pubblicate di volta in volta.
  • Christel Baier, Joost Peter Katoen, Principles of Model Checking, MIT Press, 2008
  • Mordechai Ben-Ari, Principles of the Spin Model Checker, Springer, 2008

Lezioni

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. 29Esercizi 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 PROMELAmvs-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

Anni precedenti

magistraleinformatica/mvs/start.txt · Ultima modifica: 23/05/2013 alle 16:39 (4 anni fa) da Andrea Corradini