Curzon, P.; Blandford, A.E.; (2000) 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.

Preview

PDF 16625.pdf Download (718kB)

Abstract

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 [7] 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.

Download activity - last month

Export as XMLJSONCSV

Download activity - last 12 months

Export as JSONCSVXML

Downloads by country - last 12 months

Export as XMLJSONCSV

Archive Staff Only

View Item