电子学报 ›› 2016, Vol. 44 ›› Issue (5): 1040-1050.DOI: 10.3969/j.issn.0372-2112.2016.05.005

• 学术论文 • 上一篇    下一篇

基于符号执行的能耗错误检测方法

徐超1, 陈勇2, 葛红美1, 何炎祥3   

  1. 1. 南京审计大学, 江苏南京 210029;
    2. 中国电子科技集团第十四研究所, 江苏南京 210013;
    3. 武汉大学计算机学院, 湖北武汉 430072
  • 收稿日期:2015-09-27 修回日期:2016-01-04 出版日期:2016-05-25 发布日期:2016-05-25
  • 通讯作者: 陈勇
  • 作者简介:徐超 男,1980年出生,湖北红安人,博士,副教授,研究方向为可信软件、嵌入式系统和计算机审计.E-mail:xuchao@nau.edu.cn
  • 基金资助:

    国家自然科学基金(No.61170022);江苏省高校自然科学研究面上项目(No.15KJB520019);江苏省"六大人才"高峰项目资助;江苏省高校"青蓝工程"优秀青年骨干教师培养对象资助;江苏高校优势学科建设工程资助项目

Symbolic Execution Based Energy Bug Detecting Method

XU Chao1, CHEN Yong2, GE Hong-mei1, HE Yan-xiang3   

  1. 1. Nanjing Audit University, Nanjing, Jiangsu 210029, China;
    2. The 14th Research Institute of CETC, Nanjing, Jiangsu 210013, China;
    3. Computer School of Wuhan University, Wuhan, Hubei 430072, China
  • Received:2015-09-27 Revised:2016-01-04 Online:2016-05-25 Published:2016-05-25

摘要:

能耗是制约便携式智能设备发展的重要瓶颈.随着嵌入式操作系统的广泛应用,因不能合理使用操作系统的API而导致的能耗错误已经成为各种嵌入式应用开发过程中不容忽视的因素.为减少应用中的能耗错误,以符号执行技术为基础,根据禁止休眠类能耗错误的特点,设计了对应的能耗错误检测方法.该方法首先利用过程内分析,获得单个函数的符号执行信息.然后借助过程间分析对单个函数的符号执行信息进行全局综合,得到更为精确的执行开销、锁变量匹配等相关信息,以更好的检测能耗错误.同时,符号执行记录了对应的分支路径信息,利用该信息能够结合约束求解器较为方便的生成出错的测试用例,进而定位错误位置.通过示例和实验,验证了该方法在能耗错误检测方面的可行性和有效性.

关键词: 能耗错误, 符号执行, 错误检测, 过程内分析, 过程间分析

Abstract:

Energy is one important bottleneck to the development of intelligent portable device.With the wide use of embedded operation system, the energy bug caused by unsuitablely using the API of the operation system has become the important factor in the designment of the embedded application.According to the characteristics of the No-Sleeping energy bug, a symbolic execution based energy bug detecting method is proposed to reduce the energy bug.It first uses intraprocedural analysis technology to analyze one function independently to get the energy information of the function.Then, the interprocedural analysis technology is applied to get the globe analysis of the program by the information of intraprocedural analysis which can get more accuate information for energy bug detection.Meanwhile, constraint solver can be combined to obtain the counter-example for locating the position of the error.Example and experiment results verify that the method is feasible and effective in energy bug detection.

Key words: energy bug, symbolic execution, bug detection, intraprocedural analysis, interprocedural analysis

中图分类号: