针对Java语言中间形式的谓词抽象算法.pdfVIP

3185 计算机工程与设计ComputerEngineeringandDesign2009，30(13) ’ ·开发与应用· 针对Java语言中问形式的谓词抽象算法 王波， 沈云付 (上海大学计算机工程与科学学院，上海200072) 摘要：谓词抽象是解决软件模型检查中状态空间爆炸的最有效方法之一，针对Java语言面向对象的特性，描述了一种对 语句、条件语句，类对象引用，成员方法和方法调用等。用一个Java程序实例说明了该算法的抽象过程和结果。 关键词：模型检测；状态爆炸；抽象；谓词抽象；布尔程序 中图法分类号：TP301．2文献标识码：A 文章编号：1000—7024(2009)13-3185—04 of abstractionforintermediateformofJava Algorithmpredicate program Ⅵ硷NGBo． SHENYun．fu of and (SchoolComputerEngineeringScience，Shanghai 200072，China) University,Shanghai in Abstract：Predicateabstractionisolleofthemosteffectivetoaddressstate softwaremodel the ways explosion checking．Forobject- orientedfeaturesofJava toconstructa abstraction writteninJavais this program．狮algorithmpredicate ofprograms presented．Using Java isabstractedtoaBoolean thecourseofthe handlessome abstract,this algorithm,aprogram program．In algorithm syntactic constructs methodandmethodcalls．Atlastanabstract ofJava program，includingassignment,conditionals，classreference，member andresultofJava is process programgiven． words：model abstraction；Boolean Key checking；stateexplosion；abstraction；predicateprogram 检验工具，它通过分析过程问的数据流来处理过程调用。 0引 言 NEWTON通过分析程序中的可行路径寻找用于求精布尔程 模型检测是一种关于系统性质验证的形式化方法，它通 序