DOC PREVIEW
NYU CSCI-GA 3033 - Using TLV for Model Checking

This preview shows page 1-2-3-4-5-6 out of 17 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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:= 0k P2::m0: loop forever dom1: Non-Criticalm2: await ¬y1m3: y2:= 1m4: Criticalm5: y2:= 0Variables 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:= 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 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:= 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, 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

NYU CSCI-GA 3033 - Using TLV for Model Checking

Documents in this Course
Design

Design

2 pages

Real Time

Real Time

17 pages

Load more
Download Using TLV for Model Checking
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Using TLV for Model Checking and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Using TLV for Model Checking 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?