Abstract
Human interaction is central to many computing systems that require a high level of assurance. We term such systems as high-confidence interactive systems. Examples of such systems include aircraft control systems (interacting with a pilot), automobiles with self-driving features (interacting with a driver), medical devices (interacting with a doctor), and electronic voting machines (interacting with a voter). A major challenge to verifying the correct operation of such systems is that it is difficult to formally specify the human user’s view of correct operation and perception of the input/output interface. In this paper, we describe a promising approach towards addressing this challenge that combines formal verification with systematic testing by humans. We describe an illustrative application of this approach to electronic voting in the U.S., and outline directions for future work.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alexander, K., Smith, P.: Verifying the vote in 2008 presidential election battleground states (November 2008), http://www.calvoter.org/issues/votingtech/pub/pres2008_ev.html
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 4, ch. 8. IOS Press (2009)
Federal Aviation Administration (FAA). The interfaces between flight crews and modern flight systems (1995), http://www.faa.gov/avr/afs/interfac.pdf
Jha, S., Limaye, R., Seshia, S.A.: Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 668–674. Springer, Heidelberg (2009)
Kohn, L.T., Corrigan, J.M., Donaldson, M.S. (eds.): To err is human: Building a safer health system. Technical report, A report of the Committee on Quality of Health Care in America, Institute of Medicine. National Academy Press, Washington, DC (2000)
Obradovich, J.H., Woods, D.D.: Users as designers: How people cope with poor HCI design in computer-based medical devices. Human Factors 38(4), 574–592 (1996)
Sturton, C., Jha, S., Seshia, S.A., Wagner, D.: On voting machine design for verification and testability. In: Proceedings of the ACM Conference on Computer and Communications Security (CCS) (November 2009)
Terauchi, T., Aiken, A.: Secure information flow as a safety problem. Technical Report UCB/CSD-05-1396, EECS Department, University of California, Berkeley (June 2005)
Verified Voting Foundation. America’s voting systems in 2010, http://verifiedvoting.org
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Seshia, S.A. (2013). Verifying High-Confidence Interactive Systems: Electronic Voting and Beyond. In: Frey, D., Raynal, M., Sarkar, S., Shyamasundar, R.K., Sinha, P. (eds) Distributed Computing and Networking. ICDCN 2013. Lecture Notes in Computer Science, vol 7730. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35668-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-35668-1_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35667-4
Online ISBN: 978-3-642-35668-1
eBook Packages: Computer ScienceComputer Science (R0)