Differenze

Queste sono le differenze tra la revisione selezionata e la versione attuale della pagina.

--- magistraleinformatica:mvs:year2010:start [18/02/2013 alle 21:14 (12 anni fa)] – creata Andrea Corradini
+++ magistraleinformatica:mvs:year2010:start [18/02/2013 alle 21:17 (12 anni fa)] (versione attuale) – Andrea Corradini
@@ Linea 1: / Linea 1: @@
-anno accademico 2010-11
+====== 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>