This chapter explores the role that formal modelling may play in aiding the visualization and implementation of usability, with a particular emphasis on experience requirements in an ambient and mobile system. Mechanisms for requirements elicitation and evaluation are discussed, as well as the role of scenarios and their limitations in capturing experience requirements. The chapter then discusses the role of formal modelling by revisiting an analysis based on an exploration of traditional usability requirements before moving on to consider requirements more appropriate to a built environment. The role of modelling within the development process is re-examined by looking at how models may incorporate knowledge relating to user experience, and how the results of the analysis of such models may be exploited by human factors and domain experts in their consideration of user experience issues.
Too often software engineers see the user interface as a last layer that must be placed on top of the functional (or business logic) layer in order (simply?) to enable users access to its functionality. This vision rests on the assumption that all the application’s logic is at the functional level, and is independent of the user interface. The user interface then is simply a information transmission layer between the user and the “application” (i.e., the functional layer).
Functional programs are particularly well suited to formal manipulation by equational reasoning. In particular, it is straightforward to use calculational methods for program transformation. Well-known transformation techniques, like tupling or the introduction of accumulating parameters, can be implemented using calculation through the use of the fusion (or promotion) strategy. In this paper we revisit this transformation method, but, unlike most of the previous work on this subject, we adhere to a pure point-free calculus that emphasizes the advantages of equational reasoning. We focus on the accumulation strategy initially proposed by Bird, where the transformed programs are seen as higher-order folds calculated systematically from a specification. The machinery of the calculus is expanded with higher-order point-free operators that simplify the calculations. A substantial number of examples (both classic and new) are fully developed, and we introduce several shortcut optimization rules that capture typical transformation patterns.
In this paper we show how some of the recursion patterns typically used in algebraic programming can be defined using hylomorphisms. Most of these definitions were previously known. However, unlike previous approaches that use fixpoint induction, we show how to derive the standard laws of each recursion pattern by using just the basic laws of hylomorphisms. We also define the accumulation recursion pattern introduced by Pardo using a hylomorphism, and use this definition to derive the strictness conditions that characterize this operator in the presence of partiality. All definitions are implemented and exemplified in Haskell.
Many programs have an objective that can be precisely stated as the maximization of a function defined over its local variables. This is the case of utility-based software agents, which are reactive entities that try to maximize their welfare, usually accessed by an utility function. This paper introduces a programming language suitable for explicit programming with utility functions. Starting from a standard concurrent programming language, we added primitives to allow the parametrization of each process with an utility function that should be maximized. For the moment, using techniques of Markov decision problems, we can compile sequential programs, written in a restricted version of this new language, into equally behaved programs written in the original one. Major problems in developing such utility-based programming language are the need to compare the utility of infinite executions or the need to deal with uncertainty.
Recent accounts of accidents have drawn attention to problems that arise in safety critical systems through “automation surprises”. A particular class of such surprises, interface mode changes, may have significant impact on the safety of a dynamic interactive system and may take place implicitly as a result of other system action. Formal specifications of interactive systems may provide an opportunity to analyse problems that arise in such systems. In this paper we consider the role that an interactor based specification may have as a partial model of an interactive system, so that mode consequences might be checked early in the design process. We show how interactor specifications can be translated into the SMV model checker input language, and how we can use such specifications in conjunction with the model checker to analyse potential for mode confusion in a realistic case. Our final aim is to develop a general purpose methodology for the automated analysis of interactive systems, and, in this context, we show how the verification process can be useful by raising questions that have to be addressed in a broader context of analysis.
Integration of Mobile computers into Worldwide networks is traditionally managed by hosting them into the fixed network. We argue that this approach excludes some important forms of interaction. We present a communication mechanism, suitable for developing applications that take advantage of transient connections. These communications can be supported by several transport mechanisms, including Email and plain file copying between non networked computers. 1 Introduction Future applications can be expected to follow two major trends, Mobility and Worldwideness. These two issues are strongly interrelated as Worldwide systems often experience disconnected operation under network partitions and Mobile computers are partially integrated (possibly hosted) into worldwide networks. A common scenario for the integration of mobile hosts (MHs) is based on a fixed worldwide network to which MHs connect from time to time, either by fixed or wireless links.
The recent trend towards mobility and ubiquitous computing issued a new perspective over the traditional models of distributed computation. Observation of Human behavior, in particular the study of Human information interchange techniques and protocols presents a simple, yet fruitful, mean of gathering insight on the possible protocols for interaction among mobile hosts.This work will try to go one step further on the study of mobile interactions by leaving the usual semi-centralized approach to mobile computing. Instead of focusing on the reconciliation of mobile hosts with the networked support stations, we will study the possibility of progressive adjustments, both by a mobile host and a support station and between mobile hosts. 1 Introduction The recent trend towards mobility and ubiquitous computing issued a new perspective over the traditional models of distributed computation.
The GAMA-X system is a semi-automatic generator of assisted interfaces . It aims at being an UIMS (User Interface Management System) for the Camila system capable of providing an user interface that can be used at all levels of the application development cycle from the prototype to the nal implementation. The GAMA-X system is divided into two main modules the MGI (Interface Generation Module) and the MIU (User Interaction Module). The MGI generates an user interface specication or MIU specication from the computational layer specication The MIU creates an user interface based on the specication generated by the MGI. The MIU specications can be generated by the MGI or hand written from scratch In this manual we show with an example how to write the MIU specication.
