一句话：提出 ASketch，用带洞的部分 Alloy 模型、候选片段生成器与 AUnit 测试自动补全模型，辅助用户写出正确的 Alloy 模型。
Alloy 是一种基于带传递闭包的一阶逻辑的声明式建模语言，广泛用于软件系统建模与设计缺陷查找，但写出正确的 Alloy 模型或调试有缺陷的模型往往十分困难。为此，作者提出 ASketch——一种用于 Alloy 的 sketching/综合技术。用户提供带洞（hole）的部分 Alloy 模型、为每个洞指定候选片段的生成器，以及一组刻画模型期望性质的测试；ASketch 通过搜索补全这些洞，使得补全后的模型通过全部测试。测试基于新近提出的 AUnit 框架编写，该框架为 Alloy 模型提供单元测试、测试执行与模型覆盖等传统单元测试意义上的基础设施。论文介绍了 ASketch 的 Java 实现，它是一个命令行工具，已作为开源项目发布于 GitHub。实验结果表明，ASketch 能够处理包含多个洞且搜索空间较大的部分 Alloy 模型。
Alloy is a declarative modeling language that supports first-order logic with transitive closure. Alloy has been used in a variety of domains to model software systems and find design deficiencies. However, it is often challenging to make an Alloy model correct or to debug a faulty Alloy model. ASketch is a sketching/synthesis technique that can help users write correct Alloy models. ASketch allows users to provide a partial Alloy model with holes, a generator that specifies candidate fragments to be considered for each hole, and a set of tests that capture the desired model properties. Then, the tool completes the holes such that all tests for the completed model pass. ASketch uses tests written for the recently introduced AUnit framework, which provides a foundation of testing (unit tests, test execution, and model coverage) for Alloy models in the spirit of traditional unit testing. This paper describes our Java implementation of ASketch, which is a command-line tool, released as an open-source project on GitHub. Our experimental results show that ASketch can handle partial Alloy models with multiple holes and a large search space. The demo video for ASketch can be found at https://youtu.be/T5NIVsV329E.
DOI 原文 ·
@inproceedings{paperbot4678,
title = {ASketch: a sketching framework for Alloy},
author = {Kaiyuan Wang and Allison Sullivan and Darko Marinov and Sarfraz Khurshid},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3264594}
}