基于CEGAR的C程序模型检测研究

发布时间：2021-01-05 14:03

　　软件已经成为当今社会发展中不可或缺的元素,在航空航天、医疗、交通等关键领域已经得到成功的运用。随着软件的重要性日益凸显,软件的可靠性和安全性自然而然地受到重视。长期以来,研究人员一直着眼于如何发现软件中隐藏的错误,保障软件的可靠性和安全性。模型检测是应用广泛且十分有效的方法之一。它通过对程序建模,形式化地描述性质,然后自动化地验证程序是否满足期望的性质。但是,状态空间爆炸问题是模型检测面临的一个关键问题,严重影响了模型检测方法的验证能力,降低了其对大规模程序的验证效果。因此,如何提高模型检测方法的验证效率和验证规模,使得其能更好地应用于大规模的程序验证,已经成为程序验证领域的研究热点。反例制导的抽象细化（Counterexample-guided Abstraction Refinement,CEGAR）技术能有效地缩减模型检测的状态空间,提高模型检测的效率,对大规模程序也有很好的应用性。本文重点围绕基于CEGAR的抽象模型检测方法,研究和讨论如何缓解状态空间爆炸问题,以及如何自动化地对程序的性质进行验证。本文的主要贡献和研究内容如下:第一,基于CEGAR的模型检测方法已经成功地应用于... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：145 页

【学位级别】：博士

【部分图文】：

示例程序simple.c和对应的CFG

西安电子科技大学博士学位论文同时，由于 ( 0, ..., ) → ( [0])，因此，可以得到{ ( 0, · · · , )} ; · · · ; 1{ }即 ( 0, 0, ..., , , ..., )是可满足的，得证。同样，为了更清楚地理解E-interp插值的作用，下面介绍一下对图2.1中的 . 程序，使用E-interp插值进行验证的过程。完整的抽象可达树如图3.5所示，为了方便，在图中用 表示错误插值。首先介绍使用Craig插值计算E-interp插值的过程。 第

展开控制流图 ，探索是否存在一条真反例路径，从而生成抽象可达树 。图3.6展示了验证程序安全性质的框架流图。对于一个抽象状态 : ( , , )，且 不是ERROR位置，则1.如果满足下面三个条件之一，则遍历其他路径分支: = ； = ，且 ( 0, ..., ) → ( )； = ， 被抽象状态 ′覆盖。这里， ′是已经遍历过状态。2.如果 = ，且 ( 0, ..., ) → ( )

【参考文献】：
期刊论文
[1]符号化模型检测CTL[J]. 苏开乐,骆翔宇,吕关锋.  计算机学报. 2005(11)



本文编号：2958799