This package contains the SoS/KOA vote tally application.
||Global constants used in the user interface.
||This class can be used as base class for XMLReaders that generate SAX
events from Java objects.
||This class is used to store all the information needed to
generate the 'Verwerkingsverslag' report.
||XMLReader implementation for the AuditLog class.
||A candidate in an election.
||The CandidateList stores all of the information embodied in the
XML-based candidate list files provided by the KOA application.
||The metadata associated with a candidiate list for an election.
||XMLReader implementation for the CandidateList class.
||Class to clear memory and files.
||Class to count the votes.
||Class to decrypt the votes.
||A district is a region of the country within a kieskring.
||This class is an implementation of ContentHandler which acts as a proxy to
another ContentHandler and has the purpose to provide a few handy methods
that make life easier when generating SAX events.
||Class to close this application.
||A file filter.
||The help window.
||Some static helper methods for dealing with hexadecimal notation.
||Class to handle importing candidate file.
||Class to import both private and public key file.
||Class to handle importing the votes file.
||A kieskring in an election.
||A kieslijst in an election.
||This class is the top-most class of the system and tracks and
controls the overall tally process.
||Class to generate reports.
||Class to restart the application.
||Class which reacts to buttons in the menu.
||A static class used to execute a native PDF viewer on a specific
PDF file generated by the KOA application.
||The set of votes in an election.
Package sos.koa Description
This package contains the SoS/KOA vote tally application.
sos.koa package is the top-most package of the
SoS/KOA vote tally application.
The SoS/KOA vote tally application is a software program used to
tally the secure election results produced by the KoA
(Kiezen op Afstand) Hertellen Stemmen application, developed by LogicaCMG, on behalf of the Ministry of the Interior and Kingdom
Relations (Ministerie van Binnenlandse Zaken en
This system was written by the SoS Group at the Computing Science Institute of the University of Nijmegen.
The SoS Group is led by Prof. Bart Jacobs. The
development of the SoS/KOA application was led by Dr. Engelbert Hubbers. Dr. Martijn Oostdijk and
Dr. Joseph Kiniry were the
other two primary developers. Mr. Cees-Bart Breunesse and
Mr. Flavio Garcia
provided some technical support as well.
The SoS/KOA application has three main sub-components:
- Data Input/Output - This subcomponent of the
system is responsible for performing all file input and output.
The following classes are part of the data
- Data Structures - The core components of the
system responsible for representing all data and tallying all
results. The following classes are part of the data
- GUI - This subcomponent of the system is
responsible for performing all graphical user input and output.
The following classes are part of the GUI subsystem:
- Utility Classes - A small number of classes are
utility classes containing code shared by other subsystems.
The following classes are part of the utility
are modified versions of classes released
under the Apache Software License, Version 1.1, and were originally
created by James Tauber (
jtauber AT jtauber.com). For more
information on the Apache Software Foundation, please see http://www.apache.org/.
The following tools were used to develop the SoS/KOA vote tally
- The JML tool suite,
including the JML runtime assertion checking (RAC) compiler
JML unit test generation tool jmlunit, and the JML
documentation generation tool jmldoc.
The Java Modeling Language (JML) is a behavioral interface
specification language that can be used to specify the behavior
of Java modules. It combines the design by contract approach of
Eiffel and the model-based specification approach of the Larch
family of interface specification languages, with some elements
of the refinement calculus.
JML has been used to express the semantics of all core
classes of the SoS/KOA application. The core classes are those
classes in the data structures subcomponent, discussed
- The ESC/Java2
ESC/Java2 has been used to verify some methods of all data
structure subcomponents of the SoS/KOA system. Verify,
in this context, means that ESC/Java2 was used to automatically
prove that the provided implementation fulfills the associated
contract specified with JML.
- The jProfiler
Java code profiler
- The jSwat
graphical Java code debugger
- The CheckStyle
- The Eclipse development
- The Vim text editor
- GNU Emacs
- The Collection of Emacs
Development Environment Tools
- The Java Development
Environment for Emacs
- The Emacs Code Browser
- The Xrefactory package
The SoS/KOA application was developed using the following methodology:
- The system design was decomposed into three primary units: Data
Input & Output, Data Structures, and GUI.
- One developer took responsibility for each component:
Dr. Engelbert Hubbers (Data I/O), Dr. Joseph Kiniry (Data
Structures), and Dr. Martijn Oostdijk (GUI).
- It was decided that the classes of the system most critical for
application correctness were the data structure
components. Accordingly, these were the components that were to
be most heavily annotated with JML and where most of the
testing and verification effort were to be focused.
- Appropriate APIs were chosen for the various subsystems. The
primary choices where those of cryptography (a JCE
implementation), XML data I/O (JDK packages under
javax.xml), and presentation (Apache FOP and its
- It was decided that the APIs of this set most critical to
system correctness were the cryptography APIs. Thus, JML
annotations should be written for those APIs as early as
possible. Such annotations would help detect incorrect API use
early in the design process and would be used later for system
testing and verification. Joe took responsibility for writing
basic specifications for the crypto APIs.
- Design and development of the Data I/O subsystem and GUI
subsystem proceeded semi-independently.
- Since the application had a fairly well-specified, sequential
HCI specification, and because the final results are completely
dependent upon the data selected, loaded, decrypted, and
interpreted in a serious of input stages, it was decided that
a finite-state machine model would be used to specify the GUI
and Data I/O subcomponents of the system.
That state machine is embodied in the invariants of the
MenuPanel class and their dependencies. The final verification
effort depends upon these states to express that the final vote
tallies the right information.
- The specifications (types and JML annotations) for the classes
of the core data structures subcomponent were written as
completely as possible before any code for those classes was
written. The specifications were checked, initially and
continually during development, by running the ESC/Java2
typechecker and the JML typechecker tools.
- The implementation of the core data structures were written
according to the previously written specifications. These
implementations were checked, using the JML RAC compiler and the
ESC/Java2 verification tool, continually during development.
- Integration of the three components began when each was nearly
complete. During integration a number of small issues were
brought to light and the design and implementations of the
related classes were adjusted for integration.
- GUI full system testing began, using the pre-supplied input
files, as well as some larger fabricated input files.
Initially, system testing took place only on the Linux
- Unit tests were generated for all core data structure classes
of the system using the JML unit test generation tool
jmlunit. These test guarantee that every constructor
and every method of every core class is interactively tested
against its contract for every interesting data value of the
system as well for a large set of random input values.
In a standard test execution, a total of 255 tests were run
during each test execution cycle. The test execution cycle has
been run hundreds of times. This means that every core class
has been tested for (tens of) thousands of possible data values.
- The full system was profiled, both during GUI testing and during
unit testing, to determine if there were any memory or
performance issues that needed to be resolved. A few small
issues were identified and adjusted, but no real problems were
highlighted during this analysis.
- Documentation and specification coverage was analyzed for the
full system. It was decided that full coverage was necessary
only on the core data structure classes, thus they were reviewed
for 100% coverage.
- GUI system testing took place on the Mac OS X and Windows
platforms. The only issue to address on both platforms was how
to automatically spawn the appropriate PDF viewer to show the
final reports for the application.
- The User's Guide was written.
- The high-level system documentation (like this file) was
- The application was delivered to the Ministry.