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.