欢迎来到麦多课文档分享! | 帮助中心 海量文档,免费浏览,给你所需,享你所想!
麦多课文档分享
全部分类
  • 标准规范>
  • 教学课件>
  • 考试资料>
  • 办公文档>
  • 学术论文>
  • 行业资料>
  • 易语言源码>
  • ImageVerifierCode 换一换
    首页 麦多课文档分享 > 资源分类 > PPT文档下载
    分享到微信 分享到微博 分享到QQ空间

    BDD vs. Constraint Based Model Checking- An Experimental .ppt

    • 资源ID:378878       资源大小:441KB        全文页数:48页
    • 资源格式: PPT        下载积分:2000积分
    快捷下载 游客一键下载
    账号登录下载
    微信登录下载
    二维码
    微信扫一扫登录
    下载资源需要2000积分(如需开发票,请勿充值!)
    邮箱/手机:
    温馨提示:
    如需开发票,请勿充值!快捷下载时,用户名和密码都是您填写的邮箱或者手机号,方便查询和重复下载(系统自动生成)。
    如需开发票,请勿充值!如填写123,账号就是123,密码也是123。
    支付方式: 支付宝扫码支付    微信扫码支付   
    验证码:   换一换

    加入VIP,交流精品资源
     
    账号:
    密码:
    验证码:   换一换
      忘记密码?
        
    友情提示
    2、PDF文件下载后,可能会被浏览器默认打开,此种情况可以点击浏览器菜单,保存网页到桌面,就可以正常下载了。
    3、本站不支持迅雷下载,请使用电脑自带的IE浏览器,或者360浏览器、谷歌浏览器下载即可。
    4、本站资源下载后的文档和图纸-无水印,预览文档经过压缩,下载后原文更清晰。
    5、试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓。

    BDD vs. Constraint Based Model Checking- An Experimental .ppt

    1、BDD vs. Constraint Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems,Tevfik Bultan Department of Computer Science University of California, Santa Barbara bultancs.ucsb.edu http:/www.cs.ucsb.edu/bultan/,Outline,Concurrency problems Symbolic model checking Functional

    2、ity required for symbolic model checking BDD representation Constraint representation Experimental results Related work Conclusions,Program: Bakery Data Variables: a, b: positive integer Control Variables: pc1, pc2: T, W, C Initial Condition: a=b=0 & pc1=T1 & pc2=T2 Events: eT1: pc1=T & pc1=W & a=b+

    3、1 eW1: pc1=W & (ab | b=0) & pc1=C eC1: pc1=C & pc1=T & a=0eT2: pc2=T & pc2=W & b=a+1 eW2: pc2=W & (ba | a=0) & pc2=C eC2: pc2=C & pc2=T & b=0BAKERY: AG(!(pc1=c & pc2=C),Program: Barber Data Variables: cinchair,cleave,bavail,bbusy,bdone: positive integer Control Variables: pc1,pc2,pc3: 1,2 Initial Co

    4、ndition: cinchair=cleave=bavail=bbusy=bdone=0 & pc1=pc2=pc3=1 Events: eHairCut1: pc1=1 & pc1=2 & cinchairbavail & cinchair=cinchair+1 eHairCut2: pc1=2 & pc1=1 & cleavebdone & cleave=cleave+1 eNext1: pc2=1 & pc2=2 & bavail=bavail+1 eNext2: pc2=2 & pc2=1 & bbusycinchair & bbusy=bbusy+1 eFinish1: pc3=1

    5、 & pc3=2 & bdonebbusy & bdone=bdone+1 eFinish2: pc3=2 & pc3=1 & bdone=cleave,BARBER: AG(cinchair =cleave & bavail=bbusy=bdone& cinchair=cleave & bavail=bbusy=bdone)BARBER-2: AG(cinchair=bavail & bbusy=cinchair)BARBER-3: AG(cleave=bdone),Program:Readers-Writers Data Variables: nr, nw: positive intege

    6、r Initial Condition: nr=nw=0 Events: eReaderEnter: nw=0 & nr=nr+1 eReaderExit: nr0 & nr=nr-1eWriterEnter: nr=0 & nw= 0 & nw=nw+1 eWriterExit: nw0 & nw=nw-1READERS-WRITERS: AG(nr=0 | nw=0) & nw=1),Program: Bounded-Buffer Parameterized Constant: size: positive integer Data Variables: available, produc

    7、ed, consumed: positive integer Initial Condition: produced=consumed=0& available = size Events: eProduce: 0available & produced=produced+1& available=available-1 eConsume: availablesize & consumed=consumed+1& available=available+1,BOUNDED-BUFFER: AG(produced-consumed=size-available& 0=available=size

    8、)BOUNDED-BUFFER-1: AG(produced-consumed=size-available)BOUNDED-BUFFER-2: AG(0=available=size)BOUNDED-BUFFER-3: AG(0=produced-consumed=size),Program: Circular-Queue Parameterized Constant: size: positive integer Data Variables: occupied,head,tail,produced, consumed : positive integer Initial Conditio

    9、n:occupied=head=tail=produced=consumed=0 Events: eProduce: occupied0 & occupied=occupied-1& consumed=consumed+1 & (head=size & head=0| headsize & head=head+1),CIRCULAR-QUEUE: AG(0=produced-consumed=size& produced-consumed=occupied)CIRCULAR-QUEUE-1: AG(0=produced-consumed=size)CIRCULAR-QUEUE-2: AG(pr

    10、oduced-consumed=occupied),Model Checking,Given a program and a temporal property p:Either show that all the initial states satisfy the temporal property p set of initial states truth set of pOr find an initial state which does not satisfy the property p a state set of initial states truth set of p,T

    11、emporal Properties Fixpoints,EF p p (EX p) EX (EX p) ,1,3,2,Temporal Properties Fixpoints,Note that AG p EF( p )Other temporal operators can also be represented as fixpoints AF p , EG p , p AU q , p EU q,Tools Required for Model Checking,Basic set operations intersection, union, set difference to ha

    12、ndle Equivalence Checking to check if the fixpoint is reached Relational image computation for precondition operation EX,Functionality of a Symbolic Representation,Symbolic And(Symbolic,Symbolic) Symbolic Or(Symbolic,Symbolic) Symbolic Not(Symbolic) Boolean Equivalent(Symbolic,Symbolic) Symbolic EX(

    13、Symbolic),BDDs,Efficient representation for boolean functions Disjunction, conjunction complexity: at most quadratic Negation complexity: constant Equivalence checking complexity: constant or linear Image computation complexity: can be exponential,BDD encoding for Integer Variables,Systems with boun

    14、ded integer variables can be represented using BDDs Use a binary encoding represent integer x as x0x1x2. xk where x0, x1, x2, . , xk are binary variablesYou have to be careful about the variable ordering!,Integers in SMV,SMV represents integers using a binary encodingIn the BDD variable ordering cur

    15、rent and next state bits of an integer variable are interleaved good for x = xBits of different variables are not interleaved What happens when we have x = y ?,x2 x2 x1 x1x0x0 y2 y2 y1 y1 y0 y0,We have to remember every x bit until this point for x = y,William Chans Ordering,Using a preprocessor con

    16、verts integer variables to boolean variables Interleaves bits of all integer variables in the BDD ordering Results with much better performance for systems with integer variables,Linear Arithmetic Constraints,ConstraintsConstraint representation, ai xi = c,1 i n, ai xi c,1 i n, constraintkl,1 k h,1

    17、l m,Linear Arithmetic Constraints,Can be used to represent unbounded integers Disjunction complexity: linear Conjunction complexity: quadratic Negation complexity: can be exponential Equivalence checking complexity: can be exponential Image computation complexity: can be exponential,Image Computatio

    18、n in Omega Library,Extension of Fourier-Motzkin variable elimination for real variables Eliminating one variable from a conjunction of constraints may double the number of constraints Integer variables complicate the problem even further,Fourier-Motzkin Variable Elimination,Given two constraints bz

    19、and az we havea abz bWe can eliminate z as:z . a abz b if and only if a b Every upper and lower bound pair can generate a separate constraint, the number of constraints can double for each eliminated variable,real shadow,Integers are More Complicated,If z is integer z . a abz b if a + (a - 1)(b - 1)

    20、 b Remaining solutions can be characterized using periodicity constraints in the following form:z . + i = bz,dark shadow,y . 0 3y x 7 1 x 2y 5,Consider the constraints:,2x 6y,We get the following bounds for y:,6y 2x + 14,6y 3x - 3,3x - 15 6y,When we combine 2 lower bounds with 2 upper bounds we get

    21、four constraints:,0 14 , 3 x , x 29 , 0 12,Result is: 3 x 29,2y x 1,x 5 2y,3y x + 7,x 3y,dark shadow,real shadow,29,3,y,x,Systems with Bounded Integer Variables,BDDs and constraint representations are both applicableWhich one is better?,Experiments,Intel Pentium PC (500MHz, 128MByte main memory) Thr

    22、ee approaches are compared SMV SMV with Chans interleaved variable ordering Omega library model checker,BAKERY: AG(!(pc1=c & pc2=C),BARBER: AG(cinchair =cleave & bavail=bbusy=bdone& cinchair=cleave & bavail=bbusy=bdone) BARBER-2: AG(cinchair=bavail & bbusy=cinchair) BARBER-3: AG(cleave=bdone),READER

    23、S-WRITERS: AG(nr=0 | nw=0) & nw=1),BOUNDED-BUFFER: AG(produced-consumed=size-available& 0=available=size) BOUNDED-BUFFER-1: AG(produced-consumed=size-available) BOUNDED-BUFFER-2: AG(0=available=size) BOUNDED-BUFFER-3: AG(0=produced-consumed=size),CIRCULAR-QUEUE: AG(0=produced-consumed=size& produced

    24、-consumed=occupied) CIRCULAR-QUEUE-1: AG(0=produced-consumed=size) CIRCULAR-QUEUE-2: AG(produced-consumed=occupied),SMV (interleaved),Omega,Each integer variable is restricted to 0 i 1024,SMV (interleaved),Omega,Each integer variable is restricted to 0 i 1024,Size of the buffer is restricted to 0 si

    25、ze 16,Constraint-Based Verification: Not a New Idea,Cooper 71: used a decision procedure for Presburger arithmetic to verify sequential programs represented in a block form Cousot and Halbwachs 78: used real arithmetic constraints to discover invariants of sequential programs,Constraint-Based Verifi

    26、cation:,Halbwachs 93: constraint based delay analysis in synchronous programs Halbwachs et al. 94: verification of linear hybrid systems using constraint representations Alur et al. 96: HyTech, a model checker for hybrid systems,Constraint-Based Verification,Boigelot and Wolper 94: symbolic verifica

    27、tion with periodic sets Bultan et al. 97, 99: used Presburger arithmetic constraints for model checking concurrent systems Delzanno and Podelski 99: built a model checker using constraint logic programming framework,BDD-Based Verification,Bryant 86: Reduced ordered BDDs Coudert et al. 90: BDD-based

    28、verification Burch et al. 90: Symbolic model checking McMillan 93: SMV,Combining BDDs and Constraints,Chan et al. 97: combining BDD representation with a constraint solver (it can handle nonlinear constraints but the transition system is restricted) Bultan et al. 98, 00: combining different symbolic

    29、 representations in one model checker (combined BDDs and linear arithmetic constraints in a disjunctive form),Automata-Based Representations,Klarlund et al. 95: MONA, an automata manipulation tool for verification Wolper and Boigelot: verification using automata as a symbolic representation Kukula e

    30、t al. 98: application of automata based verification to hardware verification,Automata vs. Constraint Representation,Kukula et al. 98: comparison of automata and constraint-based verification comparison based on reachability analysis no clear winner on some cases automata based approach seems to sho

    31、w asymptotic advantage this could be due to inefficient encoding of booleans in constraint representation,Conclusions,Constraint-based representations can be more efficient for integer variables with large domains BDD-based model checking is more robust Constraint-based model checkers can handle infinite state systems Constraint-based model checking suffers from inefficient representation of variables with small domains I believe there is room for improvement for constraint-based model checking techniques,


    注意事项

    本文(BDD vs. Constraint Based Model Checking- An Experimental .ppt)为本站会员(inwarn120)主动上传,麦多课文档分享仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对上载内容本身不做任何修改或编辑。 若此文所含内容侵犯了您的版权或隐私,请立即通知麦多课文档分享(点击联系客服),我们立即给予删除!




    关于我们 - 网站声明 - 网站地图 - 资源地图 - 友情链接 - 网站客服 - 联系我们

    copyright@ 2008-2019 麦多课文库(www.mydoc123.com)网站版权所有
    备案/许可证编号:苏ICP备17064731号-1 

    收起
    展开