Sciweavers

Share
DGO
2008

Specifying and verifying requirements for election processes

10 years 1 months ago
Specifying and verifying requirements for election processes
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 requirements. 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 properties using the PROPEL property elicitation tool, and perform 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. Keywords Process, elections, requirements, properties, verification
Borislava I. Simidchieva, Matthew Marzilli, Lori A
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2008
Where DGO
Authors Borislava I. Simidchieva, Matthew Marzilli, Lori A. Clarke, Leon J. Osterweil
Comments (0)
books