Fault Localization for Declarative Models in Alloy
Kaiyuan Wang, Allison Sullivan, Darko Marinov, Sarfraz Khurshid · 2020
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 AlloyFLhy, the first fault localization technique for faulty Alloy models which leverages multiple test formulas. AlloyFLhybrings the traditional spectrum-based and mutation-based fault localization techniques to Alloy and combines both techniques to locate faults. To measure the effectiveness of AlloyFLhy, we define three distance metrics and use both distance-based and top-k metrics to measure the effectiveness of AlloyFLhyon 90 real faulty models. The results show that AlloyFLhy is substantially more effective than Alloy's built-in unsat core.