Synthesizing Test Cases for Narrowing Specification Candidates

TL;DR

This paper introduces a solver-based technique for generating test cases to help select the most accurate formal specification from multiple candidates, improving the specification refinement process.

Contribution

It presents two algorithms for generating test suites to distinguish among Alloy specifications, including one that produces minimal test suites and another that scales better.

Findings

Optimal algorithm is efficient for many practical problems.

Non-optimal algorithm scales to dozens of specifications.

Generated test suites effectively narrow down candidate specifications.

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.