Verification 3

LTL, Büchi Automata, 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.

Construct Büchi automata accepting precisely the set of infinite computations satisfying the formulas Gp (invariantly p),  Fp (eventually p)   and (G ((p) -> (F(q))) as well as their complement.  Here p and q are atomic propositions.

Exercise 2

• Prove or disprove the equivalence of the formulas  (Fp) U (Fq)  and  F(p U q)
• Prove or disprove equivalence of the formulas  G(p=>Xp)  and  G(p=>Gp)

Model and analyse the protocols of JPK exercises 23 and 24 in either SPIN or NuSMV. Henrik Ejersbo Jensen will tell you about SPIN during the lecture on Thursday. Oliver will fill you in on NuSMV when he come back from Brussels (next week).

Exercise 4 (to be handed in)

Model and anlyse the protocol of JPK exercise 25 in both SPIN and NuSMV.  In particular try to compare the performance of the two tools (how far do they get).

For exercises 3 and 4 you should write a small report describing you models and verification results. Please hand them in to Oliver.