Abstract
In Computer Science stepwise refinement of algebraic specifications is a well-known formal methodology for rigorous program development. This paper illustrates how techniques from Algebraic Logic, in particular that of interpretation, understood as a multifunction that preserves and reflects logical consequence, capture a number of relevant transformations in the context of software design, reuse, and adaptation, difficult to deal with in classical approaches. Examples include data encapsulation and the decomposition of operations into atomic transactions. But if interpretations open such a new research avenue in program refinement, (conceptual) tools are needed to reason about them. In this line, the paper's main contribution is a study of the correspondence between logical interpretations and morphisms of a particular kind of coalgebras. This opens way to the use of coalgebraic constructions, such as simulation and bisimulation, in the study of interpretations between (abstract) logics.

Abstract
The original purpose of component-based development was to provide techniques to master complex software, through composition, reuse and parametrisation. However, such systems are rapidly moving towards a level in which software becomes prevalently intertwined with (continuous) physical processes. A possible way to accommodate the latter in component calculi relies on a suitable encoding of continuous behaviour as (yet another) computational effect. This paper introduces such an encoding through a monad which, in the compositional development of hybrid systems, may play a role similar to the one played by 1+, powerset, and distribution monads in the characterisation of partial, nondeterministic and probabilistic components, respectively. This monad and its Kleisli category provide a universe in which the effects of continuity over (different forms of) composition can be suitably studied.

Abstract
Software Product Lines (SPLs) are families of systems that share a high number of common assets while differing in others. In component-based systems, components themselves can be SPLs, i.e., each component can be seen as a family of variations, with different interfaces and functionalities, typically parameterized by a set of features and a feature model that specifies the valid combinations of features. This paper explores how to safely replace such families of components with more refined ones. We propose a notion of refinement for Interface Featured Timed Automata (IFTA), a formalism to model families of timed automata with support for multi-action transitions. We separate the notion of IFTA refinement into behavioral and variability refinement, i.e., the refinement of the underlying timed automata and feature model. Furthermore, we define behavioral refinement for the semantic level, i.e., transition systems, as an alternating simulation between systems, and lift this definition to IFTA refinement. We illustrate this notion with examples throughout the text and show that refinement is a pre-order and compositional.

Abstract
Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. It also captures the construction of first-order encodings of such hybridised institutions into theories in first-order logic. The method was originally developed to build suitable logics for the specification of reconfigurable software systems on top of whatever logic is used to describe local requirements of each system’s configuration. Hybridisation has, however, a broader scope, providing a fresh example of yet another development in combining and reusing logics driven by a problem from Computer Science. This paper offers an overview of this method, proposes some new extensions, namely the introduction of full quantification leading to the specification of dynamic modalities, and exemplifies its potential through a didactical application. It is discussed how hybridisation can be successfully used in a formal specification course in which students progress from equational to hybrid specifications in a uniform setting, integrating paradigms, combining data and behaviour, and dealing appropriately with systems evolution and reconfiguration. © Springer International Publishing Switzerland 2016.

Abstract
Software reconfigurability became increasingly relevant to the architectural process due to the crescent dependency of modern societies on reliable and adaptable systems. Such systems are supposed to adapt themselves to surrounding environmental changes with minimal service disruption, if any. This paper introduces an engine that statically applies reconfigurations to (formal) models of software architectures. Reconfigurations are specified using a domain specific language-ReCooPLa-which targets the manipulation of software coordination structures, typically used in service-oriented architectures (soa). The engine is responsible for the compilation of ReCooPLa instances and their application to the relevant coordination structures. The resulting configurations are amenable to formal analysis of qualitative and quantitative (probabilistic) properties.

Abstract
ARCHERY is an architectural description language for modelling and reasoning about distributed, heterogeneous and dynamically reconfigurable systems. This paper proposes a structural semantics for ARCHERY, and a method for deriving labelled transition systems (LTS) in which states and transitions represent configurations and reconfiguration operations, respectively. Architectures are modelled by bigraphs and their dynamics by parametric reaction rules. The resulting LTSs can be regarded as Kripke frames, appropriate for verifying reconfiguration constraints over architectural patterns expressed in a modal logic. The derivation method proposed here applies the approach in [1] twice, and combines the results of each application to obtain a label representing a reconfiguration operation and its actual parameters. Labels obtained in this way are minimal and yield LTSs in which bisimulation is a congruence.