Abstract
The correctness and performance of large scale service oriented systems depend on distributed middleware components performing various communication and coordination functions. It is, however, very difficult to experimentally assess such middleware components, as interesting behavior often arises exclusively in large scale settings, but such deployments are costly and time consuming. We address this challenge with Minha, a system that virtualizes multiple JVM instances within a single JVM while simulating key environment components, thus reproducing the concurrency, distribution, and performance characteristics of the actual system. The usefulness of Minha is demonstrated by applying it to the WS4D Java stack, a popular implementation of the Devices Profile for Web Services (DPWS) specification. © 2011 ACM.

Abstract
Many rely now on public cloud infrastructure-as-a-service for database servers, mainly, by pushing the limits of existing pooling and replication software to operate large shared-nothing virtual server clusters. Yet, it is unclear whether this is still the best architectural choice, namely, when cloud infrastructure provides seamless virtual shared storage and bills clients on actual disk usage. This paper addresses this challenge with Resilient Asynchronous Commit (RAsC), an improvement to a well-known shared-nothing design based on the assumption that a much larger number of servers is required for scale than for resilience. Then we compare this proposal to other database server architectures using an analytical model focused on peak throughput and conclude that it provides the best performance/cost trade-off while at the same time addressing a wide range of fault scenarios.

Abstract
Software connectors are external coordination devices which ensure the flow of data and enforce synchronization constraints within a component's network. The specification of software connectors through which context dependent behaviour is correctly propagated remains an open, non trivial issue in their semantics. This paper, building on previous work by the authors, revisits this problem and introduces a model in which context awareness is suitably handled.

Abstract
Modal logics are successfully used as specification logics for reactive systems. However, they are not expressive enough to refer to individual states and reason about the local behaviour of such systems. This limitation is overcome in hybrid logics which introduce special symbols for naming states in models. Actually, hybrid logics have recently regained interest, resulting in a number of new results and techniques as well as applications to software specification. In this context, the first contribution of this paper is an attempt to 'universalize' the hybridization idea. Following the lines of [15], where a method to modalize arbitrary institutions is presented, the paper introduces a method to hybridize logics at the same institution-independent level. The method extends arbitrary institutions with Kripke semantics (for multi-modalities with arbitrary arities) and hybrid features. This paves the ground for a general result: any encoding (expressed as comorphism) from an arbitrary institution to first order logic (FOL ) determines a comorphism from its hybridization to FOL. This second contribution opens the possibility of effective tool support to specification languages based upon logics with hybrid features. © 2011 Springer-Verlag.

Abstract
This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus by evolving through different operational modes. In each mode different functionalities are provided. Starting from a classical state-machine specification, the envisaged methodology interprets each state as a different mode of operation endowed with an algebraic specification of the corresponding functionality. Specifications are given in an expressive variant of hybrid logic which is, at a later stage, translated into first-order logic to bring into scene suitable tool support. The paper's main contribution is to provide rigorous foundations for the method, framing specification logics as institutions and the translation process as a comorphism between them.

Abstract
The paper discusses the role of interpretations, understood as multifunctions that preserve and reflect logical consequence, as refinement witnesses in the general setting of p -institutions. This leads to a smooth generalization of the "refinement by interpretation" approach, recently introduced by the authors in more specific contexts. As a second, yet related contribution a basis is provided to build up a refinement calculus of structured specifications in and across arbitrary f-institutions. © C.J. Rodrigues, M.A. Martins, A. Madeira & L.S. Barbosa This work is licensed under the Creative Commons Attribution License.