Reasoning about order errors in interaction.
In: Aagaard, M. and Harrison, J. and Schubert, T., (eds.)
Supplemental proceedings of the 13th international conference on theorem proving in higher order logics (TPHOLs 2000).
(pp. pp. 33-48).
Oregon Graduate Institute: Portland, US.
Reliability of an interactive system depends on users as well as the device implementation. User errors can result in catastrophic system failure. However, work from the field of cognitive science shows that systems can be designed so as to completely eliminate whole classes of user errors. This means that user errors should also fall within the remit of verification methods. In this paper we demonstrate how the HOL theorem prover  can be used to detect and prove the absence of the family of errors known as order errors. This is done by taking account of the goals and knowledge of users. We provide an explicit generic user model which embodies theory from the cognitive sciences about the way people are known to act. The user model describes action based on user communication goals. These are goals that a user adopts based on their knowledge of the task they must perform to achieve their goals. We use a simple example of a vending machine to demonstrate the approach. We prove that a user does achieve their goal for a particular design of machine. In doing so we demonstrate that communication goal based errors cannot occur.
|Title:||Reasoning about order errors in interaction|
|Open access status:||An open access version is available from UCL Discovery|
|Additional information:||Paper given at the 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2000) held at Portland, Oregon, USA, August 14-18 2000, and published as part of the supplemental proceedings. The main proceedings volume is published by Springer in 'Lecture Notes in Computer Science', Vol. 1869 http://www.springer.com/computer/foundations/book/978-3-540-67863-2|
|UCL classification:||UCL > School of Life and Medical Sciences > Faculty of Brain Sciences > Psychology and Language Sciences (Division of) > UCL Interaction Centre|
Archive Staff Only