Reducing the likelihood of human error in the use of interactive systems is increasingly important: the use of such systems is becoming widespread in applications that demand high reliability due to safety, security, financial or similar considerations. Consequently, the use of formal methods in verifying the correctness of interactive systems has started recently to include the modelling of human behaviour in interacting with the interface.

This course introduces fundamental concepts in Human-Computer Interaction (HCI) which draw particularly on the contributions of psychology, cognitive science and sociology. Then it presents the integration of HCI into design practice by defining informal principles, models and taxomomies, and giving an overview on different formal approaches to the characterision of the mental model of the user and the usability of the interactive system.

After an introduction to formal methods, and in particular to the two formal verification frameworks of model-checking and theorem-proving, the course focusses on Finite State Machines as a modelling formalism and on model-checking as a verification methodology. It explores how to build a formal model of the user's cognitively plausible behaviour and how to use such a model to drive the design of the computer part of the system by using model-checking as a debugging tool. This approach is illustrated using a groupware system as a case study. Model-checking is used

• to capture the emergence of user errors in the overall system that results from the composition of the user model with the system model;
• to show how these errors may affect the security of the system; and
• to show how the system may be improved by introducing safeguardes which do not compromise the usability of the system.

A second part of the course show how observable failures caused by erroneus patterns of behaviour can be expressed using temporal logic formulae. These formulae can then be decomposed into other formulae that characterise basic user patterns of behaviour, which directly correspond to the user's mental processes which caused the failure. Model-checking is used at this point to verify the soundness and completeness of the decomposition. This approach is illustrated first using an air traffic control system as the case study.

Audience

The course is taught at postgraduate level, but it does not have stringent prerequisites. In fact, only basic fragments of the formal methods notations (Finite State Machines based notations - e.g., the CSP process algebra - and Temporal Logic) are used. The motivation, purpose and limitations of using formal methods are discussed, and all formal methods notations are clearly presented before use.

Practical Part

All example used throughout the course have been implemented and formally verified using the Concurrency Workbench of the New Century (CWB-NC). The participants are instructed on how to use the tool and, if the course is long enough and appropriate conputing resources are available, may actively participate in practical sessions.

Flexibility in Length and Focus

The lenth of the course may vary between 6 and 30 hours which can be distributed in a minimum of 2 days (6 hour length) and a maximum of 2 weeks (30 hour length). Daily lectures of 2-3 hours are ideal and we discourage compressed courses where the audience is requested to attend more than 5 hours each day.

The introductory part on fundamental concepts in HCI may be largely reduced or entirely skipped if the audience has already a strong background in HCI or can actually constitute the main part of the course if this is in the interest of the audience.

The focus of the course may be on

• theory or practice (practice-oriented courses require at least one week duration);
• modelling or verification.

The title of the course may change depending on the focus.