Lecture 10 Finding Parameterized Invariants A Pnueli Automatically Finding Auxiliary Parameterized Invariants We will now consider a method for finding inductive assertions for Analysis of Reactive Systems NYU Spring 2006 BDS s 178 Lecture 10 Finding Parameterized Invariants A Pnueli Automatic Generation of Auxiliary Invariants Goal Compute Auxiliary Inductive Assertion of the form i i 1 Let reach be the assertion characterizing all the reachable states of system S N0 for N0 H 3 E g MUTEX Since H 1 N0 4 4 X i 2 3 1 reach x i 1 2 Let 1 be the assertion obtained from reach by projecting away all the references to variables subscripted by indices other than 1 E g MUTEX 1 1 2 3 x 0 3 Let i be the assertion obtained from 1 by generalizing 1 into i The candidate for inductive assertion is i i E g MUTEX i i 2 3 x 0 Unfortunately i i is not inductive over guaranteed to produce inductive assertions Analysis of Reactive Systems NYU Spring 2006 MUTEX 2 algorithm is not 179 Lecture 10 Finding Parameterized Invariants A Pnueli Compute Auxiliary Assertion of the form i i 1 Let reach system S N0 be the assertion characterizing all the reachable states of 2 Let g be the transition abstraction relation which contains for each finitedomain variable x the conjunct x x 3 For each i 1 N0 let 17 i be the transition relation which contains for each index variable k 1 N the conjunct k i k 1 and for each array variable y array 1 N of boolean the conjunct y i y 1 4 Let i reach g 17 i be the assertion obtained from reach by preserving all the global variables and porting all the properties of index 1 to index i We take N0 i i 1 Since assertion is computed internally and immediately consumed the user never gets to see it This is why we refer to this method as Verification by invisible invariants Analysis of Reactive Systems NYU Spring 2006 180 Lecture 10 Finding Parameterized Invariants Example A Pnueli MUTEX with 1 Index Assertion In file mutex5 inv1 pf we place Func abs reach f t Local trans next y y next P t loc P f loc Return succ trans reach End Func abs reach f t To compute invis Let reach reachable 1 Let phi 1 For i in 1 N Let phi phi abs reach 1 i End For i in 1 N End compute invis Analysis of Reactive Systems NYU Spring 2006 181 Lecture 10 Finding Parameterized Invariants A Pnueli File Continued To calc exc Let exc 1 For i in 1 N For j in i 1 N Let exc exc P i loc notin 3 P j loc notin 3 End For j in i 1 N End For i in 1 N End calc exc calc exc compute invis Print n Check mutual exclusion n Call inv exc phi 1 Computed assertion fails to be inductive Premise 2 fails Analysis of Reactive Systems NYU Spring 2006 182 Lecture 10 Finding Parameterized Invariants A Pnueli Compute Auxiliary Assertion of the form i 6 j i j 1 Let reach system S N0 be the assertion characterizing all the reachable states of 2 Let g be the transition abstraction relation which contains for each finitedomain variable x the conjunct x x 3 For each i 1 N0 let 17 i be the transition relation which contains for each index variable k 1 N the conjunct k i k 1 and for each array variable y array 1 N of boolean the conjunct y i y 1 Similarly define 27 j 4 Let i j reach g 17 i 27 j be the assertion obtained from reach by preserving all the global variables and porting all the properties of indices 1 2 to index i j respectively We take N0 N0 i j i 1 j i 1 Analysis of Reactive Systems NYU Spring 2006 183 Lecture 10 Finding Parameterized Invariants A Pnueli Applying the Algorithm to MUTEX Consider MUTEX reach with N0 3 4 X i 2 3 x 1 i 1 1 2 i j 1 2 3 x 0 2 2 3 x 0 i 2 3 x 0 j 2 3 x 0 2 0 1 1 0 1 i 0 1 j 0 1 i 6 j i j is an inductive assertion over MUTEX 5 and therefore over all MUTEX N It also implies the property of mutual exclusion i 6 j i 2 j 2 Analysis of Reactive Systems NYU Spring 2006 184 Lecture 10 Finding Parameterized Invariants A Pnueli In TLV In file mutex5 inv2 pf we modify function abs and compute invis as follows Func abs reach f1 f2 t1 t2 Local trans next y y next P t1 loc P f1 loc next P t2 loc P f2 loc Return succ trans reach End Func abs reach f1 f2 t1 t2 To compute invis Let reach reachable 1 Let phi 1 For i in 1 N For j in i 1 N Let phi phi abs reach 1 2 i j End For j in i 1 N End For i in 1 N End compute invis Analysis of Reactive Systems NYU Spring 2006 185 Lecture 10 Finding Parameterized Invariants Example A Modified A Pnueli MUTEX in N natural where N 1 local x boolean where x 1 local last 1 N 0 loop forever do 1 Non Critical N P h 2 hrequest x last hi 3 Critical h 1 4 release x Searching for a i inductive assertion we obtained the calculated invariant i i 3 4 x 0 last i The candidate assertion is inductive and also implies the property of mutual exclusion p i 6 j i 3 j 3 Analysis of Reactive Systems NYU Spring 2006 186 Lecture 10 Finding Parameterized Invariants A Pnueli In TLV In file mutex mod inv1 pf we place Func abs reach f t Local trans next y y next last t last f next P t loc P f loc Return succ trans reach End Func abs reach f t This time the auxiliary assertion is inductive Analysis of Reactive Systems NYU Spring 2006 187 Lecture 10 Finding Parameterized Invariants A Pnueli Example Program Arbiter Consider the following program ARBITER r g array 1 N of boolean where i 1 N r i g i 0 loop forever do k 1 N where k 1 loop forever do 0 Non Critical 1 r i 1 if r k then m0 N m1 g k 1 A C i 2 await g i 3 Critical m2 await r k i 1 m3 g k 0 4 r i 0 m4 k k N 1 5 await g i for which we wish to prove p i 6 j at 3 i at 3 j Analysis of Reactive Systems NYU Spring 2006 188 Lecture 10 Finding Parameterized Invariants A Pnueli Verifying Arbiter by the Invisible Invariants Method In file arbiter smv we place the following MODULE main DEFINE N 6 VAR k …
View Full Document
Unlocking...