ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications
ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications
复制标题
DOI：
10.1145/3551349.3556944
复制
发表时间：
2022-10
期刊：
影响因子：
--
通讯作者：
Simón Gutiérrez Brida;Germán Regis;Guolong Zheng;H. Bagheri;Thanhvu Nguyen;Nazareno Aguirre;M. Frias
中科院分区：
文献类型：
--
作者：
Simón Gutiérrez Brida;Germán Regis;Guolong Zheng;H. Bagheri;Thanhvu Nguyen;Nazareno Aguirre;M. Frias
自动程序修复(APR)技术在自动查找C或Java等编程语言中的程序修复方面取得了巨大成功。在这项工作中，我们专注于修复形式规范，特别是合金规范语言的形式规范。与大多数APR工具不同，我们的修复合金规格的方法名为Icebar，它不使用基于测试的先知进行补丁评估。相反，Icebar依赖于使用基于属性的预言器，这些预言器通常作为断言和断言出现在合金规范中。这些基于属性的Oracle为补丁评估定义了更强的条件，从而减少了因使用基于测试的Oracle而引起的臭名昭著的过度匹配问题，这通常在APR上下文中观察到。此外，由于断言和谓词是合金固有的，而测试用例不是，因此我们的工具可能比基于测试的合金修复工具对合金用户更有吸引力。从高层次上讲，Icebar是一个迭代的、基于反例的过程，它生成并验证修复候选对象。Icebar收到了一份带有失败的基于属性的先知的有缺陷的合金规范，并使用合金的反例来构建测试并提供基于测试的合金修复工具ARPair，以产生修复候选对象。然后，根据属性预言检查候选对象是否过适合：如果候选对象通过，则已找到修复方法；如果不通过，则生成进一步的反例以构建测试并增强测试套件，并迭代该过程。Icebar包括不同的机制，具有不同的可靠性，可以从失败的谓词和断言中生成反例。我们的评估表明，Icebar在减少过装量和提高维修率方面都明显优于ARPair。此外，Icebar表明，迭代改进使我们能够显著改进最先进的合金规格自动修复工具，而无需对该工具进行任何修改。
Automated program repair (APR) techniques have shown great success in automatically finding fixes for programs in programming languages such as C or Java. In this work, we focus on repairing formal specifications, in particular for the Alloy specification language. As opposed to most APR tools, our approach to repair Alloy specifications, named ICEBAR, does not use test-based oracles for patch assessment. Instead, ICEBAR relies on the use of property-based oracles, commonly found in Alloy specifications as predicates and assertions. These property-based oracles define stronger conditions for patch assessment, thus reducing the notorious overfitting issue caused by using test-based oracles, typically observed in APR contexts. Moreover, as assertions and predicates are inherent to Alloy, whereas test cases are not, our tool is potentially more appealing to Alloy users than test-based Alloy repair tools. At a high level, ICEBAR is an iterative, counterexample-based process, that generates and validates repair candidates. ICEBAR receives a faulty Alloy specification with a failing property-based oracle, and uses Alloy’s counterexamples to build tests and feed ARepair, a test-based Alloy repair tool, in order to produce a repair candidate. The candidate is then checked against the property oracle for overfitting: if the candidate passes, a repair has been found; if not, further counterexamples are generated to construct tests and enhance the test suite, and the process is iterated. ICEBAR includes different mechanisms, with different degrees of reliability, to generate counterexamples from failing predicates and assertions. Our evaluation shows that ICEBAR significantly improves over ARepair, in both reducing overfitting and improving the repair rate. Moreover, ICEBAR shows that iterative refinement allows us to significantly improve a state-of-the-art tool for automated repair of Alloy specifications without any modifications to the tool.