Automated Model Repair for Alloy
Automated Model Repair for Alloy
复制标题
DOI：
10.1145/3238147.3238162
复制
发表时间：
2018-09
期刊：
影响因子：
--
通讯作者：
Kaiyuan Wang;Allison Sullivan;S. Khurshid
中科院分区：
文献类型：
--
作者：
Kaiyuan Wang;Allison Sullivan;S. Khurshid
自动程序修复是一个活跃的研究领域。然而，现有的研究主要集中在命令式代码上，例如在Java中。本文研究了Alloy -一种具有传递闭包的一阶关系逻辑中声明模型的修复问题。我们介绍ARepair，修复合金模型的第一种技术。ARepair遵循传统的自动程序修复技术的精神。具体来说，APrepair将一个有故障的Alloy模型和一个包含一些失败测试的测试套件作为输入，并输出一个相对于给定测试正确的修复模型。ARepair集成了突变测试和程序合成的思想，为修复Alloy模型提供了有效的解决方案。实验结果表明，ARepair可以修复我们收集的38个真实世界的错误模型中的28个。
Automated program repair is an active research area. However, existing research focuses mostly on imperative code, e.g. in Java. In this paper, we study the problem of repairing declarative models in Alloy - a first order relational logic with transitive closure. We introduce ARepair, the first technique for repairing Alloy models. ARepair follows the spirit of traditional automated program repair techniques. Specifically, ARepair takes as input a faulty Alloy model and a test suite that contains some failing test, and outputs a repaired model that is correct with respect to the given tests. ARepair integrates ideas from mutation testing and program synthesis to provide an effective solution for repairing Alloy models. The experimental results show that ARepair can fix 28 out of 38 real-world faulty models we collected.