Abstract
With increasing use of computing systems while on the move and in constantly changing conditions, whether it is via mobile devices, wearable computers or embedded systems in the environment, time plays an increasingly important role in interaction. The way in which information is represented in an interface is fundamental to interaction with it, and how the information is used in the users tasks and activities. Dynamic representations where the user must perceive changes in the information displayed over time pose a further challenge to the designer. Very often this information is integrated with information from the environment in the performance of the user's tasks. The diminutive size and limited display capabilities of many ubiquitous and mobile computing devices further motivate careful design of these displays. In this paper we look at how time can be taken into account when reasoning about representational issues from the early stages of design. We look at a model which can be used to reason about these issues in a structured fashion, and apply it to an example.

Abstract
This paper looks at how to extend the type of analysis that can be done using interactor based models of interactive systems, the i2smv tool, and SMV. Originally, the type of analysis performed with i2smv/SMV was concerned with the exhaustive exploration of all possible behaviours of a device, with little direct consideration of the tasks it should support. The paper investigates how task related knowledge can be introduced into the approach in order to extend the range of properties that can be analysed.

Abstract

Abstract

Abstract

Abstract
In this paper we argue that using verification in interactive systems development is more than just checking whether the specification of the system has all the required properties; and that changing the focus from a global specification into partial, property oriented, specifications can provide a number of advantages and make verification act as an aid to decision making. We also present a compiler that allows for the verification of interactor specifications to be done in SMV, as well as a simple case study where verification is used to inform a design decision.