一句话：提出反例引导的故障定位技术 FLACK，为声明式 Alloy 模型定位并排序导致断言违反的可疑表达式。
现有故障定位技术主要面向命令式程序（如 C、Java），依赖分析程序的正确与错误执行来标记可疑语句。但声明式语言编写的模型并不被“执行”，而是被翻译成逻辑公式交由后端约束求解器求解，因此这些技术无法直接适用。本文提出 FLACK，一个面向 Alloy 模型的故障定位工具：输入是包含被违反断言（violated assertion）的 Alloy 模型，输出是可能导致断言违反的可疑表达式排名列表。其核心思想是对比反例（不满足断言的模型实例）与满足断言的实例之间的差异，从而识别输入模型中的可疑表达式。实验结果表明 FLACK 高效（可在 5 秒内处理数千行规模的真实 Alloy 模型）、准确（含缺陷表达式稳定地位于可疑列表前 1.9% 以内），且实用（常能将错误缩小到可疑表达式的精确位置）。
Fault localization is a practical research topic that helps developers identify code locations that might cause bugs in a program. Most existing fault localization techniques are designed for imperative programs (e.g., C and Java) and rely on analyzing correct and incorrect executions of the program to identify suspicious statements. In this work, we introduce a fault localization approach for models written in a declarative language, where the models are not "executed," but rather converted into a logical formula and solved using backend constraint solvers. We present FLACK, a tool that takes as input an Alloy model consisting of some violated assertion and returns a ranked list of suspicious expressions contributing to the assertion 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. The experimental results show that FLACK is efficient (can handle complex, real-world Alloy models with thousand lines of code within 5 seconds), accurate (can consistently rank buggy expressions in the top 1.9% of the suspicious list), and useful (can often narrow down the error to the exact location within the suspicious expressions).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2102-10152,
title = {FLACK: Counterexample-Guided Fault Localization for Alloy Models},
author = {Guolong Zheng and ThanhVu Nguyen and Simon Gutierrez Brida and German Regis and Marcelo F. Frias and Nazareno Aguirre and Hamid Bagheri},
booktitle = {ICSE},
year = {2021},
doi = {10.1109/icse43902.2021.00065}
}