Strumenti Utente

Strumenti Sito


magistraleinformatica:mvs:year2010:start

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
}
magistraleinformatica/mvs/year2010/start.txt · Ultima modifica: 18/02/2013 alle 21:17 (5 anni fa) da Andrea Corradini