I have worked on the application of formal methods to analysing the usability of human computer interfaces. There has been a certain amount of work on this topic, see for example, the PUMA project, the TACIT project and this page contains links to a number of relevant sources. I worked on this topic with a number of people including, Phil Barnard, Giorgio Faconti and Mieke Massink,
A central concern of HCI research is how to determine the usability of interfaces under development. The standard approach to such assessment is to construct a prototype implementation and then perform user trials and experimentation. The problem with such prototype construction is that it is both expensive and time consuming.
An alternative, and now relatively common, approach is to assess the usability of interfaces using cognitive models. There are a number of cognitive models that have been used in such assessment, e.g. SOAR, ACT-R, Programmable User Models and Interactive Cognitive Subsystems (ICS); each providing its own "information processing" inspired explanation of human cognition. Thus, such models are used to simulate the cognitive consequences of using a particular interface.
I worked on applying formal methods to such cognitive model based usability analysis. The motivation behind such an application of formal methods reflect two benefits of formal methods:-
1. Abstraction. We would argue that the abstraction devices offered by formal methods, e.g. non-determinism, can be advantageously applied in limiting the level of prescription enforced in realization of cognitive models. And this is indeed a very general problem in the cognitive setting. Specifically, many of the more general cognitive theories leave much unexplained, since complete mechanistic interpretations of cognitive behaviour are unavailable. Thus, in order to construct working simulations, large numbers of assumptions have to be made, leaving it unclear what aspect of the behaviour of the simulation corresponds to known cognitive behaviour and what arises from expediency. In the cognitive domain, this problem is called the irrelevant specification problem. We believe that limiting such overprescription has much in common with limiting overspecification which can be addressed using formal methods abstraction devices.
2. Rigorous Analysis. Perhaps the most powerful argument for adopting formal methods in computing is that they yield a description of the system which is amenable to rigorous analysis, e.g. demonstrating that your system does not enter certain degenerate states, such as deadlock states. This analysis can take one of two general forms - verification through proof or automated state space analysis. Under the former an, often hand crafted, series of formal steps are exhibited which show that a particular property can be derived from the formal specification of the system. In contrast, in the latter case a tool is used which automatically analyses the state space of a specification to determine whether a certain property holds.
Now how does the potential for rigorous analysis fit with cognitive modelling. Well, the standard cognitive science approach is to attempt to mimic cognitive behaviour by writing a computer program which when run simulates the particular cognitive task being considered. A rather obvious observation about such simulation is that it can never be exhaustive. In fact, in practice, such techniques will only be able to explore a small subset of the complete system behaviour (in this respect simulation is like testing, which as Djkstra so pertinently pointed out, can only demonstrate the presence of errors, but can never demonstrate the absence of errors). One reason for the inexhaustiveness of simulation is that the behaviour of any non-trivial system will be infinite in some respect, e.g. through using infinite data sets or exhibiting infinite concurrent behaviour. Although, it would be wrong to over emphasize the power of formal methods in resolving this problem, in particular formal methods have their own constraining boundaries (e.g. the state explosion problem), they do at least offer the potential of a more exhaustive investigation of the behaviour of cognitive models.
In response to these motivatory arguments I applied process algebra and interval temporal logic to the specification and analysis of Phil Barnard's cognitive architecture Interactive Cognitive Subsystems. A particular reason for choosing process algebra in this work is that they support both abstract description and simulated execution. In particular, the latter of these is typically not supported by approaches based on pure logic and yet it seems to be important in this application area.
My work on this topic is most comprehensively reported in the UKC internal report,
An interpretation of cognitive theory in concurrency theory Howard Bowman. Technical Report 8-98, Computing Laboratory, University of Kent at Canterbury, October 1998.
and the most complete publication is,
Analysing cognitive behaviour using LOTOS and Mexitl. H. Bowman and G. Faconti. Formal Aspects of Computing, 11:132-159, November 1999.
In addition, the following short report relates the work that I have done to the earlier syndetic modelling work of Barnard, Duce, Duke and May. They also provided a formal interpretation of ICS. However, they used Modal Action Logic as their specification notation.
Towards integrated cognitive and interface analysis. H. Bowman, G. Faconti, and M. Massink. In Howard Bowman, editor, Proceedings of Formal Methods Elsewhere 2000, Pisa, Italy, volume 43 of Electronic Notes in Theoretical Computer Science, Elsevier Science, October 2000.
I also reported my work on this topic to the cognitive science community, via the following short paper:
Modelling
concurrent cognitive architectures using process calculi. H. Bowman. In Sebastiano Bagnara, editor, European
Conference on Cognitive Science 1999, pages 161-166. Istituto di
Psicologia, CNR, October 1999.
I also developed a new LOTOS specification of ICS, which has been used to model the Attentional Blink phenomenon. Details of this approach can be found in the following publication.
"Rendering Information
Processing Models of Cognition and Affect Computationally Explicit: Distributed
Executive Control and the Deployment of Attention"
P.J. Barnard and H. Bowman
Cognitive Science Quarterly, publisher: Hermes Science Publications, vol. 3,
no. 3, pp 297-328, April 2004.
There are a number of other people who have worked on related issues:
Phil Barnard, David Duce, David Duke, Giorgio Faconti, Mieke Massink, Jon May and Richard Young.
Their ideas greatly influenced me in my work on this topic.
I also linked my work on distributed multimedia systems with the HCI field as reported in the paper,
Specification and verification of media constraints using UPPAAL. H. Bowman, G. Faconti, and M. Massink. In 5th Eurographics Workshop on the Design, Specification and Verification of Interactive Systems, DSV-IS 98, Eurographics Series. Springer-Verlag, August 1998.
Back to Howard Bowman's home page.
Last modified April 2012.