This paper looks at how to extend the type of analysis that can be done using interactor based models of interactive systems, the i2smv tool, and SMV. Originally, the type of analysis performed with i2smv/SMV was concerned with the exhaustive exploration of all possible behaviours of a device, with little direct consideration of the tasks it should support. The paper investigates how task models can be introduced into the approach in order to extend the range of properties that can be analysed.
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.
This paper presents a novel adaptation mechanism that allows every node of a gossip-based broadcast algorithm to adjust the rate of message emission 1) to the amount of resources available to the nodes within the same broadcast group and 2) to the global level of congestion in the system. The adaptation mechanism can be applied to all gossip-based broadcast algorithms we know of and makes their use more realistic in practical situations where nodes have limited resources whose quantity changes dynamically with time without decreasing the reliability.
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.
A replicação de sistemas de gestão de bases de dados (SGBD) é um mecanismo fundamental para a fiabilidade de sistemas de informação. Em sistemas geograficamente distribuídos é ainda útil na recuperação de desas- tres e disponibilidade ubíqua de dados. Uma técnica de replicação recentemente proposta é a Database State Ma- chine (DBSM), que promete aliar fiabilidade a elevado desempenho tirando partido de sistemas de comunicação em grupo. A avaliação do desempenho desta técnica tem no entanto sido efectuada com redes de comunicação demasiado simples ou irrealistas e com uma carga não representativa. Este artigo propõe uma avaliação rigorosa de uma concretização desta técnica de replicação, aliando um modelo de simulação realista de redes de comunicação com uma geração de carga efectuada de acordo com os padrões elaborados pelo Transaction Processing Council (TPC). Os resultados obtidos confirmam o interesse desta técnica em redes locais, mas mostram que o seu desempenho é condicionado pelas características da rede e da carga.
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.
In this paper we propose the mutable con- sensus protocol, a pragmatic and theoretically appealing approach to enhance the performance of distributed con- sensus with a large number of participants. First, an apparently inefficient consensus protocol is developed using the very simple stubborn channel abstraction for unreliable message passing. Then, the introduction of judiciously chosen finite delays in the implementation of channels makes it likely that the transmission of some messages is avoided. Although this does not affect correctness, which rests on an asynchronous system model, the message exchange pattern at the network level changes noticeably and can be made to resemble several different protocols. A particularly appealing instantiation, called the permutation gossip, allows the protocol to scale gracefully to a large number of processes.
The lack of a commonly accepted denition 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 specied in Vdm and a working prototype is currently being used in an industrial environment.
Version vectors and their variants play a central role in update tracking in optimistic distributed systems. Existing mechanisms for a variable number of participants use a mapping from identities to integers, and rely on some form of global configuration or distributed naming protocol to assign unique identifiers to each participant. These approaches are incompatible with replica creation under arbitrary partitions, a typical mode of operation in mobile or poorly connected environments. We present an update tracking mechanism that overcomes this limitation; it departs from the traditional mapping and avoids the use of integer counters, while providing all the functionality of version vectors in what concerns version tracking.
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.
Os protocolos probabilistas, também designados por protocolos de propagação epidémica, têm recebido recentemente um interesse crescente devido à sua capacidade de escala. Uma das principais limitações deste tipo de protocolos é que podem consumir uma excessiva largura de banda. Este artigo discute um protocolo que combina a difusão probabilista com a fiabilidade semântica. Este novo protocolo alia o suporte de um elevado número de participantes com a tolerância de receptores lentos e congestão na rede. Nomeadamente, é apresentada a concretização do protocolo usando a moldura e objectos de suporte a composição e execução de micro-protocolos Appia assim como a avaliação ao do seu desempenho.
This paper describes a generic method to derive an animation from a recursive denition, with the objective of debugging and understanding this denition 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.
Total order multicast greatly simplifies the implementa- tion of fault-tolerant services using the replicated state ma- chine approach. The additional latency of total ordering can be masked by taking advantage of spontaneous order- ing observed in LANs: A tentative delivery allows the ap- plication to proceed in parallel with the ordering protocol. The effectiveness of the technique rests on the optimistic as- sumption that a large share of correctly ordered tentative deliveries offsets the cost of undoing the effect of mistakes. This paper proposes a simple technique which enables the usage of optimistic delivery also in WANs with much larger transmission delays where the optimistic assumption does not normally hold. Our proposal exploits local clocks and the stability of network delays to reduce the mistakes in the ordering of tentative deliveries. An experimental evalu- ation of a modified sequencer-based protocol is presented, illustrating the usefulness of the approach in fault-tolerant database management.
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.
This paper suggests functional programming languages with coinductive types as suitable devices for prototyping process calculi. The proposed approach is independent of any particular process calculus and makes explicit the different ingredients present in the design of any such calculi. In particular structural aspects of the underlying behaviour model (e.g. the dichotomies such as active vs reactive, deterministic vs nondeterministic) become clearly separated from the interaction structure which defines the synchronisation discipline. The approach is illustrated by the detailed development in Charity of an interpreter for a family of process languages.