Abstract
Featured Timed Automata (FTA) is a formalism that enables the verification of an entire Software Product Line (SPL), by capturing its behavior in a single model instead of product-by-product. However, it disregards compositional aspects inherent to SPL development. This paper introduces Interface FTA (IFTA), which extends FTA with variable interfaces that restrict the way automata can be composed, and with support for transitions with atomic multiple actions, simplifying the design. To support modular composition, a set of Reo connectors are modelled as IFTA. This separation of concerns increases reusability of functionality across products, and simplifies modelling, maintainability, and extension of SPLs. We show how IFTA can be easily translated into FTA and into networks of Timed Automata supported by UPPAAL. We illustrate this with a case study from the electronic government domain.

Abstract
Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete actions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in a not necessary bivalent truth space, namely graded Kleene algebra with tests (GKAT) and Heyting Kleene algebra with tests (HKAT). On these contexts, in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT [10], we discuss the encoding of a graded PHL in HKAT and of its while-free fragment in GKAT.

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
Burden reduction is a key issue in modern public administrations' and businesses' agendas. Compliance with mandatory regulations can have a direct impact on a country's economic performance, growth, and development. Research in this area, contributes to a better understanding of the implications and context of administrative burden, and increases the efficiency of the strategies adopted to reduce it. The goal of this study is to undertake a review of the current state of the art on Administrative Burden Reduction (ABR), in order to gain a deeper insight about the subject, identify current gaps, and better plan for future research. A total of 122 papers were identified as relevant, out of a pool of 742 papers retrieved from the current literature. The relevant papers were analyzed across four dimensions: methodology, type and focus, and targeted stakeholders. Three key gaps were identified and discussed in relation to: citizen orientated services and burden reduction; empirical research and post-initiative re-evaluation; and, the role of stakeholders, interest groups and end-users in driving ABR. Lastly a conceptual framework model and next steps are proposed.

Abstract
The orchestration of high performance computing (HPC) services to build scientific applications is based on complex workflows. A challenging task consists of improving the reliability of such workflows, avoiding faulty behaviors that can lead to bad consequences in practice. This paper introduces a certifier component for certifying scientific workflows in a certification framework proposed for HPC Shelf, a cloud-based platform for HPC in which different kinds of users can design, deploy and execute scientific applications. This component is able to inspect the workflow description of a parallel computing system of HPC Shelf and check its consistency with respect to a number of safety and liveness properties specified by application designers and component developers.