Abstract
Engineering natural and appropriate interactive behaviour in ubiquitous computing systems presents new challenges to their developers. This paper explores formal models of interactive behaviour in ubiquitous systems. Of particular interest is the way that these models may help engineers to visualise the consequences of different designs. Design options based on a dynamic signage system (GAUDI) are explored using different instances of a generic model of the system.

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
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
In recent years, several approaches to the analysis of automation systems dependability through the application of formal verification techniques have been proposed. Much of the research has been concerned with the modelling languages used, and how best to express the automation systems, so that automated verification might be possible. Less attention, however, has been devoted to the process of writing properties that accurately capture the requirements that need verification. This is however a crucial aspect of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skilful process, and indeed there have been reports of properties being wrongly expressed. In this paper we put forward a tool and a collection of property patterns that aim at providing help in this area. Copyright

Abstract
Analytic usability analysis methods have been proposed as an alternative to user testing in early phases of development due to the cost of the latter approach. By working with models of the systems, analytic models are not capable of identifying implementation related problems that might have an impact on usability. Model-based testing enables the testing of an implemented software artefact against a model of what it should be (the oracle). In the case of model-based user interface testing, the models should be expressed at an adequate level of abstraction, adequately modelling the interaction process. This paper describes an effort to develop tool support enabling the use of task models as oracles for model-based testing of user interfaces.