中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 会议论文
Title:
fault localization through reasoning and sat solving
Author: Pu Fei
Source: Energy Procedia
Conference Name: 2011 International Conference on Energy and Environmental Science, ICEES 2011
Conference Date: October 14
Issued Date: 2011
Conference Place: Singapore, Singapore
Keyword: Environmental engineering ; Errors
Indexed Type: EI
ISSN: 1876-6102
Department: (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
Sponsorship: Singapore Institute of Electronics
Abstract: 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.
English Abstract: 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.
Language: 英语
Content Type: 会议论文
URI: http://ir.iscas.ac.cn/handle/311060/16273
Appears in Collections:软件所图书馆_会议论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
Pu Fei. fault localization through reasoning and sat solving[C]. 见:2011 International Conference on Energy and Environmental Science, ICEES 2011. Singapore, Singapore. October 14.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Pu Fei]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Pu Fei]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2021  中国科学院软件研究所 - Feedback
Powered by CSpace