fault localization through reasoning and sat solving

ISCAS OpenIR

	fault localization through reasoning and sat solving
	Pu Fei
	2011
会议名称	2011 International Conference on Energy and Environmental Science, ICEES 2011
会议录名称	Energy Procedia
页码	1354-1363
会议日期	October 14
会议地点	Singapore, Singapore
收录类别	EI
ISSN	1876-6102
部门归属	(1) College of Computer and Information Engineering Zhejiang Gongshang University Hangzhou 310018 China; (2) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing 100190 China
摘要	Model checking is an efficient technique for detecting errors of a system. However diagnosing program faults are most time consuming hard work. One of the major advantages of model checking is the production of a counterexample when a property violation is detected. The error trace produced by a model checker may exhibit the symptom related to the cause of errors. Thus, counterexamples can be enough and are indicative for the cause of violation of the property. We present an assumption-based approach to localize the cause of a property violation using reasoning with constraints. The assumption among the statements in counterexample is made to point out which statement(s) is (are) faulty. Some constraints will be introduced from the specifications of the program. Moreover, we transform the counterexample into a propositional logic formula which is then fed to a SAT solver or a theorem prover together with constraints. A calculus of reasoning with these constraints proceeds under a certain assumption. If the result is satisfied, the assumption is correct (we localize errors in those statements which the assumption suppose them to be faulty), otherwise, the assumption is wrong and another assumption should be made. Some examples support the applicability and effectiveness of our approach. © 2011 Published by Elsevier Ltd.; Model checking is an efficient technique for detecting errors of a system. However diagnosing program faults are most time consuming hard work. One of the major advantages of model checking is the production of a counterexample when a property violation is detected. The error trace produced by a model checker may exhibit the symptom related to the cause of errors. Thus, counterexamples can be enough and are indicative for the cause of violation of the property. We present an assumption-based approach to localize the cause of a property violation using reasoning with constraints. The assumption among the statements in counterexample is made to point out which statement(s) is (are) faulty. Some constraints will be introduced from the specifications of the program. Moreover, we transform the counterexample into a propositional logic formula which is then fed to a SAT solver or a theorem prover together with constraints. A calculus of reasoning with these constraints proceeds under a certain assumption. If the result is satisfied, the assumption is correct (we localize errors in those statements which the assumption suppose them to be faulty), otherwise, the assumption is wrong and another assumption should be made. Some examples support the applicability and effectiveness of our approach. © 2011 Published by Elsevier Ltd.
关键词	Environmental Engineering Errors
主办者	Singapore Institute of Electronics
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16273
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Pu Fei. fault localization through reasoning and sat solving[C],2011:1354-1363.