Abstraction in Model Checking.ppt
《Abstraction in Model Checking.ppt》由会员分享,可在线阅读,更多相关《Abstraction in Model Checking.ppt(68页珍藏版)》请在麦多课文档分享上搜索。
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
- 1.请仔细阅读文档,确保文档完整性,对于不预览、不比对内容而直接下载带来的问题本站不予受理。
- 2.下载的文档,不会出现我们的网址水印。
- 3、该文档所得收入(下载+内容+预览)归上传者、原创作者;如果您是本文档原作者,请点此认领!既往收益都归您。
本资源只提供5页预览,全部文档请下载后查看!喜欢就下载吧,查找使用更方便
2000 积分 0人已下载
下载 | 加入VIP,交流精品资源 |
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- ABSTRACTIONINMODELCHECKINGPPT