Abstract
Although the take-up of formal approaches to modelling and reasoning about software has been slow, there has been recent interest and facility in the use of automated reasoning techniques such as model checking 151 oil increasingly complex systems. In the case of interactive systems, formal methods can be particularly useful in reasoning about systems that involve complex interactions. These techniques for the analysis of interactive systems typically focus on the device and leave the context of use undocumented. In this paper we look at models that incorporate complexity explicitly, and discuss how they can be used in a formal setting. The paper is concerned particularly with the type of analysis that can be performed with them.

Abstract
In recent years, advances in software tools have made it easier to analyze interactive system specifications, and the range of their possible behaviors. However, the effort involved in producing the specifications of the system is Still Substantial. and a difficulty exists regarding the specification of plausible behaviors on the part of the user. Recent trends in technology towards more mobile and distributed Systems further exacerbates the issue, as contextual factors come in to play, and less structured, more opportunistic behavior on the part of the user makes purely task-based analysis difficult. In this paper we consider a resourced action approach to specification and analysis. In pursuing this approach we have two aims - firstly. to facilitate a resource-based analysis of user activity. allowing resources to be distributed across a number of artifacts, and secondly to consider within the analysis a wider range of plausible and opportunistic user behaviors without a heavy specification overhead, or requiring commitment to detailed user models.

Abstract

Abstract
The paper explores the role that formal modeling may play in aiding the visualization and implementation of usability requirements of a control panel. We propose that this form of analysis should become a systematic and routine aspect of the development Of Such interfaces. We use a notation for describing the interface that is convenient to use by software engineers, and describe a set of tools designed to make the process systematic and exhaustive.

Abstract
We investigate here an approach to modelling the dynamic information requirements of a user performing a number of tasks, addressing both the provision and representation of information, viewing the information as being distributed across a set of resources. From knowledge of available resources at the user interface, and task information needs we can identify whether the system provides the user with adequate support for task execution. We look at how we can use tools to help reason about these issues, and illustrate their use through an example. We also consider a full range of analyses suggested using this approach which could potentially be supported by automated reasoning systems.

Abstract