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

Docenti: Andrea Corradini, GianLuigi Ferrari

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

• 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

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
}