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

doi:10.3969/j.issn.0372-2112.2020.05.022

电子学报 ›› 2020, Vol. 48 ›› Issue (5): 997-1002.DOI: 10.3969/j.issn.0372-2112.2020.05.022

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

王舜, 杜晔, 韩臻

北京交通大学计算机与信息技术学院, 北京 100044

收稿日期:2019-03-29 修回日期:2019-09-02 出版日期:2020-05-25
- 作者简介:
- 王舜男,1988年生,河南洛阳人,北京交通大学博士生,主要研究方向为形式化方法、程序分析技术、信息安全等.E-mail:shunwang@bjtu.edu.cn;杜晔男,1978年生,黑龙江哈尔滨人,北京交通大学教授、博士生导师,主要研究方向为网络安全、态势感知、软件可靠性分析与评估等.E-mail:ydu@bjtu.edu.cn;韩臻男,1962年生,浙江宁波人,北京交通大学教授、博士生导师,主要研究方向为可信计算、系统安全、保密技术等.E-mail:zhan@bjtu.edu.cn
- 基金资助:
- 国家自然科学基金 (No.61672092）

Software Model Checking Method Based on Modular Abstract-Refine Algorithm Framework

WANG Shun, DU Ye, HAN Zhen

School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China

Received:2019-03-29 Revised:2019-09-02 Online:2020-05-25 Published:2020-05-25
- Supported by:
- National Natural Science Foundation of China (No.61672092)

摘要/Abstract

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

关键词: 软件模型检测, 模块化方法, 抽象—精炼(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

中图分类号:

TP311.5

王舜, 杜晔, 韩臻. 基于模块化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[J]. Acta Electronica Sinica, 2020, 48(5): 997-1002.

参考文献

[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.

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

Software Model Checking Method Based on Modular Abstract-Refine Algorithm Framework

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	薄莉莉, 朱程, 李斌, 孙小兵. 文件信息增强的方法级软件缺陷定位[J]. 电子学报, 2023, 51(3): 613-621.
[2]	李雪莹, 王田路, 梁鹏, 王翀. 基于系统模型的用户评论中非功能需求的自动分类[J]. 电子学报, 2022, 50(9): 2079-2089.
[3]	史先进, 曹爽, 张重生, 陶月锋, 吕灵灵, 沈夏炯. 基于锚点的字符级甲骨图像自动标注算法研究[J]. 电子学报, 2021, 49(10): 2020-2031.
[4]	李斌, 陈定山, 孙小兵, 薄莉莉. 面向缺陷知识的多特征匹配搜索算法[J]. 电子学报, 2021, 49(4): 661-664.
[5]	黄子杰, 陈军华, 高建华. Code Smell视角下分层Web应用失血及充血现象的量化分析[J]. 电子学报, 2020, 48(4): 772-780.
[6]	潘伟丰, 宋贝贝, 胡博, 李兵, 姜波. 基于软件网络加权k-核分析的关键类识别方法[J]. 电子学报, 2018, 46(5): 1071-1077.
[7]	赵祖威, 冯世宁, 汤恩义, 陈鑫, 李宣东, 潘敏学, 赵晨. 一种符号执行制导的循环内界分析方法[J]. 电子学报, 2017, 45(11): 2582-2592.
[8]	薛猛, 姜淑娟, 张争光, 钱俊彦, 张艳梅, 曹鹤玲. 一种基于Kalman滤波和粒子群优化的测试数据生成方法[J]. 电子学报, 2017, 45(10): 2473-2483.
[9]	朱瑞瑾, 张宝峰, 毛军捷, 骆扬, 谭毓安, 张全新. 一种基于匹配字符串地址判定ARM固件装载基址的方法[J]. 电子学报, 2017, 45(6): 1475-1482.
[10]	李勇, 黄志球, 王勇, 房丙午. 数据驱动的软件缺陷预测研究综述[J]. 电子学报, 2017, 45(4): 982-988.
[11]	田刚, 何克清, 王健, 孙承爱, 徐建建. 面向领域标签辅助的服务聚类方法[J]. 电子学报, 2015, 43(7): 1266-1274.
[12]	张龙昌, 杨艳红, 赵绪辉. 基于云模型的SaaS决策方法[J]. 电子学报, 2015, 43(5): 987-992.
[13]	李庆新, 刘淑芬, 曲明. 基于本体的Web服务行为语义建模方法[J]. 电子学报, 2015, 43(3): 601-604.
[14]	潘伟丰, 李兵, 马于涛, 姜波. 基于加权PageRank算法的关键包识别方法[J]. 电子学报, 2014, 42(11): 2174-2183.
[15]	黄贻望, 何克清, 冯在文, 黄颖. 一种目标感知的可配置业务流程分析方法[J]. 电子学报, 2014, 42(10): 2060-2068.