1、Abstraction in Model Checking,Nishant Sinha,Model Checking,Given a: Finite transition system M A temporal property p The model checking problem: Does M satisfy p?,Model Checking (safety),I,Too many states to handle !,= bad state,MUST ABSTRACT!,Abstraction,Eliminate details irrelevant to the property
2、Obtain simple finite models sufficient to verify the property E.g., Infinite state ! Finite state approximationDisadvantage Loss of Precision: False positives/negatives,Data Abstraction,Abstraction Function h : S ! S,S,S,Data Abstraction Example,Abstraction proceeds component-wise, where variables a
3、re components,x:int, -3, -1, 1, 3, , -2, 0, 2, 4, ,1, 2, 3, , -3, -2, -1,0,y:int,Data Abstraction Example,Partition concrete variables into visible(V) and invisible(I) variables.,The abstract model consists of V variables. I variables are existentially quantified out.,The abstraction function maps e
4、ach state to its projection over V.,Data Abstraction Example,0 0,0 0 0 0 0 0 0 1 0 0 1 0 0 0 1 1,h,x1 x2 x3 x4,x1 x2,Group concrete states with identical visible part to a single abstract state.,Data Type Abstraction,int x = 0; if (x = 0)x = x + 1;,Abstract Data domain,Code,How do we Abstract Behavi
5、ors?,Abstract domain A Abstract concrete values to those in AThen compute transitions in the abstract domain Over-approximations: Add extra behaviors Under-approximations: Remove actual behaviors,Formalism: Kripke Structures,M = (S,s0,!,L) on AP S: Set of States s0: Initial State !: Transition Relat
6、ion L: S ! 2AP, Labeling on States,p,p,!p,p,q,Simulations on Kripke Structures,M = (S, s0, !, L) M = (S, s0, !, L) Definition: R S S is a simulation relation between M and M iffM simulates M (M M) iff (s0, t0)2 R,Intuitively, every transition in M can be matched by some transition in M,(s,s) R impli
7、es L(s) = L(s) for all t s.t. s t , exists t s.t. s t and (t,t) R.,Guarantees from Abstraction,Strong Preservation: M P iff M PWeak Preservation: M P ) M PSimulation preserves ACTL* propertiesIf M M then M AG p ) M AG p,Overview,Formalizing Abstraction/Refinement Homomorphic Abstractions Abstract In
8、terpretation Theory Guarantees from Abstractions Safe Automated Abstraction Refinement - CEGARApplications Hardware e.g., Hom. Abstraction Software e.g., Predicate Abstraction,Building an Abstraction,Computing Abstract DomainComputing Abstract Transitions,Homomorphisms,Clarke et. al.- 94, 00Concrete
9、 States S, Abstract states SAbstraction function (Homomorphism) h: S ! S Induces a partition on S equal to size of S,Existential/Universal Abstractions,Existential Make a transition from an abstract state if at least one corresponding concrete state has the transition. Abstract model M simulates con
10、crete model MUniversal Make a transition from an abstract state if all the corresponding concrete states have the transition.,Existential Abstraction (Over-approximation),I,I,S,S,Universal Abstraction (Under-Approximation),I,I,S,S,Guarantees from Exist. Abstraction,Preservation Theorem M M ,M : coun
11、terexample may be spurious,Converse does not hold M M ,Let be a ACTL* propertyM existentially abstracts M, so M M,M,M,Guarantees from Univ. Abstraction,Preservation Theorem M 2 M 2 ,Converse does not hold M M ,Let be a existential-quantified property (i.e., expressed in ECTL*) and M simulates M,Why
12、spurious counterexample?,Refinement,Problem: Deadend and Bad States are in the same abstract state. Solution: Refine abstraction function. The sets of Deadend and Bad states should be separated into different abstract states.,Refinement,h,Refinement : h,Abstract Interpretation,Cousot et. al. 77 Fram
13、ework for approximating fixpoint computations Galois Connections Concrete: S, Abstract: S Abstract S. F(S) = S as S. F(S) = S Homomorphisms are a particular case Widening/Narrowing,Galois Connections,S concrete, S abstract S must be a complete lattice : 2S S - abstraction function : S 2S - concretiz
14、ation function Properties of and : (A) A, for A in S (X) X, for X S The above properties mean that and are Galois-connected,S,S,Abs. Interpretation: Example,int - even, odd, T (even) = ,-2,0,2,4 (odd) = ,-3,-1,1,3 (T) = intPredicate abstraction is an instance,Computing Abstract Transition Relation,E
15、xistential AbstractionR Dams97: (t, t1) R iff s (t) and s1 (t1) s.t. (s, s1) RThis ensures that M simulates M Preservation Theorem appliesSimilarly, Universal Abstraction R89,S,S,R,R,Other kinds of Abstraction,Cone of InfluenceSlicing,Automated Abstraction/Refinement,Good abstractions are hard to ob
16、tain Automate both Abstraction and Refinement processesCounterexample-Guided AR (CEGAR) Build an abstract model M Model check property P, M P? If M P, then M P by Preservation Theorem Otherwise, check if Counterexample (CE) is spurious Refine abstract state space using CE analysis results Repeat,Cou
17、nterexample-Guided Abstraction-Refinement (CEGAR),Check Counterexample,Obtain Refinement Cue,Model Check,Build New Abstract Model,M,M,No Bug,Pass,Fail,Bug,Real CE,Spurious CE,Use of Abstractions in Hardware and Software Verification,Applications,Hardware Verification: Thousands of Latches Abstract u
18、sing homomorphisms SAT-based methods (Clarke et. al.)Software Verification: Integer variables, Undecidability Predicate Abstraction SLAM MAGIC, BLASTAll these approaches are automated (CEGAR),Verifying Hardware: Abstraction,A number of approaches Localization (Kurshan et. Al.) SAT-based (02) We cons
19、ider a homomorphism-based approach inside CEGAR framework,Counterexample-Guided Abstraction-Refinement (CEGAR),Check Counterexample,Obtain Refinement Cue,Model Check,Build New Abstract Model,M,M,No Bug,Pass,Fail,Bug,Real CE,Spurious CE,Abstraction Function,Partition variables into visible(V) and inv
20、isible(I) variables.,The abstract model consists of V variables. I variables are made inputs (existentially quantified).,The abstraction function maps each state to its projection over V.,Abstraction Function Example,0 0,0 0 0 0 0 0 0 1 0 0 1 0 0 0 1 1,h,x1 x2 x3 x4,x1 x2,Group concrete states with
21、identical visible part to a single abstract state.,Abstract Model Computation,I,I,Existential Abstraction:,Obtaining Exist. Abstraction Symbolically,Concrete Model : (S, I, R, L) Abstract Model: (S,I,R,L) h: S ! SS = s j 9s 2 S. h(s)=sI = s j 9s 2 S. I(s) h(s)=sR = (s1,s2) j 9 s1,s2. R(s1,s2) h(s1)=
22、s1 h(s2)=s2,Checking the Counterexample,Model check the abstract model Yes or a Counterexample CE Counterexample : (c1, ,cm) Each ci is an assignment to V.Simulate the counterexample on the concrete model.,Checking the Counterexample,Concrete traces corresponding to the counterexample:,(Initial Stat
23、e),(Unrolled Transition Relation),(Restriction of V to Counterexample),Refine if CE is spurious,Spurious counterexample?,Refinement,h,h,h,h,Refinement (h): Make Invisible variables Visible,h,h,Refinement methods,(R. Kurshan, 80s),Localization,Simulate counterexample on concrete model with SAT If the
24、 instance is unsatisfiable, analyze conflict Make visible one of the variables in the clauses that lead to the conflict,(Chauhan, Clarke, Kukula, Sapra, Veith, Wang, FMCAD 2002),Abstraction/refinement with conflict analysis,Refinement methods,Refinement as Separation,Refinement as Separation,Deadend
25、 States,Bad States,Refinement as Separation,0 1 0 1,0 1 0,d1,b1,b2,I,V,Refinement : Find subset U of I that separates between all pairs of deadend and bad states. Make them visible.Keep U small !,v1 v2 v3 v4 v5 v6 v7,Refinement as Separation,d1,b1,b2,I,V,Refinement : Find subset U of I that separate
26、s between all pairs of deadend and bad states. Make them visible.Keep U small !,v1 v2 v3 v4 v5 v6 v7,Refinement as Separation,The state separation problem Input: Sets D, B Output: Minimal U subset of I s.t.: d D, b B, u U. d(u) b(u),The refinement h is obtained by adding U to V.,Two separation metho
27、ds,ILP-based separation Minimal separating set. Computationally expensive.Decision Tree Learning based separation. Not optimal. Polynomial.,More Details ,SAT-based Abstraction Refinement Using ILP and Machine Learning, Edmund Clarke, Anubhav Gupta, James Kukula, Ofer Strichman. CAV02Automated Abstra
28、ction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis, Pankaj Chauhan, Edmund M. Clarke, James H. Kukula, Samir Sapra, Helmut Veith, Dong Wang. FMCAD02,Software: Predicate Abstraction,Graf, Saidi 97 Abstraction using Galois Connections Predicates define abstract st
29、ates Existential abstraction using theorem provers Example P = p1, p2: p1 x5, p2 y4 States: (p1,p2), (!p1,p2) ,Defining an Abstract Domain,Predicates on Variables E.g., p1 x3 Do not abstract program location variablesWeakest Preconditions (WP) WP(x=y+1, p1) (y+13) (y2) WP (Y, x=e) = Y e/xPredicate D
30、iscovery using WP,x = y+1,x3,y2,CEGAR,Build Model Using initial set of predicates P Model Check Generate reachable states explicitly/symbolically Obtain CE Check if CE is spurious SAT-based Refinement Cue Find new predicates to add to P,Example,Q: Is Error Reachable ?,Example ( ) 1: do lock();old =
31、new; 2: if (*) 3: unlock();new +; 4: while ( new != old); 5: unlock ();return; ,lock() sets LOCK=1 unlock() sets LOCK=0,Example ( ) 1: do lock();old = new; 2: if (*) 3: unlock();new +; 4: while ( new != old); 5: unlock ();return; ,Example:CFG,lock(); old = new,Example:CFG,Q: Is Error Reachable ?,Exa
32、mple ( ) 1: do lock();old = new; 2: if (*) 3: unlock();new +; 4: while ( new != old); 5: unlock ();return; ,Step 1: Generate and Model Check Abstract space,Set of predicates: LOCK=0, LOCK=1,1,LOCK=0,lock(); old = new,unlock(),unlock() new+,new=old,4,LOCK=0,Q: When can:,Step 2: Analyze Counterexample
33、,Err,LOCK=0,Fwd Reachable (Deadend) States at node n = Rn,Formulate as satisfiability problem for a logic,Step 2: Analyze Counterexample,lock(); old = new,new=old,unlock(),LOCK=0,LOCK=0 new = old,Formulate as satisfiability problem for a logic,unlock(); new+,Step 2: Analyze Counterexample,LOCK=0,LOC
34、K=0,LOCK=0 new = old,LOCK=0 new+1 = new,LOCK=1 new+1 = old,LOCK=1 new +1 = old,Track the predicate:new = old,Step 3: Resume Search,new!=old,1,Set of predicates: LOCK=0, LOCK=1, new = old,4,LOCK=0 : new = old,Step 3: Resume Search,2,LOCK=1 new = old,3,LOCK=1 new = old,4,LOCK=0 : new = old,?,5,1,LOCK=
35、0 : new = old,5,ERROR Unreachable,Set of predicates: LOCK=0, LOCK=1, new = old,CEGAR for Software Verification,(C programs) SLAM 00 Abstract C programs to Boolean programs (C2BP) Symbolic Model Checker (Bebop), CE-analysis (Newton)(C programs) BLAST On-the-fly Predicate Abstraction Lazy Abstraction
36、Proof-based CE analysis(C programs) MAGIC Handles concurrent message-passing programs Two-level CEGAR(Java programs) ESC/Java, Bandera, ,Using SAT in Predicate Abstraction,Build Abstraction: All-SAT for computing abstract transitionsModel Check: BDD-basedChecking CE: BMC-like simulation of CERefinem
37、ent: Uses proof of infeasibility of CE from SAT solver,Conclusion,Formal basis for Abstraction/Refinement Homomorphic Abstractions Abstract Interpretation Safe AbstractionsApplications Hardware e.g., Hom. Existential Abstraction Software e.g., Predicate Abstraction,Acknowledgements,We thank the following sources for the slides: Model Checking Group, CMU BLAST group, Berkeley Bandera group, KSU,
