Abstract
Safe operation of safety critical systems depends on appropriate interactions between the human operator and the computer system. Specification of such safety-critical systems is fundamental to enable exhaustive and automated analysis of operator system interaction. In this paper we present a structured, comprehensive and computer-aided approach to formally specify and verify user interfaces based on model checking techniques. Copyright

Abstract
This paper explores the role of formal methods as part of the user-centred design of interactive systems. An iterative process is described, developing prototypes incrementally, proving user-centred requirements while at the same time evaluating the prototypes that are executable forms of the developed models using 'traditional' techniques for user evaluation. A formal analysis complements user evaluations. This approach enriches user-centred design that typically focuses understanding on context and producing sketch designs. These sketches are often non-functional (e.g. paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The use of formal methods provides a systematic approach to checking plausibility and consistency during early design stages, while at the same time enabling the generation of executable prototypes. The technique is illustrated through an example based on a pill dispenser.

Abstract

Abstract
There is considerable interest within the Human Computer Interaction (HCI) community in the use of media spaces to enhance awareness and interaction between workers in offices or other spatially distributed environments. In addition to the technical challenges of providing reliable and efficient audio-visual communication, there are important social questions, in particular how users are able to control access to their personal environments, and how to advise other users about their level of availability. Within AMODEUS-21, an ESPRIT Basic Research Action concerned with the development, transfer and assessment of techniques for modelling human-computer interaction, a prototype media space has been analysed by various user and system oriented modelling techniques. This paper describes how formal specification can be used to express requirements on the interfaces needed to control access and availability in a media space. Beyond its obvious use in clarifying the subtle relationship between these concerns, the paper describes how the specification assists in assessing design options or ginating from other modelling disciplines.

Abstract

Abstract