一句话：BeAFix 通过变异与有界穷举搜索自动修复 Alloy 模型，支持多故障与性质型 oracle。
本文介绍 BeAFix，一个自动修复错误 Alloy 模型的工具。Alloy 模型可能含多处故障。BeAFix 基于 Alloy Analyzer，通过变异算子生成修复候选，并用有界穷举方法遍历候选空间；由于候选空间增长迅速，工具采用可靠剪枝技术，从而支持修复含多个错误行或表达式的模型。该工具不要求以测试作为补丁接受准则，既可支持测试 oracle，也可利用 Alloy 中更常见的性质型 oracle，如谓词可满足性与断言有效性检查。BeAFix 提供视频演示、公开二进制和归档。
This paper describes BeAFix, a tool for automated repair of faulty Alloy models. The tool builds upon the Alloy Analyzer, the analysis tool for Alloy. It generates repair candidates by mutating a faulty Alloy model, and employs a bounded-exhaustive approach to traverse the space of repair candidates. Since BeAFix’s mutation operators make the space of repair candidates to quickly grow, the tool supports some sound pruning techniques, that allow it to fix Alloy models with more than one faulty line or expression. Additionally, BeAFix does not require tests as a patch acceptance criterion. Although BeAFix supports tests as oracles, our tool is also able to leverage property-based oracles, which are more commonly found in Alloy models in the form of predicate satisfiability and assertion validity checks.A video demonstration of BeAFix can be found at https://youtu.be/5RG40SmlFXQ. The tool’s binaries and further details about its usage, can all be found at https://sites.google.com/view/beafixevaluation/beafix. The tool is also available in a public archive at https://doi.org/10.5281/zenodo.5296466.
DOI 原文 ·
@inproceedings{paperbot6623,
title = {BeAFix: An Automated Repair Tool for Faulty Alloy Models},
author = {Simon Gutierrez Brida and German Regis and Guolong Zheng and Hamid Bagheri and ThanhVu Nguyen and Nazareno Aguirre and Marcelo Frias},
booktitle = {ASE},
year = {2021},
doi = {10.1109/ase51524.2021.9678524}
}