Abstract
As developers target a more diverse range of devices, a one-size-fits-all approach to interaction design becomes harder to sustain. By utilising the notion of interaction styles, developers can create families of user interfaces that are better matched to the interactive capabilities of devices. Style-Based Mark-up Language (SBML) is a language that separates services from style-specific interaction, and allows devices to choose the style of interface that best suits their capability and operating context. This paper outlines the service architecture and language syntax of SBML, using an online banking example. It also explores alternative single-interaction-style approaches and notions of context. Copyright © 2008 Inderscience Enterprises Ltd.

Abstract
Interactors are components in the description of an interactive system that encapsulate a state, the events that manipulate the state, and the means by which the state is made perceivable to users of the system (the presentation). This paper concerns the relationship between the models of interactors that are being developed, at York and Pisa, in the context of Esprit Basic Research Action 7040 (Amodeus-2). The models differ in their expression of the three components of an interactor, and after relating the models to the informal notion of interactor we describe the context in which the view of interaction afforded by each model is appropriate. © 1994 ACM.

Abstract
This paper describes how the HOPS notation can be used to support Human Centered Design. It discusses the role of the notation in providing multiple design viewpoints. It demonstrates how the HOPS tool can be used to animate these viewpoints. Finally, HOPS is used to specify how the system provides information resources for user action. This approach to specifying plausible user behavior is contrasted with a task based approach. The HOPS based design techniques are illustrated through a process control example. © 2010 ACM.

Abstract
The long term vision of smart service systems in which electronic environments are made sensitive and responsive to the presence of, possibly many, people is gradually taking shape through a number of pilot projects. The purposes of such systems vary from intelligent homes that assist their inhabitants to make their lives more independent and comfortable to much larger environments such as airports in which people are provided with context aware, personalised, adaptive and anticipatory services that are most relevant for them given their location and their current activities. This paper is concerned with the exploration of scalable formal models that can address the collective behaviour of a large number of people moving through a smart environment. © 2010 ACM.

Abstract
Smart environments (e.g., airports, hospitals, stadiums, and other physical spaces using ubiquitous computing to empower many mobile people) provide novel challenges for usability engineers. Firstly, interaction can be implicit and therefore unintentional on the part of its users. Secondly, the impact of a smart environment can influence the collective or crowd behavior of those immersed within it. These challenges lead to requirements for complementary analyses which must be combined with the more typical focus on the interaction between user and device. The paper explores a family of stochastic models aimed at analyzing these features with a particular focus on crowd interaction. Copyright 2009 ACM.

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. 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. © 2010 IEEE.