A generation of interoperable devices is emerging in control systems. Devices can be controlled by users at multiple levels. The devices that are controlled may be certified as safe by their vendors, but new issues may arise from their integration and remote use, as new interaction pathways will be enabled that are simply not possible when the device is used as a stand-alone system. This paper is concerned with modelling concrete interfaces that are designed to enable use of these systems. It builds on previous work concerned with proving use-centred safety properties across the interoperable system. The concern of this paper however is describing the relationship between an abstract model and a concrete interface that reflects more concretely the tasks that the users are intended to perform. In the example used in this paper, a menu interface is built on top of the abstract interface. The primary concern of the paper is describing the relationship between the abstract interface and the specified concrete interface. Properties of the interface that were discussed in previous work are proved of the concrete interface. This paper uses, as an example, use-centred safety properties of integrated clinical environments for remote medical care. Four properties are considered briefly: consistency , completeness , feedback and reversibility with an understanding of the tasks that users may perform. More detail will be given to the first two with a particular focus on the relation between the abstract interaction model and a concrete menu based model. The properties are formalised in the language of the PVS verification system. They are mechanically verified using the PVS proof assistant for a model of a realistic prototype of an integrated clinical environment. The presented analysis is intended to be performed during system design and development, and before the actual system is deployed, to increase confidence that the design complies with important use-centred safety properties that capture design guidelines discussed in usability engineering standards. It is envisaged that such an analysis could help inform a safety assessment of the integrated system.

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.

Use error due to user interface design defects is a major concern in many safety critical domains, for example avionics and health care. Early detection of latent user interface problems can be facilitated by user-centered design methods that integrate formal verification technologies. This article considers the role that formal verification technologies can play in the context of user-centered design by considering the following three existing tools: CIRCUS, PVSio-web, and IVY. These tools have been developed to support the model based analysis of critical user interfaces. They have their foundations in existing formal verification technologies, but each of them is focused towards particular issues relating to user interface design. The article explores the different phases of the user-centered design process and the extent to which each of these tools supports these phases. Criteria are developed for assessing their role at each stage of the design process. The results of the evaluation provide guidance to developers to help choose the most appropriate tool based on their analysis needs while at the same time setting challenges for future developments.

The paper describes templates for model-based analysis of usability and safety aspects of user interface software design. The templates crystallize general usability principles commonly addressed in user-centred safety requirements, such as the ability to undo user actions, the visibility of operational modes, and the predictability of user interface behavior. These requirements have standard forms across different application domains, and can be instantiated as properties of specific devices. The modeling and analysis process is carried out using the Prototype Verification System (PVS), and is further facilitated by structuring the specification of the device using a format that is designed to be generic across interactive systems. A concrete case study based on a commercial infusion pump is used to illustrate the approach. A detailed presentation of the automated verification process using PVS shows how failed proof attempts provide precise information about problematic user interface software features.

One part of demonstrating that a device is acceptably safe, often required by regulatory standards, is to show that it satisfies a set of requirements known to mitigate hazards. This paper is concerned with how to demonstrate that a user interface software design is compliant with use-related safety requirements. A methodology is presented based on the use of formal methods technologies to provide guidance to developers about addressing three key verification challenges: 1) how to validate a model, and show that it is a faithful representation of the device; 2) how to formalize requirements given in natural language, and demonstrate the benefits of the formalization process; and 3) how to prove requirements of a model using readily available formal verification tools. A model of a commercial device is used throughout the paper to demonstrate the methodology. A representative set of requirements are considered. They are based onUS Food and Drug Administration (FDA) draft documentation for programmable medical devices, and on best practice in user interface design illustrated in relevant international standards. The methodology aims to demonstrate how to achieve the FDA's agenda of using formal methods to support the approval process for medical devices.

This paper describes the application of the IVY workbench to the formal analysis of a user interface for a safety-critical aerospace system. The operation manual of the system was used as a requirement document, and this made it possible to build a reference model of the user interface, focusing on navigation between displays, the information provided by each display, and how they are interrelated. Usability-related property specification patterns were then used to derive relevant properties for verification. This paper discusses both the modeling strategy and the analytical results found using the IVY workbench. The purpose of the reference model is to provide a standard against which future versions of the interface may be assessed.

Analysis of the usability of an interactive system requires both an understanding of how the system is to be used and a means of assessing the system against that understanding. Such analytic assessments are particularly important in safety-critical systems as latent vulnerabilities may exist which have negative consequences only in certain circumstances. Many existing approaches to assessment use tasks or scenarios to provide explicit representation of their understanding of use. These normative user behaviours have the advantage that they clarify assumptions about how the system will be used but have the disadvantage that they may exclude many plausible deviations from these norms. Assessments of how a design fails to support these user behaviours can be a matter of judgement based on individual experience rather than evidence. We present a systematic formal method for analysing interactive systems that is based on constraints rather than prescribed behaviour. These constraints capture precise assumptions about what information resources are used to perform action. These resources may either reside in the system itself or be external to the system. The approach is applied to two different medical device designs, comparing two infusion pumps currently in common use in hospitals. Comparison of the two devices is based on these resource assumptions to assess consistency of interaction within the design of each device.

Abstract Pervasive environments offer an increasing number of services to a large number of people moving within these environments, including timely information about where to go and when, and contextual information about the surrounding environment. This information may be conveyed to people through public displays or direct to a person’s mobile phone. People using these services interact with the system but they are also meeting other people and performing other activities as relevant opportunities arise. The design of such systems and the analysis of collective dynamic behaviour of people within them is a challenging problem. We present results on a novel usage of a scalable analysis technique in this context. We show the validity of an approach based on stochastic process-algebraic models by focussing on a representative example, i.e. emergency egress. The chosen case study has the advantage that detailed data is available from studies employing alternative analysis methods, making cross-methodology comparison possible. We also illustrate how realistic, context-dependent human behaviour, often observed in emergency egress, can naturally be embedded in the models, and how the effect of such behaviour on evacuation can be analysed in an efficient and scalable way. The proposed approach encompasses both the agent modelling viewpoint, as system behaviour emerges from specific (discrete) agent interaction, and the population viewpoint, when classes of homogeneous individuals are considered for a (continuous) approximation of overall system behaviour.

Pervasive environments offer an increasing number of services to a large number of people moving within these environments including timely information about where to go and when. People using these services interact with the system but they are also meeting other people and performing other activities as relevant opportunities arise. The design of such systems and the analysis of collective dynamic behaviour of people within them is a challenging problem. In previous work we have successfully explored a scalable analysis of stochastic process algebraic models of smart signage systems. In this paper we focus on the validation of a representative example of this class of models in the context of emergency egress. This context has the advantage that detailed data is available from studies with alternative analysis methods. A second aim is to show how realistic human behaviour, often observed in emergency egress, can be embedded in the model and how the effect of this behaviour on building evacuation can be analysed in an efficient and scalable way.

Model checking is a formal technique for the automated analysis of system models against formal requirements. Once a suitable model and property have been specified, no further interaction by the analyst is required. However, this does not make the method necessarily user friendly since the checker must be provided with appropriate and complex input data. Furthermore, counter-examples generated by the system are often difficult to interpret. Because of this complexity, model checking is not commonly used, and exhaustive exploration of system models based on finite state descriptions is not exploited within industrial dependable systems design. The paper describes the development of an integrated collection of tools around SMV, intended to make it more accessible to practicing software engineers and in particular those concerned with the human interface issues in complex safety critical systems.

Abstract. Formal approaches to the design of interactive systems rely on reasoning about properties of the system at a very high level of abstraction. Specifications to support such an approach typically provide little scope for reasoning about presentations and the representation of information in the presentation. In contrast, psychological theories such as distributed cognition place a strong emphasis on the role of representations, and their perception by the user, in the cognitive process. However, the post-hoc techniques for the observation and analysis of existing systems which have developed out of the theory do not help us in addressing such issues at the design stage. Mn this paper we show how a formalisation can be used to investigate the representational aspects of an interface. Our goal is to provide a framework to help identify and resolve potential problems with the representation of information, and to support understanding of representational issues in design. We present a model for linking properties at the abstract and perceptual levels, and illustrate its use in a case study of a ight deck instrument. There is a widespread consensus that proper tool support is a prerequisite for the adoption of formal techniques, but the use of such tools can have a profound effect on the process itself. In order to explore this issue, we apply a higher-order logic theorem prover to the analysis.

In this article we present a new approach to interaction modeling based on the concept of information resources. The approach is inspired by recent distributed cognition (DC) literature but develops a model that applies specifically to human-computer interaction (HCI) modeling. Of course, there are many approaches to modeling HCI, and the motivation of this article is not to offer yet another approach. Rather, our motivation is that the recent developments in DC are so obviously relevant to HCI modeling and design, yet the ideas have lacked visibility in the HCI community. By providing a model whose concepts are rooted in DC concepts, we hope to achieve this visibility. DC research identifies resources for action as central to the interaction between people and technologies, but it stops short of providing a definition of such resources at a level that could be used to analyze interaction. The resources model described in this article defines a limited number of resource types as abstract information structures that can be used to analyze interaction. We demonstrate how these abstract types can be represented differently in an interface. The resources model uses the concept of interaction strategy to describe the way in which different configurations of resources can differently shape users' actions. These 2 components of the resources model (information structures and interaction strategies), through the process of coordination and integration, provide a link among devices, representations, and actions that is not well articulated in the DC literature.

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-2 1 , 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 originating from other modelling disciplines.

Article Free Access Share on Locating the scene: the particular and the general in contexts for ambulance control Authors: John C. McCarthy Department of Applied Psychology, University College Cork, Cork, Ireland Department of Applied Psychology, University College Cork, Cork, IrelandView Profile , Peter C. Wright Department of Computer Science, University Of York, York YO1 5DD, England Department of Computer Science, University Of York, York YO1 5DD, EnglandView Profile , Patrick Healey Department of Applied Psychology, University College Cork, Cork, Ireland Department of Applied Psychology, University College Cork, Cork, IrelandView Profile , Andrew Dearden Department of Computer Science, University Of York, York YO1 5DD, England Department of Computer Science, University Of York, York YO1 5DD, EnglandView Profile , Michael D. Harrison Department of Computer Science, University Of York, York YO1 5DD, England Department of Computer Science, University Of York, York YO1 5DD, EnglandView Profile Authors Info & Claims GROUP '97: Proceedings of the 1997 ACM International Conference on Supporting Group WorkNovember 1997 Pages 101–110https://doi.org/10.1145/266838.266874Published:16 November 1997Publication History 12citation505DownloadsMetricsTotal Citations12Total Downloads505Last 12 Months14Last 6 weeks3 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

This paper describes a generic model for case memory systems expressed using the Z notation. A case memory system is an essential part of any case-based reasoning system, and provides a mechanism for storing old cases, and for assessing the relationship between the stored cases and a new problem. Using the model, characteristics that have been claimed for specific case memory systems in the literature, e.g. responsiveness to a reasoner's goals or use of past experience in case assessment, are expressed formally in terms of constraints on the means by which case relations are computed. The model supports precise reasoning about the characteristics of specific systems and offers insight into the variety of options available to software or knowledge engineers seeking to reuse a case memory system, to select a case memory system shell or to develop a new system.

We put forward an approach to deriving and applying human error tolerance requirements. Such requirements are concerned with the response of a system to errors introduced by human operators. The approach provides a means by which operators' tasks can be described and analysed for likely errors and the impact of these errors on system safety can be explored. The approach, based on previous work by the same authors (P. Wright et al., 1994), uses a software engineering notation to provide the bridge between operator models and systems engineering concerns. The approach is extended to include a more refined understanding of the processes that contribute to human error. The operators' process in achieving goals is understood in terms of structured tasks. With this additional apparatus we are able to capture a more complex set of human error forms.

Requirements that involve the usability of systems can be properties of interactions rather than systems alone. This proposition is demonstrated by means of four examples. The authors suggest that a notation like CSP (communicating sequential processes) may be used to provide a framework for considering different modeling approaches. Interaction requirements that relate to multiwindowed systems, walk up and use systems, and dynamic systems such as power stations are considered. It is shown how models provide different representations to which advice from the different disciplines of human computer interaction may be applied.>

Abstract The concept of an ‘interactor’ has been introduced by Faconti and Paterno' [6] as an abstraction of an entity in interactive graphics capable of both input and output. However the notion of interaction object need not be confined to graphics systems; it represents a useful structure for thinking and reasoning about the behaviour of interactive systems in general. As part of Esprit Basic Research Action 7040 (Amodeus‐2) we are using the concept of interactor, and existing work on state‐based processes and agents, to develop a model and theory of interactive systems. In this paper we describe two formal models for interaction objects and sketch how they can be used to build a small vocabulary of operators to support the rigorous specification of a graphics system. Our model differs from the approach of Faconti and Paterno' in that it abstracts away from any specific graphics framework and is thus suited to the level of abstraction demanded by formal approaches to system development.

This article is concerned with an analysis of the requirements for text-based on-line conferencing. From a system perspective, text-based on-line conferencing can be viewed as either message passing or data sharing. These complementary views give rise to different design dimensions. For example, the message-passing view is concerned with granularity, channels, message labels, and so on. The data-sharing view is concerned with the access different individuals have to the text: read only, appending, editing, pointing, and so on. A deliberately sparse prototype was built and placed in this design space. This minimal prototype has limited functionality so that the real problems experienced by users can show through. Relevant literature from disciplines such as social psychology, conversational analysis, and linguistics is briefly reviewed in terms of three generic communication tasks: synchronizing communication, maintaining structural coherence, and maintaining referents. An empirical analysis of subjects' use of the sparse prototype was analyzed to establish the relevance of the generic communication tasks to text-based on-line conferencing. Possible forms that support for these tasks might take are discussed.

First order logic provides a means of integrating the specification and prototyping of interactive systems. It can describe graphical images in a declarative and order independent manner. It supports the definition of abstract devices which avoid the complexity of representing ‘raw’ input from a variety of physical devices. The following pages show how such techniques must be extended in order to prototype and reason about dynamic interaction with graphical interfaces. The incorporation of a temporal ordering into logical specifications provides a means of describing changes in the structure of graphical images. It can also identify the sequencing which may be implicit within specifications of interactive dialogues. This paper describes how PRELOG, a tool for Presenting and REndering LOGic specifications of interactive systems, has been extended to include a temporal logic interpreter.

Staff in the Departments of Computer Science and Psychology at the University of York have been cooperating in interdisciplinary research since 1983. The mainstream of York's approach is to apply theory developed in these parent disciplines to HCI design. Our goal is to integrate formal and empirical methods. By formal methods we mean mathematical models that are capable of capturing properties of a user interface. By empirical methods we mean the observation and measurement of user behaviour. Integration of these two approaches is achieved by an iterative design process in which formal models are successively refined by testing their predictions against the results of user trials.

Formal specifications provide the non-specialist with an extremely poor impression of what it would be like to interact with a computer system. Prototypes provide a far better impression of the ‘look and feel’ of possible implementations but lack the precision of more formal approaches. Unfortunately, specification and prototyping are typically treated as alternatives. If these two activities can be harnessed then the designer has a means of incorporating the user into systems design. Tools can ease the transition from specification to prototype by supporting the visualisation of a design in terms of graphical representations of the proposed system. This paper describes Prelog, a tool for Presenting and REndering LOGic specifications of interactive systems. Prelog supports the structured representation of interaction objects which describe virtual devices. Interaction objects support reasoning about prototypes because they provide a means of abstracting away from device dependent pragmatics which make renderings intractable.