Specifying and verifying requirements for election processes

ABSTRACT

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 briey 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.

REFERENCES

• 1: ACCURATE A Center for Correct, Usable, Reliable, Auditable, and Transparent Elections. http://accurate-voting.org/.
• 2: Brennan Center for Justice at NYU School of Law. http://www.brennancenter.org/.
• 3: Caltech/MIT Voting Technology Project. http://www.vote.caltech.edu/.
• 4: Election Assessment Hearing (June 29th, 2005). http://www.electionassessment.org/.
• 5: Verified Voting Foundation. http://www.verifiedvoting.org/.
• 6: Kepler: An Extensible System for Design and Execution of Scientific Workflows, Proceedings of the 16th International Conference on Scientific and Statistical Database Management, p.423, June 21-23, 2004 [doi>10.1109/SSDBM.2004.44]
• 7: J. L. Brunner. Project EVEREST: Evaluation & Validation of Election-Related Equipment, Standards & Testing Report of Findings. Technical report, Ohio Secretary of State Office, 2007.
• 8: L. Clarke, Y. Chen, G. Avrunin, B. Chen, R. Cobleigh, K. Frederick, E. Henneman, and L. Osterweil. Process programming to support medical safety: A case study on blood transfusion. In Proceedings of the Software Process Workshop, pages 347--359. Springer-Verlag, 2005.
• 9: James C. Corbett , George S. Avrunin, Using integer programming to verify general safety and liveness properties, Formal Methods in System Design, v.6 n.1, p.97-123, Jan. 1995 [doi>10.1007/BF01384316]
• 10: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 11: Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004 [doi>10.1145/1040291.1040292]
• 12: Dimitrios Georgakopoulos , Mark Hornick , Amit Sheth, An overview of workflow management: from process modeling to workflow automation infrastructure, Distributed and Parallel Databases, v.3 n.2, p.119-153, April 1995 [doi>10.1007/BF01277643]
• 13: E. Henneman, R. Cobleigh, K. Frederick, E. Katz-Basset, G. Avrunin, L. Clarke, J. Osterweil, C. Andrzejewski, K. Merrigan, and P. Henneman. Increasing patient safety and efficiency in transfusion therapy using formal process definitions. Technical report, University of Massachusetts, Amherst, 2006.
• 14: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 15: D. Jones. Evaluation of Voting Technologies, pages 3--16. Advances in Information Security. Kluwer Academic Publishers, 2003.
• 16: C. Lambrinoudakis, D. A. Gritzalis, V. Tsoumas, M. Karyda, and S. Ikonomopoulos. Secure Electronic Voting: The Current Landscape, pages 101--122. Advances in Information Security. Kluwer Academic Publishers, 2003.
• 17: Jeff Magee , Jeff Kramer, Concurrency: state models & Java programs, John Wiley & Sons, Inc., New York, NY, 2000
• 18: R. Mercuri and P. Neumann. Verification for Electronic Balloting Systems, pages 31--42. Advances in Information Security. Kluwer Academic Publishers, 2003.
• 19: L. Mitrou, D. A. Gritzalis, S. Katsikas, and G. Quirchmayr. Electronic Voting: Constitutional and legal requirements, and their technical implications, pages 43--60. Advances in Information Security. Kluwer Academic Publishers, 2003.
• 20: L. Osterweil, A. Wise, L. Clarke, A. Ellison, J. Hadley, E. Boose, and D. Foster. Process technology to facilitate the conduct of science. In Proceedings of the Software Process Workshop, pages 403--415. Springer-Verlag, 2005.
• 21: M. S. Raunak, B. Chen, A. Elssamadisy, L. A. Clarke, and L. J. Osterweil. Definition and analysis of election processes. In Proceedings of the Software Process Workshop, volume 3966 of LNCS, pages 178--185. Springer-Verlag, 2006.
• 22: R. Saltman. Public confidence and auditability in voting systems. In D. A. Gritzalis, editor, Secure Electronic Voting, Advances in Information Security. Kluwer Academic Publishers, 2003.
• 23: B. I. Simidchieva, L. A. Clarke, and L. J. Osterweil. Representing process variation with a process family. In Q. Wang, D. Pfahl, and D. M. Raffo, editors, Software Process Dynamics and Agility: Proceedings of the International Conference on Software Process, volume 4470 of LNCS, pages 109--120. Springer, 2007.
• 24: Rachel L. Smith , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581345]
• 25: O. Weigert. Business Process Modeling and Workflow Definition with UML. 1998.
• 26: A. Wise. Little-JIL 1.5 Language Report. Technical report, Department of Computer Science, University of Massachusetts, Amherst, MA, 2006.

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.1 ADMINISTRATIVE DATA PROCESSING
      Subjects: Government

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
      D.2.4 Software/Program Verification

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Design, Management, Theory, Verification

Keywords:
elections, process, properties, requirements, verification