A Practical Study of Debugging Using Model Checking

Debugging is one of the most time-consuming tasks in software development. The application of a model-checking technique in debugging has strong potential to solve this problem. Here, lessons learned through our practical experiences with POM/MC are discussed. The aim of this proposed hypothesis-based method of debugging is not only to reproduce a failure as counterexamples, but also to obtain a counterexample that is useful for detecting the fault or the cause of the failure. One of the characteristics of the proposed approach is that it degenerates a source code in order to clarify the fault. An example of this degeneration shows that the method is useful for fault analysis and avoidance of the "state-explosion" problem. Furthermore, the characteristics of debugging using POM/MC are explained from the viewpoint of debugging hypotheses.