Abstract
Stepwise refinement of algebraic specifications is a well known formal methodology for program development. However, traditional notions of refinement based on signature morphisms are often too rigid to capture a number of relevant transformations in the context,at of software design, reuse, and adaptation. This paper proposes a new approach to refinement in which signature morphisms are replaced by logical interpretations as a means to witness refinements. The approach is first presented in the context of equational logic, and later generalised to deductive systems of arbitrary dimension. This allows, for example, relining sentential into equational specifications and the latter into modal ones.

Abstract
This paper introduces an axiomatisation for equational hybrid logic based on previous axiomatizations and natural deduction systems for propositional and first-order hybrid logic. Its soundness and completeness is discussed. This work is part of a broader research project on the development a general proof calculus for hybrid logics.

Abstract
Software Product Lines (SPLs) enable the development of families of software systems by taking advantage of the commonalities and variabilities of the members of the family. Despite its many advantages, it is an unexplored area in the electronic government domain, an area with evident families of services, and with high demands to develop faster and better services to citizens and businesses while reducing costs. This paper discusses the need of formal methods to model SPLs for such domain. It presents a case study of a family of public licensing services modeled in UPPAAL and based on Featured Timed Automata, an extension of Timed Automata to model real-time SPLs. It analyzes the suitability of FTA to model distributed families of services, while provides hints on a possible enrichment of FTA to better support modularization and compositionality of services.

Abstract
Networking and collaboration, at different levels and through differentiated mechanisms, have become increasingly relevant and popular as an effective means for delivering public policy over the past two decades. The variety of forms of collaboration that emerge in educational scenarios makes it hard to reach general conclusions about the effectiveness of collaboration in general and of inter-institutional networks in particular. The university environment is particularly challenging in this respect as typically different agendas for collaboration and competition co-exist and are often promoted by very same entities. Although no ‘one-fits-all’ model exists for the establishment of a network of universities, the prime result of the research reported in this paper is that the concept of such a network is a most promising instrument for delivering specific services within the high education universe. In this context, the paper discusses the potential of these networks for the design of educational programmes for the GCIO (Government Chief Information Officer) function and proposes a set of guidelines to successfully establish such networks. © 2017, IFIP International Federation for Information Processing.

Abstract
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 reconfigurable systems, i.e., systems with reconfiguration mechanisms governing the dynamic evolution of their execution configurations in response to both external stimuli or internal performance measures. A formal representation of such systems is through transition structures whose states correspond to the different configurations they may adopt. Therefore, each node is endowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. This paper characterises equivalence and refinement for these sorts of models in a way which is independent of (or parametric on) whatever logic (propositional, equational, fuzzy, etc) is found appropriate to describe the local configurations. A Hennessy-Milner like theorem is proved for hybridised logics.

Abstract
Able to simultaneously encode discrete transitions and continuous behaviour, hybrid automata are the de facto framework for the formal specification and analysis of hybrid systems. The current paper revisits hybrid automata from a coalgebraic point of view. This allows to interpret them as state-based components, and provides a uniform theory to address variability in their definition, as well as the corresponding notions of behaviour, bisimulation, and observational semantics.