一句话：提出 COMBA：一种无需人工干预、基于组合覆盖准则的 Alloy 规约自动化测试生成技术。
形式规约的正确性评估十分困难。现有规约测试方法往往需要用户提供场景或缺乏系统覆盖准则。本文提出 COMBA，一种面向 Alloy 规约的组合测试技术。COMBA 仅依据规约元素自动划分状态空间，定义一族组合测试准则：给定正整数 t，要求测试用例覆盖来自不同划分的所有可行 t 元组；并利用增量 SAT 求解高效生成满足准则的测试用例。作者在大量含已知错误的 Alloy 规约上，将 COMBA 与现有测试生成方法比较。实验表明，取 t=2 时 COMBA 运行更快、生成的测试套件更小，且发现显著更多真实缺陷。
Specifications are an essential component of software development, and getting specifications right, especially formal specifications, can be very challenging. While the use of tools such as model finders and model checkers can be very effective for specification analysis through property checking, researchers have also realized that by the explicit provision of wanted and unwanted specification scenarios, in the style of testing in programs, specification assessment can be significantly enhanced. Thus, various testing and test generation techniques have been recently proposed for assessing formal specifications.In this paper, we present such a specification testing approach, in the form of a novel combinatorial testing technique for Alloy specifications, called COMBA. COMBA implements an automated partitioning of the state space of Alloy specifications solely based on elements of the specification (thus not requiring user intervention), and defines a family of test criteria, that indicate how such partitions are to be covered. The coverage of the partitions is defined by a family of combinatorial criteria that, given a positive integer t, require to cover through test cases all feasible t-uples of elements from different partitions. Finally, COMBA introduces an efficient algorithm to generate test cases that satisfy the combinatorial criteria. By leveraging on incremental SAT solving techniques, COMBA achieves significantly better performance in test generation.We experimentally assess COMBA against existing test generation approaches for Alloy, using a large number of specifications with known errors. The results show that COMBA(with t = 2) runs faster, produces smaller test suites, and finds a significantly larger number of real bugs than related approaches.
DOI 原文 ·
@inproceedings{paperbot9571,
title = {Automated Combinatorial Test Generation for Alloy},
author = {Agustín Borda and Germán Regis and Nazareno Aguirre and Marcelo Frias and Pablo Ponzio},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00240}
}