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 usability issues. In this context, the application 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.

Multi-player games are increasingly popular in the Internet. This growing interest results in the need to support a high number of participants, which raises the issue of scalability, namely in what regards the ability to offer good performance in such a large-scale setting. This paper addresses the issue of designing middleware solutions to support large-scale multi-player applications. In particular, we are interested in studying the feasibility of using epidemic multicast protocols for information dissemination in multi-player games based on a peer-to-peer architecture. We have integrated a comercial multiplayer game, the Microsoft Flight Simulator 2002, with an epidemic multicast protocol appropriate to this kind of applications, the NEEM. The paper describes how this integration was achieved and presents evaluation results of the resulting prototype.

Epidemic, or probabilistic, multicast protocols have emerged as a viable mechanism to circumvent the scalabil- ity problems of reliable multicast protocols. However, most existing epidemic approaches use connectionless transport protocols to exchange messages and rely on the intrinsic robustness of the epidemic dissemination to mask network omissions. Unfortunately, such an approach is not network- friendly, since the epidemic protocol makes no effort to re- duce the load imposed on the network when the system is congested. In this paper, we propose a novel epidemic protocol whose main characteristic is to be network-friendly. This property is achieved by relying on connection-oriented transport connections, such as TCP/IP, to support the com- munication among peers. Since during congestion mes- sages accumulate in the border of the network, the pro- tocol uses an innovative buffer management scheme, that combines different selection techniques to discard messages upon overflow. This technique improves the quality of the information delivered to the application during periods of network congestion. The protocol has been implemented and the benefits of the approach are illustrated using a com- bination of experimental and simulation results.

The lack of a commonly accepted denition of a software component, the proliferation of competing `standards' and component frameworks, is here to stay, raising the fundamental question in component based development of how to cope in practice with heterogeneity. This paper reports on the design of a Component Repository aimed to give at least a partial answer to the above question. The repository was fully specied in Vdm and a working prototype is currently being used in an industrial environment.

p>Os protocolos de difusão são muito utilizados na construção de sistemas distribuídos.
Neste contexto,a habilidade semântica é um novo modelo de coerência introduzido recentemente que explora o conceito de obsolescência:uma mensagem torna-se obsoleta quando o seu conteúdo. É sobreposto por uma outra mensagem mais recente. O conhecimento de quais as mensagens obsoletas pode ser usado para libertar recursos, aumentando o desempenho do sistema. Este artigo aborda os desafios de realizar uma concretização modular de uma pilha de protocolos oferecendo habilidade semântica. Esta concretização foi realizada usando uma moldura de objectos de suporte composição e
execução de micro-protocolos. Ao contrário do que acontece em concretizáveıs monolíticas,
numa concretização modular as mensagens em processamento na pilha de protocolos encontram-se dispersas por diferentes camadas, dificultando a tarefa de aplicar relações de
obsolescência.

This paper describes a generic method to derive an animation from a recursive denition, with the objective of debugging and understanding this denition by expliciting its control structure. This method is based on a well known algorithm of factorizing a recursive function into the composition of the producer and the consumer of its call tree. We developed a systematic method to transform both the resulting functions in order to draw the tree step by step. The theory of data types as xed points of functors, generic recursion patterns, and monads, are fundamental to our work and are brie y presented. Using polytypic implementations of monadic recursion patterns and an application to manipulate and generate graph layouts we developed a prototype that, given a recursive function written in a subset of Haskell, returns a function whose execution yields the desired animation.

View Synchrony (VS) is a powerful abstraction in the design and implementation of de- pendable distributed systems. By ensuring that processes deliver the same set of messages in each view, it allows them to maintain consistency across membership changes. However, experience indicates that it is hard to combine strong reliability guarantees as offered by VS with stable high performance. In this paper we propose a novel abstraction, Semantic View Synchrony (SVS), that exploits the application's semantics to cope with high throughput applications. This is achieved by allowing some messages to be dropped while still preserving consistency when new views are installed. Thus, SVS inherits the elegance of view synchronous communi- cation. The paper describes how SVS can be implemented and illustrates its usefulness in the context of distributed multi-player games.