位置:成果数据库 > 期刊 > 期刊详情页
基于插桩和布尔逻辑的运行时程序验证框架
  • ISSN号:1000-3428
  • 期刊名称:《计算机工程》
  • 时间:0
  • 分类:TP311[自动化与计算机技术—计算机软件与理论;自动化与计算机技术—计算机科学与技术]
  • 作者机构:[1]中国科学技术大学计算机科学与技术学院,合肥230027, [2]安徽省计算与通讯软件重点实验室,合肥230027, [3]中国科学技术大学中国科学院沈阳计算技术研究所网络与通信联合实验室,合肥230027
  • 相关基金:“核高基”重大专项(2009ZX01028-002-003-005); 国家自然科学基金资助项目(60833004); 高等学校学科创新引智计划基金资助项目(B07033)
中文摘要:

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

英文摘要:

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.

同期刊论文项目
期刊论文 75 会议论文 63 专利 12
同项目期刊论文
期刊信息
  • 《计算机工程》
  • 北大核心期刊(2014版)
  • 主管单位:中国电子科技集团公司
  • 主办单位:华东计算技术研究所 上海市计算机学会
  • 主编:游小明
  • 地址:上海市桂林路418号
  • 邮编:200233
  • 邮箱:ecice06@ecict.com.cn
  • 电话:021-64846769
  • 国际标准刊号:ISSN:1000-3428
  • 国内统一刊号:ISSN:31-1289/TP
  • 邮发代号:4-310
  • 获奖情况:
  • 1999~2000、2001~2002年度信息产业部优秀期刊奖,2003-2004、2005-2006年度信息产业部电子精品科技...,2007-2008、2009-2010年度工业和信息产业部电子精...,012年度中国科技论文在线优秀期刊一等奖,2013年度中国科技论文在线优秀期刊二等奖
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,美国化学文摘(网络版),波兰哥白尼索引,荷兰文摘与引文数据库,美国剑桥科学文摘,英国科学文摘数据库,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2014版),中国北大核心期刊(2000版)
  • 被引量:84139