DOC PREVIEW
NYU CSCI-GA 3033 - Deductive Verification

This preview shows page 1-2-20-21 out of 21 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 21 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 21 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 21 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 21 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 21 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Lecture 7: Deductive Verificatioin A. PnueliDeductive VerificationThe method of deductive verification enables proofs of temporal properties ofsystems with infinitely many states. It is based on the application of proof ruleswhich have the general formϕ1· · ·ϕnψThis rule implies that if the premisesϕ1� . . . �ϕnare valid, then so is the conclusionψ. Typically, the premises are assertions (non-temporal formulas while theconclusion is temporal.We distinguish several modes of validity:• |= p General Validity — Formula p is valid over all models. If p is anassertions, this reduces to first-order validity.• D ||= p D-state validity — Assertion p is valid over all D-reachable states. Thesame as D |= p.• D |= p D-validity — Formula p is valid over all D-computations.Analysis of Reactive Systems, NYU, Fall, 2008 108Lecture 7: Deductive Verificatioin A. PnueliWhat is Difficult in Deductive Verification?Among the recognized difficulties in the application of deductive verification, wecan count:• The underlying theory of fair discrete systems, temporal logic and proof rules.• Coming up with the appropriate auxiliary constructs: inductive invariantassertions and ranking functions.• Manipulating the supporting theorem provers.Analysis of Reactive Systems, NYU, Fall, 2008 109Lecture 7: Deductive Verificatioin A. PnueliVerification of Invariance PropertiesWe may use the following basic invariance rule to prove the invariance of assertionp. That is, establish that the formula p, for an assertion p is D-valid.Rule BINVI1. Θ → pI2. p ∧ ρ → p�pAn assertion p satisfying I1 and I2 is called inductive.Claim 13. Rule BINV is sound.Proof Let σ : s0� s1� . . . be a computation of D. By premise I1, s0satisfies p.We show that, for every j = 0� 1� . . ., the validity of p propagates from sjto sj+ 1.Assume that sj|= p. This implies that p�sj[V ]) = 1. Since sj+ 1is a D-successor ofsj, it follows that ρ�sj[V ]� sj+ 1[V ]) = 1. By premise I2, we infer that p�sj+ 1[V ]) = 1,i.e., sj+ 1|= p.By induction on j = 0� 1� . . ., we conclude that every sjsatisfies p, i.e., p is aD-invariant.Analysis of Reactive Systems, NYU, Fall, 2008 110Lecture 7: Deductive Verificatioin A. PnueliExample: Program MUX-SEMConsider the following parameterized program coordinating mutual exclusion bysemaphores.y : integer where y = 1Ni=1P [i] ::�0: loop forever do�1: Non-critical�2: request y�3: Critical�4: release yThe semaphore instructions request y and release y respectively stand for�when y > 0 do y := y − 1� and y := y + 1.We use rule BINV to verify the invariance of the assertionp1: y ≥ 0This assertion is inductive so the proof succeeds.Analysis of Reactive Systems, NYU, Fall, 2008 111Lecture 7: Deductive Verificatioin A. PnueliFor example, one of the instances of premise I2 isy ≥ 0� �� �p∧ ∃i : [1..N ] : π[i] = 2 ∧ y > 0 ∧ y�= y − 1 ∧ π�= �π with [�i) := 3])� �� �ρ2→ y�≥ 0� �� �p�Next, let us try to verify the property of mutual exclusion which can be specifiedas the invariance of the assertionp2: ¬�at−�3[1] ∧ at−�3[2])This attempt fails.Analysis of Reactive Systems, NYU, Fall, 2008 112Lecture 7: Deductive Verificatioin A. PnueliNot Every Invariant Assertion is InductiveAs is already explained when one learns mathematical induction, there are validassertions p which cannot be proven by induction, where the induction hypothesisis taken to be p itself.For example, the claimThe sum 1 + 3 + 5 + · · · + �2k − 1) is a perfect squareor, more mathematicallyp : ∃u : 1 + 3 + 5 + · · · + �2k − 1) = u2cannot be proven by induction, using p as the induction hypothesis.To overcome this difficulty, one often has to come up with a strengthening of p ,being an assertionϕwhich implies p and is inductive. For the above example, thiscan beϕ: 1 + 3 + 5 + · · · + �2k − 1) = k2Analysis of Reactive Systems, NYU, Fall, 2008 113Lecture 7: Deductive Verificatioin A. PnueliRule INVThe above considerations lead to the more general INV rule.Rule INVFor an assertionϕ,I1. Θ →ϕI2.ϕ∧ ρ →ϕ�I3.ϕ→ ppBy premises I1 and I2,ϕis an invariant of the system. That is, all reachable statessatisfyϕ. Since, by premise I3,ϕimplies p, it follows that p is also a D-invariant.For example, we can establish the invariance ofp2: ¬�at−�3[1] ∧ at−�3[2])using rule INV with the strengtheningϕ: �y ≥ 0) ∧ �at−�3�4[1] + at−�3�4[2] + · · · + at−�3�4[N] + y = 1)Analysis of Reactive Systems, NYU, Fall, 2008 114Lecture 7: Deductive Verificatioin A. PnueliUsing TLV for Incremental StrengtheningThe 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 LTL formulas over finite-state systems. As wewill show, it can also be used for incremental development of inductive assertions.To do so, we define a finite-state restriction of the original program, explicitlycalculate the candidate assertion, and apply rule BINV.• If the rule application produces a counter-example, the assertion is notinductive. We should strengthen it, and repeat the procedure.• If the rule application succeeds, there are good chances (but no guarantee)that the assertion is inductive. This it the time to shift to PVS in order to get thefinal confirmation.Analysis of Reactive Systems, NYU, Fall, 2008 115Lecture 7: Deductive Verificatioin A. PnueliTLVSPLCoutputsys.spl sys.smvscr.pfAnalysis of Reactive Systems, NYU, Fall, 2008 116Lecture 7: Deductive Verificatioin A. PnueliThe Input File mux3.smvMODULE mainDEFINE N:= 3;VAR y : boolean;P : array 1..N of process MP(y);Id: process Idle;ASSIGN init(y) := 1;MODULE IdleMODULE MP(y)VAR loc: 0..4;ASSIGNinit(loc) := 0;next(loc) := caseloc in {0,1,3,4} : (loc + 1) mod 5;loc = 2 & y : 3;1 : loc;esac;next(y) := caseloc = 2 & next(loc) = 3 : 0;loc = 4 & next(loc) = 0 : 1;Analysis of Reactive Systems, NYU, Fall, 2008 117Lecture 7: Deductive Verificatioin A. Pnueli1 : y;esac;JUSTICE loc != 0, loc != 3, loc != 4COMPASSION (loc = 2 & y, loc = 3)Analysis of Reactive Systems, NYU, Fall, 2008 118Lecture 7: Deductive Verificatioin A. PnueliModel Checking Mutual ExclusionIn file scr1.pf, we place the textPrint "\n Model Check mutual exclusion


View Full Document

NYU CSCI-GA 3033 - Deductive Verification

Documents in this Course
Design

Design

2 pages

Real Time

Real Time

17 pages

Load more
Download Deductive Verification
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 Deductive Verification 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 Deductive Verification 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?