Generation of Ballot Test Data for Vote Counting

Dermot Cochran is working on this project.

Recently we have developed a theory about how to identify interesting test data for an arbitrary voting scheme. This project requires the application of this theory to a non-trivial voting scheme of your choice, by using an automated theorem proven to find examples of sets of ballots which test each interesting scenario. You would need to generate the complete set of test data by the method and use it to achieve full test coverage of an existing open source implementation of a vote counting scheme. You should then analyze the test results and explain any discrepancies or inconsistencies found in the implementation being tested. Ideally, you would release a test generation tool based on your work.

  • Supervisor Dermot Cochran
  • Subject Area software engineering
  • Pre-requisites strong knowledge of Java and strong programming skills
  • Co-requisites (things you must learn along the way) Voting systems and electoral law, the Java Modeling Language, the JML tool suite, the Alloy modeling language and the Alloy Analyser API
  • Subject Coverage software engineering with applied formal methods
  • Project Type formal system design and specification
  • Hardware/Software PC, laptop or workstation capable of running Java and Eclipse

Description

Recently we have developed a theory about how to identify interesting test data for an arbitrary voting scheme. This project requires the application of this theory to a non-trivial voting scheme of your choice, by using an automated theorem proven to find examples of sets of ballots which test each interesting scenario. You would need to generate the complete set of test data by the method and use it to achieve full test coverage of an existing open source implementation of a vote counting scheme. You should then analyze the test results and explain any discrepancies or inconsistencies found in the implementation being tested.

Mandatory Goals

  1. Use the generated ballots to create a complete test suite for an existing voting system.
  2. Analyze the test results and explain any discrepancies or inconsistencies found in the implementation being tested.

Discretionary Goals

  1. Coauthor, submit, and publish a paper on this work.

Exceptional Goals

  1. Release a test generation tool based on your work.

Sources of Information and Preparatory Reading

  1. The Verified Software Repository Project
  2. The KindSoftware Coding Standard
  3. The JML tool suite
  4. The Extended Static Checker for Java, ESC/Java2
  5. Design by Contract
  6. A Verification Centric Software Development Process for Java