Abstract

Abstract

Abstract

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.