Synthesizing Test Cases for Narrowing Specification Candidates
Alcino Cunha, Nuno Macedo
TL;DR
The paper addresses selecting a best Alloy specification among multiple candidates by generating a narrowing test suite whose classifications by a domain expert identify a single winner. It proposes two solver-based synthesis strategies: a non-optimal SAT-based algorithm scalable to many candidates and an optimal PM-SAT-based method that guarantees a minimal test set. A prototype implements both approaches for Alloy and evaluates on 28 requirements from Alloy4Fun, showing that the non-optimal method scales better with the number of candidates ($N$) while the optimal method produces smaller $|T|$ but faces scalability limits as $N$ grows. The work situates the problem within the minimum test set literature and outlines future extensions to temporal logic and other formalisms.
Abstract
This paper proposes a technique to help choose the best formal specification candidate among a set of alternatives. Given a set of specifications, our technique generates a suite of test cases that, once classified by the user as desirable or not, narrows down the set of candidates to at most one specification. Two alternative solver-based algorithms are proposed, one that generates a minimal test suite, and another that does not ensure minimality. Both algorithms were implemented in a prototype that can be used generate test suites to help choose among alternative Alloy specifications. Our evaluation of this prototype against a large set of problems showed that the optimal algorithm is efficient enough for many practical problems, and that the non-optimal algorithm can scale up to dozens of candidate specifications while still generating reasonably sized test suites.