Implementing the Irish Voting System
Note: This project was the 2006-2007 Final Year Project of UCD student Patrick Tierney.
- 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 EBON specification language, the JML tool suite, ESC/Java2
- Subject Coverage software engineering with applied formal methods
- Project Type system implementation using Design by Contract
- Hardware/Software any machine and operating system that runs Java 1.4
Description
Using a verification-centric software process and Design by Contract, implement the Irish voting system law (knows as "votail" in Irish) according to a pre-existing architecture design and formal specification.
Mandatory Goals
- Become familiar with the Irish voting system law.
- Implement, using JML-annotated Java, the Irish voting system according to the pre-existing architecture design and formal specification.
Discretionary Goals
- Write an EBON specification of the system.
- Generate and execute unit tests using JML-jUnit.
- Check the Mondex system implementation rigorously with ESC/Java2.
- Contribute this implementation to the Verified Software Repository.
Exceptional Goals
- Write unit tests corresponding to EBON scenarios using jUnit.
- Coauthor, submit, and publish a paper on this work.
- Check the system implementation rigorously with ESC/Java2.
- Specify and prove some (behavioral and security) properties about the specification.
Sources of Information and Preparatory Reading
- Specifying the Irish Voting System
- The Commission for Electronic Voting website
- The Verified Software Repository Project
- The BON specification language website
- The Extended BON project
- The KindSoftware Coding Standard
- The JML tool suite
- The Extended Static Checker for Java, ESC/Java2
- Design by Contract