基于模块化Abstract-Refine算法框架的软件模型检测方法

doi:10.3969/j.issn.0372-2112.2020.05.022

摘要
图/表
参考文献(0)
相关文章 (15)

全文: PDF (536 KB) HTML (1 KB)
输出: BibTeX | EndNote (RIS)

摘要 Abstract-Refine（抽象—精炼）方法是软件模型检测领域中较为有效的设计思想，具有较高的通用性和效率优势，但目前并没有一个框架可以对其精确进行描述及实现有效的模块化使用和替换.本文提出了一种模块化的Abstract-Refine算法框架，分析和解释了Abstract-Refine算法所接受的输入程序的精细结构和特性，并对Abstract-Refine算法和相关子算法运用平衡操作符做以模块化解耦，使得子算法的修改和更换不需要依赖对上层的变更.经过实验验证，本方法可有效实现传统算法模块化解耦，同时不对原算法的性能造成冲击.

	服务

	把本文推荐给朋友
	加入我的书架
	加入引用管理器
	E-mail Alert
	RSS
	作者相关文章
	王舜
	杜晔
	韩臻

关键词 ：软件模型检测, 模块化方法, 抽象&mdash, 精炼(Abstract-Refine), 通用算法, 抽象程序

Abstract：Abstract-Refine is a relatively effective method in the field of software model checking,which has the advantages of high generality and efficiency.However,there is no framework for precise description and effective modular use or replacement of this method so far.This paper introduces a modular Abstract-Refine algorithm framework which analyzes and explains the structure of input program in fine-grained level.Also,this method modularly decouples Abstract-Refine algorithm from its sub-algorithms with the balancing operator,so that any modifications on sub-algorithms will not affect the upper level.Experiments verify that our approach can effectively implement modular decoupling of traditional algorithms,and will not impact the performance of original algorithms.

Key words： software model checking modularity Abstract-Refine general algorithm abstract program

收稿日期: 2019-03-29

ZTFLH:

TP311.5

基金资助:国家自然科学基金（No.61672092）

作者简介: 王舜男,1988年生,河南洛阳人,北京交通大学博士生,主要研究方向为形式化方法、程序分析技术、信息安全等.E-mail:shunwang@bjtu.edu.cn;杜晔男,1978年生,黑龙江哈尔滨人,北京交通大学教授、博士生导师,主要研究方向为网络安全、态势感知、软件可靠性分析与评估等.E-mail:ydu@bjtu.edu.cn;韩臻男,1962年生,浙江宁波人,北京交通大学教授、博士生导师,主要研究方向为可信计算、系统安全、保密技术等.E-mail:zhan@bjtu.edu.cn

引用本文:

王舜, 杜晔, 韩臻. 基于模块化Abstract-Refine算法框架的软件模型检测方法[J]. 电子学报, 2020, 48(5): 997-1002. WANG Shun, DU Ye, HAN Zhen. Software Model Checking Method Based on Modular Abstract-Refine Algorithm Framework. Acta Electronica Sinica, 2020, 48(5): 997-1002.

链接本文:

http://www.ejournal.org.cn/CN/10.3969/j.issn.0372-2112.2020.05.022 或 http://www.ejournal.org.cn/CN/Y2020/V48/I5/997

[1] ALBARGHOUTHI A,GURFINKEL A,CHECHIK M.From under-approximations to over-approximations and back[A].Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)[C].Berlin:Springer,2012.157-172.
[2] BIERE A,CIMATTI A,CLARKE E M,et al.Bounded model checking[J].Advances in Computers,2003,58(11):117-148.
[3] FLANAGAN C,QADEER S.Predicate abstraction for software verification[A].ACM SIGPLAN Notices[C].NewYork:ACM.2002,37(1):191-202.
[4] RAJAMANI S K,GULAVANI B.Counterexample driven refinement for abstract interpretation[P].US Patent 7509534.2009-3-24.
[5] 魏欧,石玉峰,徐丙凤,等.软件模型检测中的抽象模型研究综述[J].计算机研究与发展,2015,52(7):1580-1603. WEI O,SHI Y,XU B,et al.Abstract modeling formalisms in software model checking[J].Journal of Computer Research and Development,2015,52(7):1580-1603.(in Chinese)
[6] SHVED P,MANDRYKIN M,MUTILIN V.Predicate analysis with BLAST 2.7[A].Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)[C].Berlin:Springer,2012.525-527.
[7] BALL T J,BOUNIMOVA E O,LEVIN V A,et al.Program analysis through predicate abstraction and refinement[P].US Patent 8402444.2013-3-19.
[8] FRIEDBERGER K.CPA-BAM:Block-abstraction memoization with value analysis and predicate analysis[A].Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016)[C].Berlin:Springer,2016.912-915.
[9] WONISCH D.Block abstraction memoization for CPAchecker[A].Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)[C].Berlin:Springer,2012.531-533.
[10] MCMILLAN K L.Interpolation:Proofs in the service of model checking[A].Handbook of Model-Checking[M].Berlin:Springer,2014.
[11] FEDYUKOVICH G,HYVARINEN A E J,SHARYGINA N.Interpolation-based model checking for efficient incremental analysis of software[A].Proceedings of IEEE 16th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS 2013)[C].IEEE,2013.8-9.
[12] VIZEL Y,GURFINKEL A,MALIK S.Fast interpolating BMC[A].Proceedings of International Conference on Computer Aided Verification (CAV 2015)[C].Cham:Springer,2015.641-657.
[13] BEYER D,LOWE S.Interpolation for value analysis[A].Proceedings of Software Engineering & Management[C].Bonn:Gesellschaft für Informatik,2015.73-74.
[14] 段钊,田聪,段振华.基于CEGAR的C程序空指针解引用检测[J].计算机研究与发展,2016,53(1):155-164. DUAN Z,TIAN C,DUAN Z.CEGARbased null-pointer dereference checking in C programs[J].Journal of Computer Research and Development,2016,53(1):155-164.(in Chinese)
[15] CIMATTI A,GRIGGIO A.Software model checking via IC3[A].Proceedings of International Conference on Computer Aided Verification (CAV 2012)[C].Berlin:Springer,2012.277-293.
[16] BEYER D,LOWE S.Explicit-state software model checking based on CEGAR and interpolation[A].Proceedings of International Conference on Fundamental Approaches to Software Engineering (FASE 2013)[C].Berlin:Springer,2013.146-162.
[17] Beyer D,Löwe S.Explicit-state software model checking based on CEGAR and interpolation[A].Proceedings of International Conference on Fundamental Approaches to Software Engineering (FASE 2013)[C].Berlin:Springer,2013.146-162.
[18] BEYER D,KEREMOGLU M E.CPAchecker:A tool for configurable software verification[A].Proceedings of International Conference on Computer Aided Verification (CAV 2011)[C].Berlin:Springer,2011.184-190.