This paper extends the authors' previous work on a formal approach to the specification of reconfigurable systems, introduced in [7], in which configurations are taken as local states in a suitable transition structure. The novelty is the explicit consideration that not only the realisation of a service may change from a configuration to another, but also the set of services provided and even their functionality, may themselves vary. In other words, interfaces may evolve, as well.

This poster presents a pilot project on non-conventional learning strategies based on students’ active participation in real-life FLOSS projects. The aim of the project is to validate the hypothesis that the peer-production model, which underlies most FLOSS projects, can enhance the learning-teaching process based on extensive and systematic collaborative practices.

The complexity of modern software systems entails the need for reconfiguration mechanisms gov-
erning the dynamic evolution of their execution configurations in response to both external stimulus
or internal performance measures. Formally, such systems may be represented by transition systems
whose nodes correspond to the different configurations they may assume. Therefore, each node is en-
dowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics
of the services provided in the corresponding configuration.
Hybrid logics, which add to the modal description of transition structures the ability to refer to
specific states, offer a generic framework to approach the specification and design of this sort of
systems. Therefore, the quest for suitable notions of equivalence and refinement between models of
hybrid logic specifications becomes fundamental to any design discipline adopting this perspective.
This paper contributes to this effort from a distinctive point of view: instead of focussing on a specific
hybrid logic, the paper introduces notions of bisimilarity and refinement for hybridised logics, i.e.
standard specification logics (e.g. propositional, equational, fuzzy, etc) to which modal and hybrid
features were added in a systematic way.

Software connectors encapsulate interaction patterns between services in complex, distributed service-oriented applications. Such patterns evolve over time, in response to faults, changes in the expected QoS levels, emergent requirements or the reassessment of contextual conditions. This paper builds up on a model for connector reconfiguration to introduce notions of reconfiguration equivalence and refinement allowing for reasoning about them. This paves the way towards a (still missing) calculus of connector reconfigurations.

Abstract In the domain of machines' design, one of the most important issues to solve is related with the controller's design, mainly, guaranteeing that the machine will behave as expected. In order to achieve a dependable controller, some steps can be considered, such as the formalization of its specification - before being translated to the program that will be inserted in the controller device - and the respective analysis and verification. Nowadays, some formal analysis techniques, such as formal verification, are used to achieve this purpose. The dependability of a controller, however, is impacted by its execution context. This paper proposes an approach for the formal verification of the specification of mechatronic system's controllers, which considers, on the formal verification tasks, the behavior of the plant and the behavior of the Human Machine Interface of the Mechatronic system. Some conclusions are extrapolated for other systems of the same kind.

This paper presents the first BFT selection model and algorithm that can be used to choose the most convenient protocol according to the BFT user (i.e., an enterprise) preferences. The selection algorithm applies some mathematical formulas to make the selection process easy and automatic. The algorithm operates in three modes: Static, Dynamic, and Heuristic. The Static mode addresses the cases where a single protocol is needed; the Dynamic mode assumes that the system conditions are quite fluctuating and thus requires runtime decisions, and the Heuristic mode uses additional heuristics to improve user choices. To the best of our knowledge, this is the first work that addresses selection in BFT.

Enabling anonymous communication over the Internet is crucial. The first protocols that have been devised for anonymous communication are subject to freeriding. Recent protocols have thus been proposed to deal with this issue. However, these protocols do not scale to large systems, and some of them further assume the existence of trusted servers. In this paper, we present RAC, the first anonymous communication protocol that tolerates freeriders and that scales to large systems. Scalability comes from the fact that the complexity in terms of the number of message exchanges is independent from the number of nodes in the system. Another important aspect of RAC is that it does not rely on any trusted third party. We theoretically prove, using game theory that our protocol is a Nash equilibrium, i.e, that freeriders have no interest in deviating from the protocol. Further, we experimentally evaluate RAC using simulations. Our evaluation shows that, whatever the size of the system (up to 100.000 nodes), the nodes participating in the system observe the same throughput.