Institutional Repository
| fault localization through reasoning and sat solving | |
| Pu Fei | |
| 2011 | |
| Conference Name | 2011 International Conference on Energy and Environmental Science, ICEES 2011 |
| Source | Energy Procedia |
| Pages | 1354-1363 |
| Conference Date | October 14 |
| Conference Place | Singapore, Singapore |
| 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 |
| 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.; 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. |
| Keyword | Environmental Engineering Errors |
| Sponsorship | Singapore Institute of Electronics |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16273 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Pu Fei. fault localization through reasoning and sat solving[C],2011:1354-1363. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment