Metodi per la Verifica del Software (A.A. 2010/11)

Docenti: Andrea Corradini, GianLuigi Ferrari

Corso	Giorno	Ora	Aula
Lezione (per recuperi)	Lunedì	17-19	L1
Lezione	Mercoledì	9-11	L1
Lezione	Giovedì	16-18	F1

Ricevimento: su appuntamento via email (andrea [at] di [dot] unipi [dot] it, giangi [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
1	14-03-2011	Introduzione al corso	lec1.pdf
2	16-03-2011	Sistemi di transizione, Program graphs	lec2.pdf
3	23-03-2011	Composizione parallela di sistemi	lec3.pdf e lec4.pdf, fino a pag 51
4	24-03-2011	Channel systems, Composizione sincrona; Proprietà Linear Time	lec4.pdf e lec5.pdf, fino a pag 137
5	30-03-2011	Invariant and Safety Properties	lec5.pdf e lec6.pdf, fino a pag 82
6	31-03-2011	Liveness Properties and Fairness	lec6.pdf e lec7.pdf, fino a pag 135
7	06-04-2011	Process Fairness, Esercitazione	lec7.pdf, esercizi-2011-01.pdf
8	07-04-2011	Regular Safety Properties	lec08.pdf
9	13-04-2011	Büchi Automata	lec09_10.pdf, fino a pag. 135
10	14-04-2011	Model Checking with Büchi Automata	lec09_10.pdf, lec11.pdf
11	04-05-2011	Linear Time Logic	lec12_13.pdf, fino a pag 182 (def. di weak until)
12	05-05-2011	SPIN: Introduzione all'ambiente	mvs-spin-01.pdf
13	09-05-2011	LTL Model Checking	lec14_15.pdf, fino a pag 227 (escluso soundness)
14	11-05-2011	SPIN: Ancora sul linguaggio PROMELA	mvs-spin-02.pdf; Esercizi suggeriti: http://spinroot.com/spin/Man/Exercises.html
15	12-05-2011	LTL and fairness; Panoramica su CTL	lec12_13.pdf, da pag 243; lec17.pdf, fino a pag 81
16	16-05-2011	Esercitazione	esercizi-2011-02.pdf
17	18-05-2011	PROMELA: cicli do-od, sequenze atomiche e altro	mvs-spin-03.pdf
18	19-05-2011	Specifica di proprietà in PROMELA: asserzioni, end/progress/accept states, never claims	mvs-spin-04.pdf
19	23-05-2011	Esercitazione
20	25-05-2011	PROMELA: Never claims, trace assertion, da LTL a never claims. Presentazione progetto	mvs-spin-05.pdf
21	26-05-2011	Classificazione di proprietà LTL; LTL e ω-regualar properties; CTL e LTL	mvs-spin-06.pdf

Alternating Bit Protocol (con lossy channels e timeout

mtype = { msg, ack };
chan to_sndr = [1] of { mtype, bit };
chan to_rcvr = [1] of { mtype, bit };
chan from_sndr = [1] of { mtype, bit };
chan from_rcvr = [1] of { mtype, bit };

active proctype sender()
{	bit a;
	do
	:: from_sndr!msg,a;
		if
		:: to_sndr?ack,eval(a);
			a = 1 -  a
		:: timeout /* retransmission */
		fi
    od
}
active proctype channel()
{	mtype m; bit a;
	do
	:: from_sndr?m,a ->
		if
		:: to_rcvr!m,a
		:: skip /* message loss */
		fi
	:: from_rcvr?m,a ->
		to_sndr!m,a
	od
}
active proctype receiver()
{	bit a;
	do
	:: to_rcvr?msg,eval(a);
		from_rcvr!ack,a;

		a = 1 - a
	od
}