一句话:提出首个 Alloy 模型自动修复技术 ARepair,融合变异测试与程序合成,修复 28/38 个真实缺陷模型。
自动程序修复已有大量研究,但主要面向 Java 等命令式代码,未覆盖 Alloy 这类带传递闭包的一阶关系逻辑声明式模型。本文提出首个 Alloy 模型修复技术 ARepair:以含失败用例的测试集为规约,先利用变异测试定位与生成候选修复成分,再借助程序合成搜索满足测试的模型修改,输出对给定测试正确的修复后模型。作者在收集的 38 个真实缺陷 Alloy 模型上进行评估,共成功修复 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.