Lecture 2: Demonstrating Model Checking A. PnueliUsing TLV for Model CheckingWe will introduce the programmable symbolic model checker TLV and illustrate itsuse for model checking finite-state systems.The TLV tool, developed by Elad Shahar, is a programmable symbolic calculatorover finite-state systems, based on the CMU symbolic model checker SMV.It can be used to model check temporal properties of finite-state systems.TLVSPLCoutputsys.spl sys.smvscr.pfAnalysis of Reactive Systems, NYU, Spring, 2006 33Lecture 2: Demonstrating Model Checking A. PnueliExamples of Model CheckingWe will illustrate how formal verification (when it works) can aid us in thedevelopment of reliable programs.Consider the following program TRY-1 which attempts to solve the mutualexclusion problem by shared variables:local y1, y2: boolean where y1= y2= 0P1::ℓ0: loop forever doℓ1: Non-Criticalℓ2: await ¬y2ℓ3: y1:= 1ℓ4: Criticalℓ5: y1:= 0k P2::m0: loop forever dom1: Non-Criticalm2: await ¬y1m3: y2:= 1m4: Criticalm5: y2:= 0Variables y1and y2signify whether processes P1and P2are interested in enteringtheir critical sections.Analysis of Reactive Systems, NYU, Spring, 2006 34Lecture 2: Demonstrating Model Checking A. PnueliProgram Properties: InvarianceFor program TRY-1, the property of mutual exclusion can be specified by requiringthat the assertionϕexclusion: ¬(at−ℓ4∧ at−m4)be an invariant of TRY-1. This implies that no execution of TRY-1 can ever get to astate in which both processes execute their critical sections at the same time.In LTL, this property can be specified as¬(at−ℓ4∧ at−m4)Analysis of Reactive Systems, NYU, Spring, 2006 35Lecture 2: Demonstrating Model Checking A. PnueliInvoking TLVTo check whether assertionϕexclusionis an invariant of program TRY-1, we invokethe model checking tool TLV, a model checker based on the SMV tool developedin CMU by Ken McMillan and Ed Clarke.We prepare two input files: try1.smv which contains the SMV representationof TRY-1, and try1.pf, a proof script file. The proof script file contains someprinting commands, definition of the assertionϕexclusionand a command to checkits invariance over the program.We will present each of these input files.Analysis of Reactive Systems, NYU, Spring, 2006 36Lecture 2: Demonstrating Model Checking A. PnueliFile try1.smvMODULE mainVAR y1: boolean; y2: boolean;P[1]: process MP(y1,y2); P[2]: process MP(y2,y1);MODULE MP(mine,hers)VAR loc : 0..5;ASSIGN init(mine) := 0; init(loc) := 0;next(loc) := caseloc in {0,3,4,5} : (loc+1) mod 6;loc=1 : {1,2};loc=2 & !hers : 3;1 : loc;esac;next(mine) := caseloc=3 : 1;loc=5 : 0;1 : mine;esac;JUSTICEloc!=0, !(loc=2 & !hers), loc!=3, loc!=4,loc!=5Analysis of Reactive Systems, NYU, Spring, 2006 37Lecture 2: Demonstrating Model Checking A. PnueliFile try1.pfPrint "Check for Mutual Exclusion\n";Let exclusion := !(P[1].loc=4 & P[2].loc=4);Call Invariance(exclusion);The call to procedure Invariance invokes the process which checks whetherany reachable state violates the assertion exclusion.Analysis of Reactive Systems, NYU, Spring, 2006 38Lecture 2: Demonstrating Model Checking A. PnueliResults of Verifying TRY-1The results of model-checking TRY-1 are>> Load "try1.pf";Model checking Invariance Property***Property is NOT VALID***Counter-Example Follows:State 1 : y1 = 0, y2 = 0, P[1].loc = 0, P[2].loc = 0,State 2 : y1 = 0, y2 = 0, P[1].loc = 0, P[2].loc = 1,State 3 : y1 = 0, y2 = 0, P[1].loc = 0, P[2].loc = 2,State 4 : y1 = 0, y2 = 0, P[1].loc = 0, P[2].loc = 3,State 5 : y1 = 0, y2 = 0, P[1].loc = 1, P[2].loc = 3,State 6 : y1 = 0, y2 = 0, P[1].loc = 2, P[2].loc = 3,State 7 : y1 = 0, y2 = 0, P[1].loc = 3, P[2].loc = 3,State 8 : y1 = 0, y2 = 1, P[1].loc = 3, P[2].loc = 4,State 9 : y1 = 1, y2 = 1, P[1].loc = 4, P[2].loc = 4,Analysis of Reactive Systems, NYU, Spring, 2006 39Lecture 2: Demonstrating Model Checking A. PnueliExpressed in a More Readable Formlocal y1, y2: boolean where y1= y2= 0P1::ℓ0: loop forever doℓ1: Non-Criticalℓ2: await ¬y2ℓ3: y1:= 1ℓ4: Criticalℓ5: y1:= 0k P2::m0: loop forever dom1: Non-Criticalm2: await ¬y1m3: y2:= 1m4: Criticalm5: y2:= 0The counter example is:hℓ0, m0, y1: 0, y2: 0i,hℓ1, m0, y1: 0, y2: 0i,hℓ1, m1, y1: 0, y2: 0i,hℓ1, m2, y1: 0, y2: 0i,hℓ1, m3, y1: 0, y2: 0i,hℓ2, m3, y1: 0, y2: 0i,hℓ3, m3, y1: 0, y2: 0i,hℓ3, m4, y1: 0, y2: 1i,hℓ4, m4, y1: 1, y2: 1ireaching the state hℓ4, m4, y1: 1, y2: 1i which violates mutual exclusion!Obviously, the problem is that the processes test each other’s y value first andonly later set their own y.Analysis of Reactive Systems, NYU, Spring, 2006 40Lecture 2: Demonstrating Model Checking A. PnueliSecond Attempt: Set first and Test LaterThe following program TRY-1 interchange the order of testing and setting:local y1, y2: boolean where y1= y2= 0P1::ℓ0: loop forever doℓ1: Non-Criticalℓ2: y1:= 1ℓ3: await ¬y2ℓ4: Criticalℓ5: y1:= 0k P2::m0: loop forever dom1: Non-Criticalm2: y2:= 1m3: await ¬y1m4: Criticalm5: y2:= 0Let us see whether the program is now correct.Analysis of Reactive Systems, NYU, Spring, 2006 41Lecture 2: Demonstrating Model Checking A. PnueliProgram Properties: Absence of DeadlockA state s is said to be a deadlock state if no process can perform any action. Inour FDS model, the idling transition is always enabled. Therefore, we define s tobe a deadlock state if it has no D-successor different from itself.Mathematically, we can characterize all deadlock states by the assertionδ : ¬∃V′6= V : ρ(V, V′)and then check for the invariance of the assertion ¬δ.To check for the interesting properties of program TRY-2, we prepare thefollowing script file:Print "Check for Mutual Exclusion\n";Let exclusion := !(P[1].loc=4 & P[2].loc=4);Call Invariance(exclusion);Run check_deadlock;Analysis of Reactive Systems, NYU, Spring, 2006 42Lecture 2: Demonstrating Model Checking A. PnueliModel Checking TRY-2We obtain the following results:>> Load "try2.pf";Check for Mutual
View Full Document