基于插桩和布尔逻辑的运行时程序验证框架

doi:10.3969/j.issn.1000-3428.2013.01.006

计算机工程 ›› 2013, Vol. 39 ›› Issue (1): 29-34. doi: 10.3969/j.issn.1000-3428.2013.01.006

基于插桩和布尔逻辑的运行时程序验证框架

李业华^1,2,3，顾乃杰 ^1,2,3，张颖楠 ^1,2,3，彭飞 ^1,2,3

(1. 中国科学技术大学计算机科学与技术学院，合肥 230027；2. 安徽省计算与通讯软件重点实验室，合肥 230027；3. 中国科学技术大学中国科学院沈阳计算技术研究所网络与通信联合实验室，合肥 230027)

收稿日期:2012-04-10 修回日期:2012-05-08 出版日期:2013-01-15 发布日期:2013-01-13
作者简介:李业华(1986－)，男，硕士研究生、CCF会员，主研方向：程序验证，网络负载均衡；顾乃杰，博士、博士生导师；张颖楠，硕士；彭飞，博士
基金资助:
“核高基”重大专项(2009ZX01028-002-003-005)；国家自然科学基金资助项目(60833004)；高等学校学科创新引智计划基金资助项目(B07033)

Runtime Program Verification Framework Based on Instrumentation and Boolean Logic

LI Ye-hua ^1,2,3, GU Nai-jie ^1,2,3, ZHANG Ying-nan^1,2,3, PENG Fei ^1,2,3

(1. School of Computer Science and Technology, University of Science and Technology of China, Hefei 230027, China; 2. Anhui Province Key Laboratory of Computing and Communication Software, Hefei 230027, China; 3. Network and Communication Joint Laboratory, USTC&SICT, Hefei 230027, China)

Received:2012-04-10 Revised:2012-05-08 Online:2013-01-15 Published:2013-01-13

摘要/Abstract

摘要：

针对软件测试和静态程序验证中存在的连续性程序执行验证和推理问题，提出一个基于程序插桩和布尔逻辑的运行时程序验证框架——RPA。定义一种用于描述运行时程序性质和规范的动态逻辑语言RPAL，实现自动化插桩以收集运行时程序状态信息，设计一个支持高效验证的句子调度算法。实验结果表明，结合合适的谓词扩展，RPA可以有效地验证和分析软件逻辑，发现潜在的软件错误。

关键词: RPA框架, RPAL语言, 运行时程序验证, 程序插桩, 布尔逻辑, 事实推理

Abstract:

Continuously verifying and reasoning on software’s execution property are notoriously hard to solve by general software test and static program verification. Aiming at the problems, this paper proposes a runtime program verification framework named RPA based on program instrumentation and Boolean logic. RPA defines a dynamic logic language which describes and asserts runtime properties of target program, proposes an automatic instrumentation approach to collect state information in runtime program, and designs a scheduling algorithm to support fast verification and reasoning. Experimental results show that combined with appropriate predicate extensions, RPA can effectively verify and analyze the software logic, to identify potential software errors.

Key words: RPA framework, RPAL language, runtime program verification, program instrumentation, Boolean logic, fact reasoning

中图分类号:

TP311

李业华, 顾乃杰, 张颖楠, 彭飞. 基于插桩和布尔逻辑的运行时程序验证框架[J]. 计算机工程, 2013, 39(1): 29-34.

LI Ye-Hua, GU Ai-Jie, ZHANG Ying-Nan, BANG Fei. Runtime Program Verification Framework Based on Instrumentation and Boolean Logic[J]. Computer Engineering, 2013, 39(1): 29-34.

http://www.ecice06.com/CN/Y2013/V39/I1/29

参考文献

[1] 梁睿. 基于运行时验证的AOP程序检测框架研究[D]. 兰州: 兰州大学, 2009.
[2] Aiken A, Bugrara S, Dillig I, et al. Saturn Project[EB/OL]. [2012-03-01]. http://saturn.stanford.edu.
[3] Killian C, Anderson J W, Jhala R, et al. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code[C]//Proc. of NSDI’07. Cambridge, USA: [s. n.], 2007.
[4] Aiken A, Bugrara S, Dillig I, et al. An Overview of the Saturn Project[C]//Proc. of PASTE’07. San Diego, USA: [s. n.], 2007.
[5] Aiken A, Bugrara S, Dillig I, et al. The Saturn Program Analysis System[EB/OL]. [2012-03-01]. http://saturn. stanford.edu.
[6] Reynolds P, Killian C, Wiener J L, et al. Pip: Detecting the Unexpected in Distributed Systems[C]//Proc. of NSDI’06. San Jose, USA: [s. n.], 2006.
[7] Liu Xuezheng, Guo Zhenyu, Wang Xi, et al. D3S: Debug Deployed Distributed System[C]//Proc. of NSDI’08. San Francisco, USA: [s. n.], 2008.
[8] Killian C E, Anderson J W, Braud R. Mace: Language Support for Building Distributed Systems[C]//Proc. of PLDI’07. San Diego, USA: [s. n.], 2007.
[9] Yang Junfeng, Chen Tisheng, Wu Ming, et al. MODIST: Transparent Model Checking of Unmodified Distributed Systems[C]//Proc. of NSDI’09. Boston, USA: [s. n.], 2009.
[10] Yabandeh M, Knezevic N, Kostic D, et al. CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems[C]//Proc. of NSDI’09. Boston, USA: [s. n.], 2009.
[11] Pnueli A. The Temporal Logic of Programs[C]//Proc. of the 18th IEEE Symposium on Foundation of Computer Science. [S. l.]: IEEE Computer Society, 1977.
[12] Shende S S, Malony A D. The Tau Parallel Performance System[J]. International Journal of High Performance Computing Applications, 2006, 20(2): 287-311.
[13] Shende S S, Malony A D. Pdtoolkit Project[EB/OL]. [2012-03-01]. http://www.cs.uoregon.edu/Research/tau/do wnloads.php.
[14] Luk Chi-Keung, Cohn R, Muth R, et al. Pin: Building Customized Program Analysis Tools with Dynamic Instrumentation[C]//Proc. of PLDI’05. Chicago, USA: [s. n.], 2005.
[15] Tarreau W. Haproxy Project: The Reliable, High Perfor- mance TCP/HTTP Load Balancer[EB/OL]. [2012-03-01]. http://haproxy.1wt.eu.

选择文件类型/文献管理软件名称

选择包含的内容

基于插桩和布尔逻辑的运行时程序验证框架

Runtime Program Verification Framework Based on Instrumentation and Boolean Logic

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 4

编辑推荐

Metrics

本文评价

[1]	孙家泽, 易刚, 舒新峰. 基于Adaboost模型的并发程序数据竞争语句级检测[J]. 计算机工程, 2021, 47(12): 215-220.
[2]	王轶, 蒋同海, 董军, 周喜. 基于路径覆盖插桩的可执行代码测试工具实现[J]. 计算机工程, 2012, 38(5): 35-37,40.
[3]	郭宁, 冯萍, 康继昌. 基于布尔逻辑的双序列搜索比对算法[J]. 计算机工程, 2011, 37(23): 205-207.
[4]	于全喜;张毅坤;胡燕京;朱伟. 嵌入式软件路径覆盖测试数据采集[J]. 计算机工程, 2009, 35(21): 54-56,5.

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

基于插桩和布尔逻辑的运行时程序验证框架

Runtime Program Verification Framework Based on Instrumentation and Boolean Logic

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 4

编辑推荐

Metrics

本文评价