Overview | Package | Class | Tree | Deprecated | Index | Help
| SOA © 2004 SoS Group All Rights Reserved
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES

## Package sos.koa

This package contains the SoS/KOA vote tally application.

See:
Description

Interface Summary
KOAConstants | Global constants used in the user interface.

Class Summary
AbstractObjectReader | This class can be used as base class for XMLReaders that generate SAX events from Java objects.
AuditLog | This class is used to store all the information needed to generate the 'Verwerkingsverslag' report.
AuditLogXMLReader | XMLReader implementation for the AuditLog class.
Candidate | A candidate in an election.
CandidateList | The CandidateList stores all of the information embodied in the XML-based candidate list files provided by the KOA application.
CandidateListMetadata | The metadata associated with a candidiate list for an election.
CandidateListXMLReader | XMLReader implementation for the CandidateList class.
ClearAdapter | Class to clear memory and files.
CountAdapter | Class to count the votes.
DecryptAdapter | Class to decrypt the votes.
District | A district is a region of the country within a kieskring.
EasyGenerationContentHandlerProxy | 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.
ExitAdapter | Class to close this application.
FileNameFilter | A file filter.
HelpAdapter | The help window.
Hex | Some static helper methods for dealing with hexadecimal notation.
ImportCandidatesAdapter | Class to handle importing candidate file.
ImportKeyAdapter | Class to import both private and public key file.
ImportVotesAdapter | Class to handle importing the votes file.
KiesKring | A kieskring in an election.
KiesLijst | A kieslijst in an election.
MenuPanel | This class is the top-most class of the system and tracks and controls the overall tally process.
ReportAdapter | Class to generate reports.
RestartAdapter | Class to restart the application.
Task | Class which reacts to buttons in the menu.
ViewPdf | A static class used to execute a native PDF viewer on a specific PDF file generated by the KOA application.
VoteSet | The set of votes in an election.

Exception Summary
KOAException | General KOA exception.

## Package sos.koa Description

This package contains the SoS/KOA vote tally application.

## Package Specification

The `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 Koninkrijksrelaties).

## Package Authors

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.

## System Structure

The SoS/KOA application has three main sub-components:

1. 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 input/output subsystem:
   - `AbstractObjectReader`
   - `AuditLog`
   - `AuditLogXMLReader`
   - `CandidateListXMLReader`
   - `EasyGenerationContentHandlerProxy`
2. 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 structures subsystem:
   - `Candidate`
   - `CandidateList`
   - `CandidateListMetadata`
   - `District`
   - `KiesKring`
   - `KiesLijst`
   - `VoteSet`
3. 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:
   - `ClearAdapter`
   - `CountAdapter`
   - `DecryptAdapter`
   - `ExitAdapter`
   - `FileNameFilter`
   - `HelpAdapter`
   - `ImportCandidatesAdapter`
   - `ImportKeyAdapter`
   - `ImportVotesAdapter`
   - `MenuPanel`
   - `ReportAdapter`
   - `RestartAdapter`
   - `Task`
   - `ViewPdf`
4. Utility Classes - A small number of classes are utility classes containing code shared by other subsystems. The following classes are part of the utility subsystem:
   - `Hex`
   - `KOAConstants`
   - `KOAException`

The classes `AbstractObjectReader`, `AuditLogXMLReader`, `CandidateListXMLReader` and `EasyGenerationContentHandlerProxy` 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/.

## Libraries User

- The Apache Avalon Framework
- The Apache XML Project's Batik SVG toolkit
- The Bouncy Castle Crypto APIs
- The jUnit Java unit test framework
- The FOP (Formatting Objects Processor) package
- The SAX and DOM XML parsers that are part of the JDK 1.4 API

## Tools Used

The following tools were used to develop the SoS/KOA vote tally application.

- The JML tool suite, including the JML runtime assertion checking (RAC) compiler jmlrac, the 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 above.
- The ESC/Java2 verification tool
  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 tool
- The Eclipse development environment
- 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 for Emacs

## Development Methodology

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 dependencies).
- 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 platform.
- 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 written.
- The application was delivered to the Ministry.

Overview | Package | Class | Tree | Deprecated | Index | Help
| SOA © 2004 SoS Group All Rights Reserved
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES