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
In the last years, new technologies - referred as emerging information and communication technologies (EICTs), have appeared and are immersed in peoples' lives assisting them and facilitating their daily activities. Taking advantage of the diffusion and infusion of these technologies, governments are using EICTs to deliver better public services to citizens. However, to address citizens' demands and to provide customer oriented services governments face various types of challenges. The aim of this research work is to provide solutions to some of the challenges, in particular to the rapid development of electronic public services (EPS) and the service integration in the context of development of smart cities. Following the aim, we propose an approach, called Virtual Factory for Smart City Service Integration. The idea of the virtual factory is to provide a framework to automatically produce software based on a given set of specifications of a family of EPS taking advantage of similarities in the EPS business processes. The expected contributions of this research work is to produce a domain specific language (DSL) for service specification and supporting tools that based on the produced specifications, workflow techniques and ideas of software product lines (SPL) can automatically produce software applications for EPS that can be easily parameterized and completed. Copyright 2014 ACM.

Abstract
The development of smart mobility initiatives requires specialized and contextualized policies addressing the needs and interests of many stakeholders involved. Since the development of such policies is challenging, there is a need to learn from the experience of many cities around the world offering efficient and successfully adopted smart mobility services. However, in practice, the information provided about such initiatives is shallow and unstructured. To address this issue, we study the state of the art in mobility services, reviewing scientific publications and 42 smart mobility services delivered by nine smart cities around the world, and we propose a taxonomy for planning and designing smart mobility services. The taxonomy provides a common vocabulary to discuss and share information about such services. It comprises eight dimensions: type of services, maturity level, users, applied technologies, delivery channels, benefits, beneficiaries, and common functionality. The contribution of the proposed taxonomy is to serve as a tool for guiding policy makers by identifying a spectrum of mobility services that can be provided, to whom, what technologies can be used to deliver them, and what is the delivered public value so to justify their implementation. In addition, the taxonomy can also assist researchers in further developing the domain. By identifying common functionality, it could also help Information Technology (IT) teams in building and maintaining smart mobility services. Finally, we further discuss usage scenarios of the taxonomy by policy makers, IT staff and researchers.

Abstract
Causal Loop Diagrams (CLDs) are a modeling tool employed in Business Dynamics. Such a diagram consists of many tightly coupled loops to capture dynamic behavior of systems. Intuitive operational semantics, describing how changes are propagated among the loops, provide a basis for model animation or manual inspection. They are, however, not precise enough to enable automated property checking. This paper proposes and defines a net-based formal framework, showing true concurrency, so that automated analysis is made possible.

Abstract
VirtuosoNext (TM) is a distributed real-time operating system (RTOS) featuring a generic programming model dubbed Interacting Entities. This paper focuses on these interactions, implemented as so-called Hubs. Hubs act as synchronisation and communication mechanisms between the application tasks and implement the services provided by the kernel as a kind of Guarded Protected Action with a well defined semantics. While the kernel provides the most basic services, each carefully designed, tested and optimised, tasks are limited to this handful of basic hubs, leaving the development of more complex synchronization and communication mechanisms up to application specific implementations. In this work we investigate how to support a programming paradigm to compositionally build new services, using notions borrowed from the Reo coordination language, and relieving tasks from coordination aspects while delegating them to the hubs. We formalise the semantics of hubs using an automata model, identify the behaviour of existing hubs, and propose an approach to build new hubs by composing simpler ones. We also provide tools and methods to analyse and simplify hubs under our automata interpretation. In a first experiment several hub interactions are combined into a single more complex hub, which raises the level of abstraction and contributes to a higher productivity for the programmer. Finally, we investigate the impact on the performance by comparing different implementations on an embedded board.

Abstract
Reactive programming (RP) languages and Synchronous Coordination (SC) languages share the goal of orchestrating the execution of computational tasks, by imposing dependencies on their execution order and controlling how they share data. RP is often implemented as libraries for existing programming languages, lifting operations over values to operations over streams of values, and providing efficient solutions to manage how updates to such streams trigger reactions, i.e., the execution of dependent tasks. SC is often implemented as a standalone formalism to specify existing component-based architectures, used to analyse, verify, transform, or generate code. These two approaches target different audiences, and it is non-trivial to combine the programming style of RP with the expressive power of synchronous languages. This paper proposes a lightweight programming language to describe component-based Architectures for Reactive systems, dubbed ARx, which blends concepts from RP and SC, mainly inspired to the Reo coordination language and its composition operation, and with tailored constructs for reactive programs such as the ones found in ReScala. ARx is enriched with a type system and with algebraic data types, and has a reactive semantics inspired in RP. We provide typical examples from both the RP and SC literature, illustrate how these can be captured by the proposed language, and describe a web-based prototype tool to edit, parse, and type check programs, and to animate their semantics. © IFIP International Federation for Information Processing 2020.