Fault Localization for Declarative Models in Alloy

Fault localization is a popular research topic and many techniques have been proposed to locate faults in imperative code, e.g. C and Java. In this paper, we focus on the problem of fault localization for declarative models in Alloy - a first order relational logic with transitive closure. We introduce AlloyFL hy , the first fault localization technique for faulty Alloy models which leverages multiple test formulas. AlloyFL hy brings the traditional spectrum-based and mutation-based fault localization techniques to Alloy and combines both techniques to locate faults. To measure the effectiveness of AlloyFL hy , we define three distance metrics and use both distance-based and top-k metrics to measure the effectiveness of AlloyFL hy on 90 real faulty models. The results show that AlloyFLhy is substantially more effective than Alloy's built-in unsat core.