Abstract
Systematic user errors commonly occur in the use of interactive systems. We describe a formal reusable user model implemented in higherorder logic that can be used for machine-assisted reasoning about user errors. The core of this model is a series of non-deterministic guarded temporal rules. We consider how this approach allows errors of various specific kinds to be detected and so avoided by proving a single theorem about an interactive system. We illustrate the approach using a simple case study.
Chapter PDF
References
R. Butterworth, A. Blandford and D. Duke. Using formal models to explore display based usability issues. Journal of Visual Languages and Computing, 10:455–479, 1999.
M. Byrne and S. Bovair. A working memory model of a common procedural error. Cognitive Science, 21(1): 31–61, 1997.
F. Corella, Z. Zhou, X. Song, M. Langevin and E. Cerny. Multiway Decision Graphs for automated hardware verification. Formal Methods in System Design, 10(1): 7–46, 1997.
P. Curzon and A. Blandford. Using a verification system to reason about post-completion errors. Presented at Design, Specification and Verification of Interactive Systems 2000. Available from http://www.cs.mdx.ac.uk/puma/.
P. Curzon and A. Blandford. Reasoning about order errors in interaction. Supplementary Proceedings of the International Conference on Theorem Proving in Higher-order Logics, August 2000. Available from http://www.cs.mdx.ac.uk/puma/.
P. Curzon and I. Leslie. Improving hardware designs whilst simplifying their proof. Designing Correct Circuits, Workshops in Computing, Springer-Verlag 1996.
D.J. Duke, P.J. Barnard, D.A. Duce, and J. May. Syndetic modelling. Human-Computer Interaction, 13(4): 337–394, 1998.
M.J.C. Gordon and T.F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press 1993.
W-O Lee. The effects of skills development and feedback on action slips. In Monk, Diaper, and Harrison, editors, People and Computers VII. CUP, 1992.
T.G. Moher and V. Dirda. Revising mental models to accommodate expectation failures in human-computer dialogues. In Design, Specification and Verification of Interactive Systems’95, pp 76–92. Wien: Springer, 1995.
F. Paterno' and M. Mezzanotte. Formal analysis of user and system interactions in the CERD case study. In Proceedings. of EHCI’95: IFIP Working Conference on Engineering for Human-Computer Interaction, pp 213–226. Chapman and Hall, 1995.
J. Reason. Human Error. Cambridge University Press, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Curzon, P., Blandford, A. (2001). Detecting Multiple Classes of User Errors. In: Little, M.R., Nigay, L. (eds) Engineering for Human-Computer Interaction. EHCI 2001. Lecture Notes in Computer Science, vol 2254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45348-2_9
Download citation
DOI: https://doi.org/10.1007/3-540-45348-2_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43044-5
Online ISBN: 978-3-540-45348-2
eBook Packages: Springer Book Archive