Specifying the Danish Voting System
Olavur Kjolbro is now working on this project for MSc thesis at IT University of Copenhagen
Write a formal specification of the Danish Voting System using formal BON and JML. Show the refinement from Danish electoral law through BON and to JML. Outline the Java architecture which would be needed to implement the system. Generate unit tests from the JML specification and write unit tests for the BON scenarios. Compare and contrast with existing specifications of the Irish and Dutch voting systems. A full implementation of the specification is *not* expected. Use of the Mobius PVE is required. Ideally, you would help to identify a standard methodology for formal specification of voting systems.
- 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) Danish 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 Danish voting system law and design and formally specify an architecture to realize this voting system. Note that a full implementation of the specification is not required.
Mandatory Goals
- Become familiar with the Danish voting system law.
- Perform a requirements analysis of the Danish voting system by careful analysis of the legal text.
- Design and formally specify, using BON with refinement JML-annotated Java, the Danish voting system according to the aforementioned requirements analysis.
Discretionary Goals
- Check the soundness of the formal specification using ESC/Java.
- Compare and contrast with existing specifications of the Irish and Dutch voting systems.
- Coauthor, submit, and publish a paper on this work.
Exceptional Goals
- Specify and prove some (behavioral and security) properties about the specification.
- Propose a standard methodology for formal specification of voting systems.