一句话：AlloyFL 是 Alloy 模型故障定位技术，以错误模型与故障暴露测试套件为输入，输出按可疑度排序的位置列表。
Alloy 是一种常用的声明式建模语言，其 Analyzer 借助全自动的 SAT 分析引擎支持用户编写并执行模型，从而提升系统可靠性。然而，为复杂属性编写正确的约束十分困难，用户往往难以确定模型中的故障位置。为此，本文提出 AlloyFL：它以含故障的 Alloy 模型和能够暴露故障的测试套件为输入，输出一份按可疑度从高到低排序的位置列表，帮助用户定位问题。作者将该技术以 Java 实现为 Alloy Analyzer 的扩展。实验结果表明，AlloyFL 能够检测真实世界故障的位置，并且在模型存在多处故障时依然有效。论文还提供了演示视频链接。
Declarative models help improve the reliability of software systems: models can be used to convey requirements, analyze system designs and verify implementation properties. Alloy is a commonly used modeling language. A key strength of Alloy is the Analyzer, Alloy's integrated development environment (IDE), which allows users to write and execute models by leveraging a fully automatic SAT based analysis engine. Unfortunately, writing correct constraints of complex properties is difficult. To help users identify fault locations, AlloyFL is a fault localization technique that takes as input a faulty Alloy model and a fault-revealing test suite. As output, AlloyFL returns a ranked list of locations from most to least suspicious. This paper describes our Java implementation of AlloyFL as an extension to the Analyzer. Our experimental results show AlloyFL is capable of detecting the location of real world faults and works in the presence of multiple faulty locations. The demo video for AlloyFL can be found at https://youtu.be/ZwgP58Nsbx8.