Specifying the Irish Voting System

Note: This project was accomplished by Dermot Cochran in 2005-2006 to earn his MSc in Advanced Software Engineering in the School of Computer Science and Informatics at UCD. This work is now a part of the KOA Remote Voting System. Dermot continues to work on this project. Please contact him for more details.

The report/thesis written for this project is available here: "Secure Internet Voting in Ireland Using the Open Source Kiezen op Afstand (KOA) Remote Voting System" by Dermot Cochran.

  • Supervisor Dr. Joseph Kiniry
  • Subject Area software engineering
  • Pre-requisites strong knowledge of Java and strong programming skills
  • Co-requisites (things you must learn along the way) Irish voting system and law, the Java Modeling Language, the JML tool suite, ESC/Java2
  • 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

Using a verification-centric software process, perform an analysis of the Irish voting system law (knows as "votail" in Irish) and design and formally specify an architecture to realize this voting system.

Mandatory Goals

  1. Become familiar with the Irish voting system law.
  2. Perform a requirements analysis of the Irish voting system by careful analysis of the legal text.
  3. Design and formally specify, using JML-annotated Java, the Irish voting system according to the aforementioned requirements analysis.

Discretionary Goals

  1. Check the soundness of the formal specification using ESC/Java.
  2. Contribute this formal specification to the Verified Software Repository.

Exceptional Goals

  1. Coauthor, submit, and publish a paper on this work.
  2. Specify and prove some (behavioral and security) properties about the specification.

Sources of Information and Preparatory Reading

  1. The Commission for Electronic Voting website
  2. The Verified Software Repository Project
  3. The KindSoftware Coding Standard
  4. The JML tool suite
  5. The Extended Static Checker for Java, ESC/Java2
  6. Design by Contract