On Voting Machine Design for Verification and Testability
Abstract
We present an approach for the design
and analysis of an electronic voting machine based on a novel
combination of formal verification and systematic testing.
The system was designed specifically to enable verification and testing.
In our architecture,
the voting machine is a finite-state transducer that
implements the bare essentials required for an election.
We formally specify how each component of the machine is intended to work
and formally verify that a Verilog
implementation of our design
meets this specification.
However, it is more challenging to verify that the composition
of these components will behave as a voter would expect, because
formalizing human expectations is difficult.
We show how systematic testing can be used to address this issue, and
in particular to verify that
the machine will behave correctly on election day.