Abstract
This paper presents an interaction model for pervasive computing environments supporting localized activities, i.e., activities strongly associated to a specific physical environment. We are particularly interested in activities performed by occasional visitors to public spaces. This interaction model is characterized by an activity-centered approach to pervasive computing and is defined in a conceptual model inspired by Activity Theory. ActivitySpot, a software infrastructure implementing this conceptual model, is also presented. User interaction in ActivitySpot is based on simple, everyday pervasive computing devices, which facilitates usage learning and allows for a wide user population. ActivitySpot has supported the deployment of several pervasive computing solutions for localized activities. Our conceptual model has been evaluated by user studies run at different public spaces and global results demonstrate the model's suitability to the targeted type of scenario.

Abstract
This paper presents a new approach in plant modeling for the formal verification of real time systems. A system composed by two tanks is used, where all its components are modeled by simple modules and all the interdependences of the system's modular models are presented. As innovating parameters in the plant modeling, having as purpose its use on formal verification tasks, the plant is modeled using Dymola software and Modelica programming language. The results obtained in simulation are used to define the plant models that are used for the formal verification tasks, using the model-checker UPPAAL. The paper presents, in a more detailed way, the part of this work that is related to formal verification, being pointing out the used plant modeling approach. © 2007 IFAC.

Abstract

Abstract
When modelling complex interactive systems, traditional interactor-based approaches suffer from lack of expressiveness regarding the composition of the different interactors present in the user interface model into a coherent system. In this paper we investigate an alternative approach to the composition of interactors for the specification of complex interactive systems which is based on the coordination paradigm. We layout the fundations for the work and present an illustrative example. Lines for future work are identified.

Abstract
There is an inherent trade-off between epidemic and deterministic tree-based broadcast primitives. Tree-based approaches have a small message complexity in steady-state but are very fragile in the presence of faults. Gossip, or epidemic, protocols have a higher message complexity but also offer much higher resilience. This paper proposes an integrated broadcast scheme that combines both approaches. We use a low cost scheme to build and maintain broadcast trees embedded on a gossip-based overlay. The protocol sends the message payload preferably via tree branches but uses the remaining links of the gossip overlay for fast recovery and expedite tree healing. Experimental evaluation presented in the paper shows that our new strategy has a low overhead and that is able to support large number of faults while maintaining a high reliability.

Abstract
Gossip, or epidemic, protocols have emerged as a powerful strategy to implement highly scalable and resilient reliable broadcast primitives. Due to scalability reasons, each participant in a gossip protocol maintains a partial view of the system. The reliability of the gossip protocol depends upon some critical properties of these views, such as degree distribution and clustering coefficient. Several algorithms have been proposed to maintain partial views for gossip protocols. In this paper we show that tinder a high number of faults, these algorithms take a long time to restore the desirable view properties. To address this problem, we present HyParView, a new membership protocol to support gossip-based broadcast that ensures high levels of reliability even in the presence of high rates of node failure. The HyFarView protocol is based on a novel approach that relies in the use of two distinct partial views, which are maintained with different goals by different strategies.