Abstract
The paper describes a model that includes an explicit description of the information resources that are assumed to guide use, enabling a focus on properties of "plausible interactions". The information resources supported by an interactive system should be designed to encourage the correct use of the system. These resources signpost a user's interaction, helping to achieve desired goals. Analysing assumptions about information resource support is particularly relevant when a system is safety critical that is when interaction failure consequences could be dangerous, or walk-up-and-use where interaction failure may lead to reluctance to use with expensive consequences. The paper shows that expressing these resource constraints still provides a wider set of behaviours than would occur in practice. A resource may be more or less salient at a particular stage of the interaction and as a result potentially overlooked. For example, the resource may be accessible but not used because it does not seem relevant to the current goal. The paper describes how the resource framework can be augmented with additional information about the salience of the assumed resources. A medical device that is in common use in many hospitals is used as illustration.

Abstract
In this paper we consider two very different case studies explored using scalable analysis techniques and stochastic process algebra. The first case study is a classical computer science problem: determining the efficiency of two non-repudiation protocols. We use PEPA to specify the model derived from the protocol specification and mean value analysis and fluid approximation to derive the desired metrics. In the second case study we model a human-centric system, concerning patient flow through a hospital clinic. The model is derived from the clinic practice and observed takt times are used to populate the model. We use PEPA and fluid approximations to derive measures. The two case studies demonstrate the power and versatility of the modelling and analysis approaches used. © 2013 Springer-Verlag.

Abstract
The paper is concerned with the comparative analysis of interactive devices. It compares two devices by checking systematically a set of template properties that are designed to explore important interface characteristics. The two devices are designed to support similar tasks in a clinical setting. The devices differ as a result of judgements based on a range of considerations including software. Variations between designs are often relatively subtle and do not always become evident through even relatively thorough user testing. Notwithstanding their subtlety, these differences may be important to the safety or usability of the device. The illustrated approach uses formal techniques to provide the analysis. This means that similar analysis can be applied systematically.

Abstract
It is well known that human error in the use of interactive devices can have severe safety or business consequences. It is important therefore that aspects of the design that compromise the usability of a device can be predicted before deployment. A range of techniques have been developed for identifying potential usability problems including laboratory based experiments with prototypes and paper based evaluation techniques. This paper proposes a framework that integrates experimental techniques with formal models of the device, along with assumptions about how the device will be used. Abstract models of prototype designs and use assumptions are analysed using model checking techniques. As a result of the analysis hypotheses are formulated about how a design will fail in terms of its usability. These hypotheses are then used in an experimental environment with potential users to test the predictions. Formal methods are therefore integrated with laboratory based user evaluation to give increased confidence in the results of the usability evaluation process. The approach is illustrated by exploring the design of an IV infusion pump designed for use in a hospital context. © 2013 Springer-Verlag Berlin Heidelberg.

Abstract

Abstract