Data aggregation plays an important role in the design of scalable systems, allowing the determination of meaningful system-wide properties to direct the execution of distributed applications. In the particular case of wireless sensor networks, data collection is often only practicable if aggregation is performed. Several aggregation algorithms have been proposed in the last few years, exhibiting different properties in terms of accuracy, speed and communication tradeoffs. Nonetheless, existing approaches are found lacking in terms of fault tolerance. In this paper, we introduce a novel fault-tolerant averaging based data aggregation algorithm. It tolerates substantial message loss (link failures), while competing algorithms in the same class can be affected by a single lost message. The algorithm is based on manipulating flows (in the graph theoretical sense), that are updated using idempotent messages, providing it with unique robustness capabilities. Furthermore, evaluation results obtained by comparing it with other averaging approaches have revealed that it outperforms them in terms of time and message complexity.

Data aggregation plays a basal role in the design of scalable distributed applications, allowing the determination of meaningful system-wide properties to direct the execution of the system. For instance, aggregation can be used to estimate: the size of the network to dimension of Distributed Hash Table (DHT) structures, or to set a quorum in dynamic settings; the average system load to guide local loadbalancing decisions; the total network disk space in a P2P sharing system. In the particular case of Wireless Sensor Networks (WSN), due to energy constraints, data collection is often only practicable if aggregation is performed.

As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. A correct understanding of the logics in which properties are expressed is needed in order to guarantee that properties correctly encode the intent of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skilful process. Errors in this step of the process can create serious problems since a false sense of security if gained with the analysis. However, when compared to the effort put into developing and applying modelling languages, little attention has been devoted to the process of writing properties that accurately capture verification requirements. This paper illustrates how a collection of property patterns, and its tool support, can help in simplifying the process of generating logical formulae from informally expressed requirements.

Automation systems according to IEC 61850 are a powerful solution for station automation. Engineering of such distributed systems is however a non-trivial task which requires different approaches and enhanced tool support. In this paper the authors (i) present how IEC 61850 is viewed and is being adopted by a utility and vendor, (ii) discuss its engineering potential and current issues, (iii) point-out global requirements for next generation tools, (iv) present the InPACTproject which is tackling some of these concerns and (v) propose key elements of visual languages as one contributing enhancement.

Ubiquitous computing poses new usability challenges that cut across design and development. We are particularly interested in "spaces" enhanced with sensors, public displays and personal devices. How can prototypes be used to explore the user's mobility and interaction, both explicitly and implicitly, to access services within these environments? Because of the potential cost of development and design failure, the characteristics of such systems must be explored using early versions of the system that could disrupt if used in the target environment. Being able to evaluate these systems early in the process is crucial to their successful development. This paper reports on an effort to develop a framework for the rapid prototyping and analysis of ambient intelligence systems.

This paper presents techniques developed to check program equivalences in the context of cryptographic software development, where specifications are typically reference implementations. The techniques allow for the integration of interactive proof techniques (required given the difficulty and generality of the results sought) in a verification infrastructure that is capable of discharging many verification conditions automatically. To this end, the difficult results in the verification process (to be proved interactively) are isolated as a set of lemmas. The fundamental notion of natural invariant is used to link the specification level and the interactive proof construction process.

Gossip, or epidemic, protocols have emerged as a highly scalable and resilient approach to implement several application level services such as reliable multicast, data aggregation, publish-subscribe, among others. All these protocols organize nodes in an unstructured random overlay network. In many cases, it is interesting to bias the random overlay in order to optimize some efficiency criteria, for instance, to reduce the stretch of the overlay routing. In this paper we propose X-BOT, a new protocol that allows to bias the topology of an unstructured gossip overlay network. X-BOT is completely decentralized and, unlike previous approaches, preserves several key properties of the original (non-biased) overlay (most notably, the node degree and consequently, the overlay connectivity). Experimental results show that X-BOT can generate more efficient overlays than previous approaches.