Assumption-based Reasoning with Constraints for Diagnosing Program Faults
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 advantage 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 statements) is (are) faulty. Some constraints will be introduced from the specifications of the program. Moreover, we transform the counterexample into a prepositional 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 satisfiable, 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.
fault diagnosing assumption-based reasoning model checking constraint counterexample
Fei Pu
College of Computer and Information Engineering Zhejiang Gongshang University Hangzhou, China
国际会议
重庆
英文
456-462
2011-01-21（万方平台首次上网日期，不代表论文的发表时间）