Abstract
This paper presents the encoding of the hybridisation method proposed in [MMDB11, DM13] into the Hets platform. © 2013 Springer-Verlag Berlin Heidelberg.

Abstract
As a complex artefact, software has to meet requirements formulated and verified at different levels of abstraction. A basic distinction is drawn between behavioural (dynamic) and data (static) aspects. From an educational point of view, although disguised under a number of different designations, both issues are usually present, but kept separated, in typical Computer Science undergraduate curricula. It is often argued that they tackle orthogonal problems through essentially different methods. This paper explores an alternative path 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.

Abstract
Lightweight formal methods, of which Alloy is a prime example, combine the rigour of mathematics without compromising simplicity of use and suitable tool support. In some cases, however, the verification of safety or mission critical software entails the need formore sophisticated technologies, typically based on theorem provers. This explains a number of attempts to connect Alloy to specific theorem provers documented in the literature. This chapter, however, takes a different perspective: instead of focusing on one more combination of Alloy with still another prover, it lays out the foundations to fully integrate this system in the Hets platform which supports a huge network of logics, logic translators and provers. This makes possible for Alloy specifications to “borrow” the power of several, non dedicated proof systems. The chapter extends the authors’ previous work on this subject by developing in full detail the semantical foundations for this integration, including a formalisation of Alloy as an institution, and introducing a new, more general translation of the latter to second-order logic.

Abstract
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.

Abstract
Boilerplates are simplified, normative English texts, intended to capture software requirements in a controlled way. This paper proposes a pallet of boilerplates as a requirements modelling language for reconfigurable systems, i.e., systems structured in different modes of execution among which they can dynamically commute. The language semantics is given as an hybrid logic, in an institutional setting. The mild use made of the theory of institutions, which, to a large extent, may be hidden from the working software engineer, not only provides a rigorous and generic semantics, but also paves the way to tool-supported validation.

Abstract
Hierarchical transition systems provide a popular mathematical structure to represent state-based software applications in which different layers of abstraction are represented by inter-related state machines. The decomposition of high level states into inner sub-states, and of their transitions into inner sub-transitions is common refinement procedure adopted in a number of specification formalisms. This paper introduces a hybrid modal logic for k-layered transition systems, its first-order standard translation, a notion of bisimulation, and a modal invariance result. Layered and hierarchical notions of refinement are also discussed in this setting.