Specifying and verifying requirements for election processes
Borislava I. Simidchieva, Matthew Marzilli, Lori A. Clarke, Leon J. Osterweil · 2008
In this paper we outline an approach for modeling election processes and then performing rigorous analysis to verify that these process models meet selected behavioral require-ments. We briefly outline some high-level requirements that an election process must satisfy and demonstrate how these are refined into a collection of lower-level properties that can be used as the basis for verification. We present a motivating example of an election process modeled using the Little-JIL process definition language, capture the lower-level proper-ties using the PROPEL property elicitation tool, and per-form formal analysis to verify that the process model adheres to these properties using the FLAVERS finite-state verifier. We illustrate how this approach can identify errors in the process model when a property is violated.