结合Craig插值分析的软件错误诊断方法

doi:10.3969/j.issn.0372-2112.2016.10.033

电子学报 ›› 2016, Vol. 44 ›› Issue (10): 2514-2521.DOI: 10.3969/j.issn.0372-2112.2016.10.033

结合Craig插值分析的软件错误诊断方法

徐勇^1,2, 毋国庆¹, 袁梦霆¹

1. 武汉大学计算机学院, 湖北武汉 430072;
2. 广东肇庆学院数学与统计学院, 广东肇庆 526061

收稿日期:2015-11-03 修回日期:2016-02-16 出版日期:2016-10-25
- 作者简介:
- 徐勇,男,1977年生,博士生,主要研究方向为软件工程、软件调试.E-mail:xyus@whu.edu.cn;毋国庆,男,1954年生,教授、博士生导师,主要研究领域为软件需求工程、形式化方法.E-mail:wgq@whu.edu.cn
- 基金资助:
- 国家自然科学基金 (No.91118003，No.61003071）; 深圳战略性新兴产业发展专项资金 (No.JCYJ20120616135936123）; 中央高校基本科研业务费专项资金 (No.3101046，No.201121102020006）

Software Fault Localization Based on Model-Based Diagnosis Combined Craig Interpolant Analysis

XU Yong^1,2, WU Guo-qing¹, YUAN Meng-ting¹

1. Computer School, Wuhan University, Wuhan, Hubei 430072, China;
2. School of Mathematics and Statistics, Zhaoqing University, Zhaoqing, Guangdong 526061, China

Received:2015-11-03 Revised:2016-02-16 Online:2016-10-25 Published:2016-10-25

摘要/Abstract

摘要：

基于模型诊断（MBD）的理论应用到软件错误定位中取得了一定的效果.但是经典MBD理论基于元件间独立地发生故障这一假设，导致软件错误定位的结果中存在假阳性的诊断.论文对现有基于MBD的软件错误定位方法进行了改进，提出了冲突中元件的冗余分析方法.该方法既包括了基于Craig插值的元件冗余分析机制，同时利用条件语句取值的二元性（真或假）的特点，对冲突中的条件语句元件进行软件错误的无相关分析.实验结果表明：冲突中的元件冗余分析方法可以有效地减少诊断的假阳性率，将诊断结果数减少了48.4%，碰集树生成的结点数减少了47.6%.

关键词: 基于模型诊断, 软件错误定位, 冗余分析, Craig插值

Abstract:

Model-based diagnosis,an intelligent diagnosis theory has been successfully applied in software fault localization with promising results.However,traditional MBD relies on the assumption that components in the system fail dependently which makes the diagnoses with high false positives in software fault localization.In this paper,a component redundancy analysis approach is presented.The approach not only uses Craig interpolant to filter redundant components,but also employs a fact that a branch predicate evaluates to either true or false to filter some branch condition components.Experimental results show that the proposed approach effectively reduces the false positive rates of diagnoses,i.e.,reducing the number of diagnosis by 48.4%,and reducing the number of nodes of hitting set tree generated during diagnosis computation by 47.6%.

Key words: model-based diagnosis (MBD), fault localization, redundancy analysis, Craig interpolant

中图分类号:

TP311

徐勇, 毋国庆, 袁梦霆. 结合Craig插值分析的软件错误诊断方法[J]. 电子学报, 2016, 44(10): 2514-2521.

XU Yong, WU Guo-qing, YUAN Meng-ting. Software Fault Localization Based on Model-Based Diagnosis Combined Craig Interpolant Analysis[J]. Acta Electronica Sinica, 2016, 44(10): 2514-2521.

参考文献

[1] Lee Naish,Hua Jie Lee,Kotagiri Ramamohanarao.A model for spectra-based software diagnosis [J].ACM Transactions on software engineering and methodology (TOSEM),2011,20(3):11.
[2] Rui Abreu,Peter Zoeteweij,Rob Golsteijn,Arjan J C Van Gemund.A practical evaluation of spectrum-based fault localization [J].Journal of Systems and Software,2009,82(11):1780-1792.
[3] Konighofer R,Roderick Bloem.Automated error localization and correction for imperative programs [A].Formal Methods in Computer-Aided Design (FMCAD) [C].USA:IEEE,2011,91-100.
[4] Rui Abreu,Arjan J C Van Gemund.Diagnosing multiple intermittent failures using maximum likelihood estimation [J].Artificial Intelligence,2010,174(18):1481-1497.
[5] Chao Liu,Long Fei,Xifeng Yan,Jiawei Han,Samuel P Midkiff.Statistical debugging:A hypothesis testing-based approach [J].IEEE Transactions on Software Engineering,2006,32(10):831-848.
[6] Dennis Jeffrey,R Gupta.Effective and efficient localization of multiple faults using value replacement [A].IEEE International Conference on Software Maintenance [C].USA:IEEE,2009.221-230.
[7] Andreas Zeller,Ralf Hildebrandt.Simplifying and isolating failure-inducing input [J].IEEE Transactions on Software Engineering,2002,28(2):183-200.
[8] Swarup Kumar Sahoo,John Criswell,Chase Geigle,Vikram Adve.Using likely invariants for automated software fault localization [J].ACM SIGARCH Computer Architecture News,2013,41(1):139-152.
[9] 王建峰,魏长安,盛云龙,等.基于错误交互集的组合测试软件故障定位方法[J].电子学报,2014,42(6):1173-1178. WANG Jian-feng,WEI Chang-an,et al.Locating errors in combinatorial testing using set of possible faulty interactions [J].Acta Electronica Sinica,2014,42(6):1173-1178.(in Chinese)
[10] Raymond Reiter.A theory of diagnosis from first principles [J].Artificial intelligence,1987,32(1):57-95.
[11] Rui Abreu,Peter Zoeteweij,Arjan J C van Gemund.An observation-based model for fault localization [A].Proceedings of the International Workshop on Dynamic Analysis [C].USA:ACM,2008.64-70.
[12] Franz Wotawa,Mihai Nica,Iulia Moraru.Automated debugging based on a constraint model of the program and a test case [J].The Journal of Logic and Algebraic Programming,2012,81(4):390-407.
[13] Birgit Hofer,Franz Wotawa.Combining slicing and constraint solving for better debugging:The conbas approach [A].Advances in Software Engineering [C].Hindawi Publishing Corporation,2012.Article ID 628571.
[14] Jorg Weber, Franz Wotawa.Diagnosing dependent failures in the hardware and software of mobile autonomous robots [A].New Trends in Applied Artificial Intelligence [C].Berlin:Springer,2007.633-643.
[15] William Craig.Linear reasoning.a new form of the herbrand-gentzen theorem [J].The Journal of Symbolic Logic,1957,22(3):250-268.
[16] Evren Ermis,Martin Schaf,Thomas Wies.Error invariants [A].Lecture Notes in Computer Science:Formal Methods (Volume 7436) [C].Berlin:Springer,2012.187-201.
[17] 陈祖希,徐中伟,霍伟伟,等.基于 Craig插值的线性混成系统符号化模型检测[J].电子学报,2014,42(7):1338-1346. CHEN Zu-xi,XU Zhong-wei,et al.Symbolic model checking for linear hybrid systems base on craig interpolation [J].Acta Electronica Sinica,2014,42(7):1338-1346.(in Chinese)
[18] Xiangyu Zhang,Neelam Gupta,Rajiv Gupta.Locating faults through automated predicate switching [A].Proceedings of the 28th International Conference on Software Engineering [C].USA:ACM,2006.272-281.
[19] Jurgen Christ,Evren Ermis,Martin Schaf,Thomas Wies.Flow-sensitive fault localization [A].Verification,Model Checking,and Abstract Interpretation [C].Brelin:Springer,2013.189-208.
[20] Leonardo De Moura,Nikolaj Bj? rner.Z3:An efficient smt solver [A].Tools and Algorithms for the Construction and Analysis of Systems [C].Berlin:Springer,2008.337-340.

结合Craig插值分析的软件错误诊断方法

Software Fault Localization Based on Model-Based Diagnosis Combined Craig Interpolant Analysis

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 6

编辑推荐

Metrics

[1]	赵相福, 黄森, 童向荣, 欧阳丹彤, 张立明, 章星林. IBWIICC:结合局部独立覆盖检测策略增量求解极小碰集的算法[J]. 电子学报, 2022, 50(11): 2722-2729.
[2]	欧阳丹彤, 刘伯文, 刘梦, 张立明, 张永刚. 结合电路结构基于分块的诊断方法[J]. 电子学报, 2018, 46(7): 1571-1577.
[3]	欧阳丹彤, 刘伯文, 周建华, 张立明. 结合问题特征利用SE-Tree反向深度求解冲突集的方法[J]. 电子学报, 2017, 45(5): 1175-1181.
[4]	陈祖希, 徐中伟, 霍伟伟, 喻钢. 基于Craig插值的线性混成系统符号化模型检测[J]. 电子学报, 2014, 42(7): 1338-1346.
[5]	郭旭峰, 于芳, 刘忠立. 基于哈希表的高效存储器内建自修复方法[J]. 电子学报, 2013, 41(7): 1371-1377.
[6]	俞洋;李嘉铭;乔立岩. 基于地址分割的嵌入式存储器内建自修复方法[J]. 电子学报, 2010, 38(2A): 169-173.