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

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

===== Alternating Bit Protocol (con lossy channels e timeout =====

<code>
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
}
</code>