Process Model-Based Continuous Improvement of Election Process Quality and Robustness

ABSTRACT

This work demonstrates how the application of software analysis techniques to rigorously-defined models of elections can identify defects and vulnerabilities, whose remediation leads to demonstrable improvements in the elections. The work applies Finite State Verification (Model Checking) to identify process defects and Fault Tree Analysis to show how incorrect performance (by either humans or machines) can create hazards. The work also demonstrates how both can be combined to provide automated support for the synthesis of hazards and attacks, and the verification of the robustness of processes to such attacks.

Award ID: 0905530