Localizing Program Errors via Slicing and Reasoning
Model-based program debugging exploits discrepancies between the program behavior anticipated by a programmer and the programs actual behavior when executed on a set of inputs. From symptoms exhibited by a failing trace,potential culprits in the program can be localized. However, since the cause of the error is nested deeper into the code than the error itself, localizing errors and correcting the errors are most time consuming hard work. The error trace produced by a model checker may contain more information than it appears. 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. In order to reduce the time consuming for error localizing, we first use dynamic program slicing to localize several statements to account for the violation of property.Assumption among these statements is then made to point out which statement(s) is (are)faulty. Some constraints will be introduced from the properties which are model checked for the program. A calculus of reasoning with these constraints is processed under the assumption along a counterexample. If the result may be consistent, the assumption is true (we can localize errors in those statements which the assumption suppose them to be faulty), otherwise, the assumption is wrong and another assumption should be mode.Some examples support the applicability and effectiveness of our approach.
Fei Pu Yan Zhang
Intelligent Systems Laboratory School of Computing and Mathematics University of Western Sydney, Australia
国际会议
11th IEEE High Assurance Systems Engineering Symposium(HASE 2008)(第十一届IEEE高可信系统工程国际研讨会)
南京
英文
187-196
2008-12-03（万方平台首次上网日期，不代表论文的发表时间）