Abstract

Abstract
The quality of an interactive system can be measured in terms of its usability. Empirical approaches to usability evaluation attempt to assess the system under real usage conditions. This type of approach can be very expensive. Analytical approaches have been proposed as a means of reasoning about usability issues from early in development. These approaches use models to focus the analysis in specific usuability issues. In this context, the aplication of (mathematically) formal notations and tools has been proposed. This paper presents a formal approach to the analysis of interactive systems. The analysis can be carried out taking into account all possible behaviours of the device, or it can be guided by the tasks the device is supposed to support.

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
Genericity is a topic which is not sufficiently developed in state-based systems modelling, mainly due to a myriad of approaches and behaviour models which lack unification. This paper adopts coalgebra theory to propose a generic notion of a state-based software component, and an associated calculus, by quantifying over behavioural models specified as strong monads. This leads to the pointfree, calculational reasoning style which is typical of the so-called Bird-Meertens school. ©2003 Published by Elsevier Science B. V.