Model-based diagnosis versus error explanation

摘要

Debugging techniques assist a developer in localizing and correcting faults in a system's description when the behavior of the system does not conform to its specification. Two fault localization techniques are model-based diagnosis and error explanation. Model-based diagnosis computes a subset of the system's components which when replaced correct the system. Error explanation determines potential causes of the system's misbehavior by comparing faulty and correct execution traces. In this paper we focus on fault localization for imperative, non-concurrent programs. We compare the two fault localization techniques in a unified setting presenting SAT-based algorithms for both. The algorithms serve as a vantage point for a fair comparison and allow for efficient implementations leveraging state-of-the-art decision procedures. Firstly, in our comparison we use constructed programs to study strengths and weaknesses of the two fault localization techniques. We show that in general none of the fault localization techniques is superior but that the computed fault candidates depend on the program structure. Secondly, we implement the SAT-based algorithms in a prototype tool utilizing a Satisfiability Modulo Theories (SMT) solver and evaluate them on mutants of the ANSI-C program TCAS from the Software-Artifact Infrastructure Repository (SIR).