Fault Localization for Declarative Models in Alloy
Kaiyuan Wang, Allison Sullivan, Darko Marinov, Sarfraz Khurshid
Abstract
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 <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">hy</sub> , the first fault localization technique for faulty Alloy models which leverages multiple test formulas. AlloyFL <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">hy</sub> 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 <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">hy</sub> , we define three distance metrics and use both distance-based and top-k metrics to measure the effectiveness of AlloyFL <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">hy</sub> on 90 real faulty models. The results show that AlloyFLhy is substantially more effective than Alloy's built-in unsat core.