mm1

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
mm1

Verification 4

Subject:

Partial order Reduction. SPIN.

Litterature:

LTL

JK: 2.1, 2.2, 2.5-2.9 (you may choose only to skim 2.8)

Partial Order Reduction

CGP: 10.1, 10.2, 10.3, (skim 10.4), 10.5; 11.-11.4

Excercises.

Exercise 1

Model and analyse the protocols of JPK exercises 23 and 24 in SPIN

Exercise 2

Model and anlyse the protocol of JPK exercise 25 in SPIN