Fault Localization for Declarative Models in Alloy
Fault Localization for Declarative Models in Alloy
复制标题
DOI：
10.1109/issre5003.2020.00044
复制
发表时间：
2018-07
期刊：
影响因子：
--
通讯作者：
Kaiyuan Wang;Allison Sullivan;D. Marinov;S. Khurshid
中科院分区：
文献类型：
--
作者：
Kaiyuan Wang;Allison Sullivan;D. Marinov;S. Khurshid
故障本地化是一个流行的研究主题，已经提出了许多技术来定位命令式代码，例如C和Java。闭合，我们引入了合金的第一个故障合金模型，以利用多个测试公式。合金，我们定义三个距离指标，并同时使用基于距离的指标和TOP-K指标来测量合金对90个实际故障模型的有效性。
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. AlloyFLhy 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 AlloyFLhy, we define three distance metrics and use both distance-based and top-k metrics to measure the effectiveness of AlloyFLhy on 90 real faulty models. The results show that AlloyFLhy is substantially more effective than Alloy’s built-in unsat core.