Abstract
This paper discusses a method for the analysis of dependable interactive systems using model checking, and its support by a tool designed to make it accessible to a broader community. The method and the tool are designed to be of value to system engineers, usability engineers and software engineers. It has been designed to help usability engineers by making those aspects of the analysis relevant to them explicit while concealing those aspects of modelling and model checking that are not relevant. The paper presents the results of a user evaluation of the effectiveness of aspects of the tool and how it supports the proposed method. © Springer Science + Business Media, LLC 2006.

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. © 2011 BCS.

Abstract
The engineering of ubiquitous computing systems provides important challenges. Not least among these is the need to understand how to implement designs that create a required experience for users. The paper explores a particular class of such systems for built environments. In particular it is concerned with the capture of experience requirements and production of prototypes that create experience. The aim is to develop methods and tools for such environments to enable the creation of particular sorts of experience in users. An approach that combines the use of scenarios, personae and snapshots with the use of prototypes and models is described. The technique aims to elicit an understanding of the required experience of the system and then create a design that satisfies the requirements. © 2008 Springer Berlin Heidelberg.

Abstract
Mobility of ubiquitous systems offers the possibility of using the current context to infer information that might otherwise require user input. This can either make user interfaces more intuitive or cause subtle and confusing mode changes. We discuss the analysis of such systems that will allow the designer to predict potential pitfalls before the design is fielded. Whereas the current predominant approach to understanding mobile systems is to build and explore experimental prototypes, our exploration highlights the possibility that early models of an interactive system might be used to predict problems with embedding in context before costly mistakes have been made. Analysis based on model checking is used to contrast configuration and context issues in two interfaces to a process control system. © IFIP International Federation for Information Processing 2005.

Abstract
Understanding the properties of interactions is essential to the design of effective interactive systems involving two or more agents, and to the evaluation of existing systems. This understanding can inform the design of multi-agent systems by helping the designer identify properties that a system should conform to. In addition, a focus on the properties of interactions can lead to a better understanding of the space of possibilities, by recognizing features of multi-agent systems which are often simply incidental outcomes of design, not explicitly considered in the design specification. We present an Interaction Framework, in which abstract interactional requirements and properties can be expressed in a way which is not biased towards the perspective of any one agent to the interaction. These can be used to derive requirements on the design of computer systems, to highlight those aspects of users which influence the properties of the interaction, and hence to guide the design of the interactive system.

Abstract
This short paper argues that references in user interfaces, in particular names and the values they denote, are often designed in a way that is incomplete and inconsistent thereby causing problems for users. This paper explores names and values through illustrations in order to clear the way for a more systematic approach to the design of names and reference. © 2007 Harold Thimbleby, Michael Harrison,.