Modeling Test Cases for Voting

Dermot Cochran, Joseph Roland Kiniry

    Research output: Book / Anthology / Report / Ph.D. thesisReportResearch

    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.
    Original languageEnglish
    Place of PublicationCopenhagen
    PublisherIT-Universitetet i København
    EditionTR-2011-143
    Number of pages28
    ISBN (Electronic)978-87-7949-239-4
    Publication statusPublished - Sept 2011
    SeriesIT University Technical Report Series
    NumberTR-2011-143
    ISSN1600-6100

    Fingerprint

    Dive into the research topics of 'Modeling Test Cases for Voting'. Together they form a unique fingerprint.

    Cite this