Modeling Test Cases for Voting
TR-2011-143, Authors: Dermot Cochran and Joseph R. Kiniry
Modeling Test Cases for Voting
Dermot Cochran
Joseph R. Kiniry
September 2011
Abstract
The ballot counting process for Proportional Representation by Single Transferable Vote (PR-STV) elections can be modeled formally using the Alloy model checker so as to cover all possible branches through the ballot counting algorithm. We use the Alloy model finder to describe the elections in terms of scenarios, consisting of equivalence classes of possible outcomes for each candidate in the election, where each outcome represents one branch through the algorithm. We show how test data is generated from a first order logic representation of the counting algorithm using the Alloy model finder. This process guarantees that we find the minimal number of ballots needed to test each scenario.
Technical report TR-2011-143 in IT University Technical Report Series, September 2011.
Available as PDF.