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.TheTLV tool, developed by Elad Shahar, is a programmable symbolic calculatoroverfinite-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, Fall, 2009 33Lecture 2: Demonstrating Model Checking A. PnueliExamples of Model CheckingWe will illustrate how formal verification (when it works) can aid us in thedevelopment ofreliable programs.Consider the following programTRY-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:= 0k P2::m0: loop forever dom1: Non-Criticalm2: await ¬y1m3: y2:= 1m4: Criticalm5: y2:= 0Variablesy1and y2signify whether processes P1and P2are interested in enteringtheir critical sections.Analysis of Reactive Systems, NYU, Fall, 2009 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.InLTL, this property can be specified as¬(at−`4∧ at−m4)Analysis of Reactive Systems, NYU, Fall, 2009 35Lecture 2: Demonstrating Model Checking A. PnueliInvoking TLVTo check whether assertionϕexclusionis an invariant of program TRY-1, we invokethemodel checking tool TLV, a model checker based on the SMV tool developedinCMU by Ken McMillan and Ed Clarke.We prepare two input files:try1.smv which contains the SMV representationofTRY-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, Fall, 2009 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, Fall, 2009 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 procedureInvariance invokes the process which checks whetherany reachable state violates the assertionexclusion.Analysis of Reactive Systems, NYU, Fall, 2009 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, Fall, 2009 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:= 0k P2::m0: loop forever dom1: Non-Criticalm2: await ¬y1m3: y2:= 1m4: Criticalm5: y2:= 0The 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 processestest each other’s y value first andonly later set their owny.Analysis of Reactive Systems, NYU, Fall, 2009 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:= 0k P2::m0: loop forever dom1: Non-Criticalm2: y2:= 1m3: await ¬y1m4: Criticalm5: y2:= 0Let us see whether the program is now correct.Analysis of Reactive Systems, NYU, Fall, 2009 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. InourFDS model, the idling transition is always enabled. Therefore, we define s tobe adeadlock state if it has no D-successor different from itself.Mathematically, we can characterize all deadlock states by the assertionδ : ¬∃V06= V : ρ(V, V0)and then check for the invariance of the assertion ¬δ.To check for the interesting properties of programTRY-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, Fall, 2009 42Lecture 2: Demonstrating Model Checking A. PnueliModel Checking TRY-2We obtain the following results:>> Load "try2.pf";Check for Mutual ExclusionModel checking Invariance Property*** Property is VALID ***Check for the absence of Deadlock.Model