Abstract
Component's QoS constraints cannot be ignored when composing them to build reliable loosely-coupled, distributed systems. Therefore they should be explicitly taken into account in any formal model for component-based development. Such is the purpose of this paper: to extend a calculus of component composition to deal, in an effective way, with QoS constraints. Particular emphasis is put on how the laws that govern composition can be derived, in a calculational, pointfree style, in this new model.

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
Refinement by interpretation replaces signature morphisms by logic interpretations as a means to translate specifications and witness refinements. The approach was recently introduced by the authors [M. A. Martins, A. Madeira, and L. S. Barbosa. Refinement via interpretation. In Proc. of 7th IEEE Int. Conf. on Software Engineering and Formal Methods, Hanoi, Vietnam, November 2009. IEEE Computer Society Press] in the context of equational specifications, in order to capture a number of relevant transformations in software design, reuse and adaptation. This paper goes a step forward and discusses the generalization of this idea to deductive systems of arbitrary dimension. This makes possible, for example, to refine sentential into equational specifications and the latter into modal ones. Moreover, the restriction to logics with finitary consequence relations is dropped which results in increased flexibility along the software development process.

Abstract
Traditional notions of refinement of algebraic specifications, based on signature morphisms, art often too rigid to capture a number of relevant transformations in the context of software design, reuse and adaptation. This paper proposes an alternative notion of specification refinement, building on recent work on logic interpretation. The concept is discussed, its theory partially developed, its use illustrated through a number of examples.

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.