Queen Mary, University of London logo HUM project logo UCL logo

HUM project

Work packages

Studies of human error

Human Error Modelling (HUM) Project

Formal user models

Formal cognitive architecture

Our cognitive architecture is a higher-order formalisation of abstract principles of cognition (Curzon et al, forthcoming ; Ruksenas et al, 2007). The principles focus on goals and domain knowledge of a user. Examples of such principles are a user entering an interaction with knowledge of the task and its subsidiary goals, reactive behaviour, non-determinism of action, no-option and goal based termination, and the distinction between the mental commitment and a physical action itself. A recent development of the architecture separated the user and the device state spaces, structuring the underlying user state space at the same time (Ruksenas et al, 2007). This structure distinguishes input signals (originating from user perception), output signals (consequences of user actions) and internal state (user memory). This restructuring also introduced intermediate entities that we refer to as interpretation and effect, relating the now distinct user and device state spaces. Intuitively, the effect is an abstract view of how user actions are translated into device commands (e.g. interactive systems with voice or gesture recognition of user inputs). Similarly, the interpretation is an abstract view of the pathways from device signals and environment objects to the user decision of what they could mean. This restructuring allows us to detect problems arising from the user (mis)interpretation of device prompts. It is also a step towards modelling aspects of distributed cognition. A recent development of the cognitive architecture involves support for timing analysis in terms of GOMS-like predictions of execution times (Ruksenas et al, forthcoming a).

Verification tools

Our original formalisation (Curzon et al, forthcoming) of the cognitive architecture was developed within the HOL theorem prover. A more recent version (Ruksenas et al, 2007) is based on the SAL model checking environment. Since SAL provides support for higher-order specifications, the cognitive architecture remains generic, and can be instantiated to verify any specific interactive system. It retains much of the core features that made the HOL version attractive but also allows for model checking of instantiated systems. Besides the restructuring of the architecture, the SAL version simplifies the treatment of the underlying state space by using simple variables instead of the history functions of the original. Since SAL is being developed as a framework for combining various verification tools, we envisage the SAL version of the architecture to be used for the future development of a verification methodology integrating both theorem proving and model checking based frameworks.

Case studies

To facilitate the development of a user-centered verification methodology, we performed a series of case studies (Curzon et al, forthcoming) using the HOL theorem prover. In each we considered a simple, albeit financially critical, interactive system. The intention was to illustrate how multiple classes of systematic user errors can be detected or verified absent from the designs of interactive systems. We also investigated proper soft-key interfaces in which the functionality associated with device inputs can change over time and the related class of errors induced by indirect interface changes. Finally, we demonstrated how a scenario based verification approach could be followed. Specifically we looked at how various user classes, for example beginners and experts, can be represented by choosing different instantiations of the generic user model. Using the SAL model checker, we analysed how the shape (form, size, etc.) of prompts affects user (mis)understanding of the corresponding device requests (Ruksenas et al, 2007). SAL was also used to explore security aspects of cognitive interpretation by analysing how user habits can potentially provoke confidentiality leaks (Ruksenas et al, forthcoming b ). Furthermore, we analysed the interdependence of usability (correctness) and performance properties by combining human error verification with timing analysis (Ruksenas et al, forthcoming a). We also considered an example of the integration of hardware and interaction verification to formally prove the usability of a simple interactive system (Xiong et al, 2006).

Meta-level verification

The verification of specific systems is only a part of a larger verification framework where the formal user specification could be combined with, say, design rules to reason about general properties of interactive systems. Design rules are guidelines that take into account human frailty. We demonstrated that design rules can be justified by deriving them from a formal cognitive architecture (Curzon and Blandford, 2005). The scope of application of the rules was informally explored. We also showed how the correctness of design rules can be formally proved with respect to our cognitive architecture. Finally, we investigated the verification of the integration of theorem proving and state exploration (model checking) environments within the context of usability verification (Xiong et al, 2006).


Curzon, P., Ruksenas, R., Blandford, A. (forthcoming) "An Approach to Formal Verification of Human-Computer Interaction". In press: BCS Formal Aspects of Computing.

Ruksenas, R., Curzon, P., Blandford, A., Back, J. (forthcoming a) "Combining Human Error Verification and Timing Analysis". In press: Proceedings of Engineering Interactive Systems (EIS 2007), Lecture Notes in Computer Science, Springer.

Ruksenas, R., Curzon, P., Blandford, A. (forthcoming b) "Detecting Cognitive Causes of Confidentiality Leaks". In press: Proceedings of Formal Methods for Interactive Systems 2006 (Workshop held in conjunction with ICFEM2006), Electronic Notes in Theoretical Computer Science.

Ruksenas, R., Curzon, P., Back, J., Blandford, A. (2007) "Formal Modelling of Cognitive Interpretation". In: Proceedings of Design, Specification and Verification of Interactive Systems (DSVIS 2006), vol.
4323 of Lecture Notes in Computer Science, pp 123-136, Springer.

Xiong, H., Curzon, P., Tahar, S. and Blandford, A. (2006). "Providing a Formal Linkage between MDG and HOL". In press, Formal Methods in Systems Design.

Working Papers

Curzon, P. and Blandford, A. (2005). "Justifying Usability Design Rules Based on a Formal Cognitive Model". QMUL Research Report RR-05-07.

This page last modified 11 September, 2007 by George Papatzanis


IMC logo
Logo of EPSRC
go to UCLIC home page