一句话：FLACK 通过比较反例与满足断言的实例之间的差异，自动定位 Alloy 模型中导致断言违反的可疑表达式并排序。
现有故障定位技术多面向命令式程序（如 C、Java），依赖测试比较正确与错误执行轨迹来识别可疑语句，不适用于 Alloy 这类声明式语言——其模型并不被执行，而是被转换为逻辑公式交由 SAT 求解器求解。本文提出 FLACK 工具，输入为违反断言的 Alloy 模型，输出为按可疑程度排序的表达式列表。其核心思想是分析反例之间的差异：即不满足断言的实例与满足断言的实例之间的区别，从而在输入模型中找出导致违反的可疑表达式。作者在 157 个包含各类 bug 的 Alloy 模型上进行了实验，结果表明 FLACK 在定位这些 bug 原因时兼具效率与准确性。工具、评测基准与结果均已公开。
Fault localization can help developers identify buggy statements or expressions in programs. Existing fault localization techniques are often designed for imperative programs (e.g., C and Java) and rely on tests to compare correct and incorrect execution traces to identify suspicious statements. In this demo paper, we present FLACK, a tool to automatically locate faults for models written in Alloy, a declarative language where the models are not executed but instead converted into a logical formula and solved using a SAT solver. FLACK takes as input an Alloy model that violates some assertions and returns a ranked list of suspicious expressions contributing to the violation. The key idea is to analyze the differences between counterexamples, i.e., instances of the model that do not satisfy the assertion and instances that do satisfy the assertion to find suspicious expressions in the input model. An experiment with 157 Alloy models with various bugs shows the efficiency and accuracy of FLACK in localizing the causes of these bugs. FLACK and its evaluation benchmark and results can be downloaded from https://github.com/guolong-zheng/flack. The video demonstration is available at https://youtu.be/FKa2ohqIUms.
DOI 原文 ·
@inproceedings{paperbot6505,
title = {FLACK: Localizing Faults in Alloy Models},
author = {Guolong Zheng and ThanhVu Nguyen and Simon Gutierrez Brida and German Regis and Marcelo Frias and Nazareno Aguirre and Hamid Bagheri},
booktitle = {ASE},
year = {2021},
doi = {10.1109/ase51524.2021.9678740}
}