Publications

Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the scheduling (e.g., resource allocation, run- time environments) of stateless functions. Recent work proposed using domain-specific languages to express per-function policies, e.g., policies that enforce the allocation on nodes that enjoy lower latencies to databases and services used by the function. Here, we focus on affinity-aware scenarios, i.e., where, for performance and functional requirements, the allocation of a function depends on the presence/absence of other functions on nodes. We present aAPP, an extension of a declarative, platform-agnostic language that captures affinity-aware scheduling at the FaaS level. We implement an aAPP-based prototype on Apache OpenWhisk. Besides proving that a FaaS platform can capture affinity awareness using aAPP and improve performance in affinity-aware scenarios, we use our prototype to show that aAPP imposes no noticeable overhead in scenarios without affinity constraints.

We present a new garbage collection reference counting algorithm capable of collecting reference cycles—overcoming a known limitation of traditional reference counting. The algorithm’s key features include resilience to errors during tracing, support for object finalisation, no need for supplementary heap memory during collection, and a fast breadth-first tracing approach that avoids stack overflows. We implement the algorithm as a Rust library that is idiomatic and highly compatible with the Rust ecosystem and that leverages Rust’s type system and borrow checker to minimise unsafe code and prevent undefined behaviour. We report benchmarks that show that our proposal performs comparably to popular Rust alternatives and outperforms them when dealing with garbage cycles.

In education, the capability of generating human-like text of Large Language Models (LLMs) inspired work on how they can increase the efficiency of learning and teaching. We study the affordability of these models for educators and students by investigating how LLMs answer multiple-choice questions (MCQs) with respect to hardware constraints and refinement techniques. We explore this space by using generic pre-trained LLMs (the 7B, 13B, and 70B variants of LLaMA-2) to answer 162 undergraduate-level MCQs from a course on Programming Languages (PL)—the MCQ dataset is a contribution of this work, which we make publicly available. Specifically, we dissect how different factors, such as using readily-available material—(parts of) the course’s textbook—for fine-tuning and quantisation (to decrease resource usage) can change the accuracy of the responses. The main takeaway is that smaller textbook-based fine-tuned models outperform generic larger ones (whose pre-training requires conspicuous resources), making the usage of LLMs for answering MCQs resource- and material-wise affordable.

Serverless programming revolutionises the implementation of cloud architectures by allowing developers to deploy stateless functions without managing server infrastructure, enabling efficient scaling and resource usage. Serverless shifts to the cloud provider the burden of managing servers and scaling, enabling developers to focus solely on writing the code for the functionalities specific to a given architecture. In this paper, we introduce Fenrir, a programming framework designed to facilitate the transition from monolithic programming to serverless. Fenrir enables developers to write applications in a monolithic style. Using annotation, users specify which components of the monolith shall implement separate serverless functions. Given these annotations, Fenrir generates a deployable serverless codebase, facilitating quick development and testing cycles while ensuring the alignment of the execution semantics between monolithic and serverless code.

We develop a novel approach for run-time global adaptation of microservice applications, based on synthesis of architecture-level reconfigurations. More precisely, we devise an algorithm for proactive-reactive automatic scaling that reaches a target system’s Maximum Computational Load by performing optimal deployment orchestrations. We evaluate our approach by developing a platform for the modelling and simulation of microservice architectures, and we use such a platform to compare local/global and reactive/proactive scaling. Empirical benchmarks, obtained through our platform, show that that proactive global scaling consistently outperforms the reactive approach, but the best performances can be obtained by our original approach for mixing proactivity and reactivity. In particular, our approach surpasses the state-of-the-art when both performance and resource consumption are considered.

We present JoT, a testing framework for Microservice Architectures (MSAs) based on technology agnosticism, a core principle of microservices. The main advantage of JoT is that it reduces the amount of work for a) testing for MSAs whose services use different technology stacks, b) writing tests that involve multiple services, and c) reusing tests of the same MSA under different deployment configurations or after changing some of its components. In JoT, tests are orchestrators that can both consume or offer operations from/to the MSA under test. The language for writing JoT tests is Jolie, which provides constructs that support technology agnosticism and the definition of terse test behaviours.

Choreographies provide a clear way to specify the intended communication behaviour of concurrent and distributed systems. Previous theoretical work investigated the translation of choreographies into (models of) programs based on message passing. However, existing theories still present a gap between how they model communications — using channel names à la CCS or π-calculus — and implementations — which use lower-level mechanisms for message routing. We start bridging this gap with a new formal framework called Applied Choreographies. In Applied Choreographies, developers write choreographies in a familiar syntax (from previous work) and reason about their behaviour through simple, abstract name-based communication semantics. The framework offers state-of-the-art features of choreographic models, e.g., modular programming supported via choreographic types. To provide its correctness guarantee, Applied Choreographies comes with a compilation procedure that transforms a choreography into a low-level, implementation-adherent calculus of Service-Oriented Computing (SOC). To manage the complexity of the compilation, we divide its formalisation and proof into three stages, respectively dealing with: (a) the translation of name-based communications into their SOC equivalents, namely, using correlation mechanisms based on message data; (b) the projection of the given choreography into a composition of partial, single-participant choreographies (towards their translation into SOC processes); (c) the translation of partial choreographies and the distribution of global, choreography-level state into local SOC processes. We provide behavioural correspondence results for each stage. Thus, given a choreography specification, we guarantee to synthesise its faithful service-oriented implementation.

Software-defined networking and network function virtualization have brought unparalleled flexibility in defining and managing network architectures. With the widespread diffusion of cloud platforms, more resources are available to execute virtual network functions concurrently, but the current approach to defining networks in the cloud development is held back by the lack of tools to manage the composition of more complex flows than simple sequential invocations. In this paper, we advocate for the usage of choreographic programming for defining the multiparty workflows of a network. When applied to the composition of virtual network functions, this approach yields multiple advantages: a single program expresses the behavior of all components, in a way that is easier to understand and check; a compiler can produce the executable code for each component, guaranteeing correctness properties of their interactions such as deadlock freedom; and the bottleneck of a central orchestrator is removed. We describe the proposed approach and show its feasibility via a case study where different functions cooperatively solve a security monitoring task.

We present Jolie Checker Toolchain (JCT), a plugin-based toolchain for model-code consistency and compliance analysis aimed at helping developers ensure that evolving implementations of Jolie microservices remain aligned with their intended architectural design specified with domain- and model-driven engineering approaches like LEMMA and MDSL. One of JCT’s strengths lies in providing a uniform surface for plugin development, based on the analysis of abstract syntax trees, that leverages existing code generation tools, framing checks as correspondence relations between the expected and actual programs. We present two JCT plugins to respectively check the consistency of domain-driven design annotations on Jolie APIs and verify Jolie code conformity to a given LEMMA data model. We illustrate both plugins via a use case drawn from the Lakeside Mutual architecture.

Function-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent developments demonstrate the benefits of using domain-specific languages to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies thanks to proximity and connection pooling. In this paper, we consider APP, one of the languages proposed to specify Allocation Priority Policies in FaaS implemented on top of the popular OpenWhisk serverless platform. The aim of our operational semantics is twofold: on the one hand, it represents the underlying substrate necessary for the application of formal analysis techniques, on the other hand, it can drive consistent implementations of APP on top of the numerous serverless platforms recently proposed.

Function-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent developments demonstrate the benefits of using domain-specific languages to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies thanks to proximity and connection pooling. In this paper, we consider APP, one of the languages proposed to specify Allocation Priority Policies in FaaS implemented on top of the popular OpenWhisk serverless platform. The aim of our operational semantics is twofold: on the one hand, it represents the underlying substrate necessary for the application of formal analysis techniques, on the other hand, it can drive consistent implementations of APP on top of the numerous serverless platforms recently proposed.

Choreographic Programming (CP) is a language paradigm whereby software artefacts, called choreographies, specify the behaviour of communicating participants. Choreographic programming is famous for its correctness-by-construction approach to the development of concurrent, distributed systems. In this paper, we illustrate FaaSChal, a proposal for a CP language tailored for the case of serverless Function-as-a-Service (FaaS). In FaaS, developers define a distributed architecture as a collection of stateless functions, leaving to the serverless platform the management of deployment and scaling. We provide a first account of a CP language tailored for the FaaS case via examples that present some of its relevant features, including projection. In addition, we showcase a novel application of CP. We use the choreography as a source to extract information on the infrastructural relations among functions so that we can synthesise policies that strive to minimise their latency while guaranteeing the respect of user-defined constraints.

The Topology-aware Allocation Priority Policies (tAPP) language allows users of serverless platforms to orient the scheduling of their functions w.r.t. the topological properties of the available computation nodes. A tAPP-based platform can support multiple scheduling policies, which one would usually enforce via (brittle) ad-hoc multi-instance platform deployments.

Choreographies are coordination plans for concurrent and distributed systems, which define the roles of the involved participants and how they are supposed to work together. In the paradigm of choreographic programming, choreographies are programs that can be compiled into executable implementations. In this article, we present Choral, the first choreographic programming language based on mainstream abstractions. The key idea in Choral is a new notion of data type, which allows for expressing that data is distributed over different roles. We use this idea to reconstruct the paradigm of choreographic programming through object-oriented abstractions. Choreographies are classes, and instances of choreographies are objects with states and behaviours implemented collaboratively by roles. Choral comes with a compiler that, given a choreography, generates an implementation for each of its roles. These implementations are libraries in pure Java, whose types are under the control of the Choral programmer. Developers can then modularly compose these libraries in their programs, to participate correctly in choreographies. Choral is the first incarnation of choreographic programming offering such modularity, which finally connects more than a decade of research on the paradigm to practical software development. The integration of choreographic and object-oriented programming yields other powerful advantages, where the features of one paradigm benefit the other in ways that go beyond the sum of the parts. On the one hand, the high-level abstractions and static checks from the world of choreographies can be used to write concurrent and distributed object-oriented software more concisely and correctly. On the other hand, we obtain a much more expressive choreographic language from object-oriented abstractions than in previous work. This expressivity allows for writing more reusable and flexible choreographies. For example, object passing makes Choral the first higher-order choreographic programming language, whereby choreographies can be parameterised over other choreographies without any need for central coordination. We also extend method overloading to a new dimension: specialisation based on data location. Together with subtyping and generics, this allows Choral to elegantly support user-defined communication mechanisms and middleware.

Crypto-ransomware aims at extorting money from users by encrypting their files and asking them to pay for the decryption key. We present Ranflood; a configurable drop-in solution that contrasts ransomware attacks with a deluge of decoy files at specific locations (e.g., sensitive folders of the user, the attack site), deceiving the attacker into encrypting sacrificial files. Ranflood further slows down the attack by contending with the malware access to IO and computation resources of the targeted machine. The aim is to buy time for the defence team to take action (e.g., manually shutting down an unresponsive machine). We show how the extensibility and modularity of Ranflood’s software architecture (1) can accommodate a wide spectrum of flooding strategies, easing the process of improving its effectiveness also against future ransomware families and (2) strive to maximise the tool’s efficiency by exploiting the highest level of parallelism afforded by the attacked machine.

We discuss an integrated approach for the design, specification, automatic deployment and simulation of microservice-based applications based on the ABS language. In particular, the integration of architectural modeling inspired by TOSCA (component types/port dependencies/architectural invariants) into the ABS language (static and dynamic aspects of ABS, including component properties, e.g., speed, and their use in timed/probabilistic simulations) via dedicated annotations. This is realized by the integration of the ABS toolchain with a dedicated tool, called Timed SmartDepl. Such a tool, at ABS code compile time, solves (starting from the provided architectural specification) the optimal deployment problem and produces ABS deployment orchestrations to be used in the context of timed simulations. Moreover, the potentialities and the expressive power of this approach are confirmed by further integration with external tools, e.g.: the Zephyrus tool, used by Timed SmartDepl to solve the optimal deployment problem via constraint solving, and a machine learning-based predictive module, that generates in advance data to be used in a timed ABS simulation exploiting such predicted data (e.g., simulating the usage, during the day, of predicted data generated during the preceding night).

Function as a service (FaaS) is a serverless cloud execution model offering cost-efficiency, scalability, and simplified development by enabling developers to focus on code and delegate server management and application scaling to the serverless platform. Early FaaS implementations provided no control to users over function placement, but raising data locality-bound scenarios motivated new implementations with user-defined constraints over function allocations, e.g., to keep functions accessing a database close to the latter, with the aim of reducing latency, enhancing security, or complying with regulations. In this article, we show how, by leveraging the Allocation Priority Policies languageused for controlling function schedulingand state-of-the-art planning tools, it is possible to enforce security properties and data-locality constraints, thereby guiding the definition of fine-grained serverless scheduling policies.

State-of-the-art serverless platforms use hard-coded scheduling policies that hardly accommodate users in implementing functional or performance-related scheduling logic of their functions, e.g., preserving the execution of critical functions within some geographical boundaries or minimising data-access latencies. We addressed this problem by introducing {APP}: a declarative language for defining per-function scheduling policies which we also implemented as an extension of the open-source OpenWhisk serverless platform. Here, we present a gentle introduction to {APP} through an illustrative application developed over several incremental steps.

We formally define and implement a translation of domain and service models expressed in the LEMMA modelling ecosystem for microservice architectures to source code in the Jolie microservice programming language. Specifically, our work extends previous efforts on the generation of Jolie code to the inclusion of the LEMMA service modelling layer. We also contribute an implementation of our translation, given as an extension of the LEMMA2Jolie tool, which enables the practical application of our encoding. As a result, LEMMA2Jolie now supports a software development process whereby microservice architectures can first be designed by microservice developers in collaboration with domain experts in LEMMA, and then be automatically translated into Jolie APIs. Our tool can thus be used to enhance productivity and improve design adherence.

This textbook is a thorough, up-to-date introduction to the principles and techniques that guide the design and implementation of modern programming languages.

The goal of the book is to provide the basis for a critical understanding of most modern programming languages. Thus, rather than focusing on a specific language, the book identifies the most important principles shared by large classes of languages. The notion of ‘abstract machine’ is a unifying concept that helps to maintain an accurate and elementary treatment. The book introduces, analyses in depth, and compares the imperative, object-oriented, functional, logic, concurrent, constraint-based, and service-oriented programming paradigms. All material coming from the first English edition has been updated and extended, clarifying some tricky points, and discussing newer programming languages. This second edition contains new chapters dedicated to constraint, concurrent, and service-oriented programming.

Topics and features:

Requires familiarity with one programming language is a prerequisite Provides a chapter on history offering context for most of the constructs in use today

• Presents an elementary account of semantical approaches and of computability
• Introduces new examples in modern programming languages like Python or Scala
• Offers a chapter that opens a perspective on applications in artificial intelligence Conceived as a university textbook, this unique volume will also be suitable for IT specialists who want to deepen their knowledge of the mechanisms behind the languages they use. The choice of themes and the presentation style are largely influenced by the experience of teaching the content as part of a bachelor’s degree in computer science.

The serverless paradigm offers benefits such as time savings and cost efficiency by delegating resource allocation and scaling to the platform. However, as the number of functions and interactions grows, the complexity of reasoning about the implementation correctness increases. Traditional monolithic development provides a more linear and simpler programming experience, with established best practices and tools for various development phases. From this observation, we propose Fenrir, an open-source programming framework for programming serverless applications managed as a monolithic codebase. Developers write applications in a monolithic style and then annotate specific parts that should be deployed as separate serverless functions, along with their corresponding call events. The Fenrir compiler uses these annotations to generate a correct-by-construction deployable serverless codebase that adheres to the source program’s execution semantics. This approach enables quick development and testing cycles, ensuring that the serverless application behaves as intended. We outline the main features of the Fenrir framework, including its annotation constructors and compilation pipeline, and briefly illustrate how Fenrir works with examples.

Current proprietary and open-source serverless platforms follow opinionated, hardcoded scheduling policies to deploy the functions to be executed over the available workers. Such policies may decrease the performance and the security of the application due to locality issues (e.g., functions executed by workers far from the databases to be accessed). These limitations are partially overcome by the adoption of APP, a new platform-agnostic declarative language that allows serverless platforms to support multiple scheduling logics. Defining the ``right’’ scheduling policy in APP is far from being a trivial task since it often requires rounds of refinement involving knowledge of the underlying infrastructure, guesswork, and empirical testing. In this paper, we start investigating how information derived from static analysis could be incorporated into APP scheduling function policies to help users select the best-performing workers at function allocation. We substantiate our proposal by presenting a pipeline able to extract cost equations from functions’ code, synthesising cost expressions through the usage of off-the-shelf solvers, and extending APP allocation policies to consider this information.

Ransomware is one of the most infamous kinds of malware, particularly the “crypto” subclass, which encrypts users’ files, asking for some monetary ransom in exchange for the decryption key. Recently, crypto-ransomware grew into a scourge for enterprises and governmental institutions. The most recent and impactful cases include an oil company in the US, an international Danish shipping company, and many hospitals and health departments in Europe. Attacks result in production lockdowns, shipping delays, and even risks to human lives. To contrast ransomware attacks (crypto, in particular), we propose a family of solutions, called Data Flooding against Ransomware, tackling the main phases of detection, mitigation, and restoration, based on a mix of honeypots, resource contention, and moving target defence. These solutions hinge on detecting and contrasting the action of ransomware by flooding specific locations (e.g., the attack location, sensible folders, etc.) of the victim’s disk with files. Besides the abstract definition of this family of solutions, we present an open-source tool that implements the mitigation and restoration phases, called Ranflood. In particular, Ranflood supports three flooding strategies, apt for different attack scenarios. At its core, Ranflood buys time for the user to counteract the attack, e.g., to access an unresponsive, attacked server and shut it down manually. We benchmark the efficacy of Ranflood by performing a thorough evaluation over 6 crypto-ransomware (e.g., WannaCry, LockBit) for a total of 78 different attack scenarios, showing that Ranflood consistently lowers the amount of files lost to encryption.

We introduce LEMMA2Jolie, a tool for translating domain models of microservice architectures given in LEMMA into concrete APIs of microservices in the Jolie programming language. Our tool combines the state of the art for the design and implementation of microservices: developers can use Domain-Driven Design (DDD) for the construction of the domain models of a microservice architecture, and then automatically transition to a service-oriented programming language that provides native linguistic support for implementing the behaviour of each microservice.

We present JoT, a testing framework for Microservice Architectures (MSAs) based on technology agnosticism, a core principle of microservices. The main advantage of JoT is that it reduces the amount of work for a) testing for MSAs whose services use different technology stacks, b) writing tests that involve multiple services, and c) reusing tests of the same MSA under different deployment configurations or after changing some of its components (e.g., when, for performance, one reimplements a service with a different technology). In JoT, tests are orchestrators that can both consume or offer operations from/to the MSA under test. The language for writing JoT tests is Jolie, which provides constructs that support technology agnosticism and the definition of terse test behaviours. We present the methodology we envision for testing MSAs with JoT and we validate it by implementing non-trivial test scenarios taken from a reference MSA from the literature (Lakeside Mutual).

In this work, we focus on by-design global scaling, a technique that, given a functional specification of a microservice architecture, orchestrates the scaling of all its components, avoiding cascading slowdowns typical of uncoordinated, mainstream autoscaling. State-of-the-art by-design global scaling adopts a reactive approach to traffic fluctuations, undergoing inefficiencies due to the reaction overhead. Here, we tackle this problem by proposing a proactive version of by-design global scaling able to anticipate future scaling actions. We provide four contributions in this direction: i) a platform able to host both reactive and proactive global scaling; ii) a proactive implementation based on data analytics; iii) a hybrid solution that mixes reactive and proactive scaling; iv) use cases and empirical benchmarks, obtained through our platform, that compare reactive, proactive, and hybrid global scaling performance. From our comparison, proactive global scaling consistently outperforms reactive, while the hybrid solution is the best-performing one.

The adoption of edge and fog systems, along with the introduction of privacy-preserving regulations, compel the usage of tools for expressing complex data queries in an ephemeral way. That is, queried data should not persist. Database engines partially address this need, as they provide domain-specific languages for querying data. Unfortunately, using a database in an ephemeral setting has inessential issues related to throughput bottlenecks, scalability, dependency management, and security (e.g., query injection). Moreover, databases can impose specific data structures and data formats, which can hinder the development of microservice architectures that integrate heterogeneous systems and handle semi-structured data. In this article, we present Jolie/Tquery, the first query framework designed for ephemeral data handling in microservices. Jolie/Tquery joins the benefits of a technology-agnostic, microservice-oriented programming language, Jolie, and of one of the most widely-used query languages for semi-structured data in microservices, the MongoDB aggregation framework. To make Jolie/Tquery reliable for the users, we follow a cleanroom software engineering process. First, we define Tquery, a theory for querying semi-structured data compatible with Jolie and inspired by a consistent variant of the key operators of the MongoDB aggregation framework. Then, we describe how we implemented Jolie/Tquery following Tquery and how the Jolie type system naturally captures the syntax of Tquery and helps to preserve its invariants. To both illustrate Tquery and Jolie/Tquery, we present the use case of a medical algorithm and build our way to a microservice that implements it using Jolie/Tquery. Finally, we report microbenchmarks that validate the expectation that, in the ephemeral case, using Jolie/Tquery outperforms using an external database (MongoDB, specifically).

State-of-the-art serverless platforms use hard-coded scheduling policies that are unaware of the possible topological constraints of functions. Considering these constraints when scheduling functions leads to sensible performance improvements, e.g., minimising loading times or data-access latencies. This issue becomes more pressing when considered in the emerging multi-cloud and edge-cloud-continuum systems, where only specific nodes can access specialised, local resources. To address this problem, we present a declarative language for defining serverless scheduling policies to express constraints on topologies of schedulers and execution nodes. We implement our approach as an extension of the OpenWhisk platform.

We formally define and implement a translation from domain models in the LEMMA modelling framework to microservice APIs in the Jolie programming language. Our tool enables a software development process whereby microservice architectures can first be designed with the leading method of Domain-Driven Design, and then corresponding data types and service interfaces (APIs) in Jolie are automatically generated. Developers can extend and use these APIs as guides in order to produce compliant implementations. Our tool thus contributes to enhancing productivity and improving the design adherence of microservices.

Increased levels of digitalization in society expose companies to new security threats, requiring them to establish adequate security and privacy measures. Additionally, the presence of exogenous forces like new regulations, e.g., GDPR and the global COVID-19 pandemic, pose new challenges for companies that should preserve an adequate level of security while having to adapt to change. In this paper, we investigate such challenges through a two-phase study in companies located in Denmarka country characterized by a high level of digitalizationfocusing on software development and tech-related companies. Our results show a number of issues, most notably i) a misalignment between software developers and management when it comes to the implementation of security and privacy measures, ii) difficulties in adapting company practices in light of implementing GDPR compliance, and iii) different views on the need to adapt security measures to cope with the COVID-19 pandemic.

Microservices is an emerging paradigm for developing distributed systems. With their widespread adoption, more and more work investigated the relation between microservices and security. Alas, the literature on this subject does not form a well-defined corpus: it is spread over many venues and composed of contributions mainly addressing specific scenarios or needs. In this work, we conduct a systematic review of the field, gathering 290 relevant publicationsat the time of writing, the largest curated dataset on the topic. We analyse our dataset along two lines: (a) quantitatively, through publication metadata, which allows us to chart publication outlets, communities, approaches, and tackled issues; (b) qualitatively, through 20 research questions used to provide an aggregated overview of the literature and to spot gaps left open. We summarise our analyses in the conclusion in the form of a call for action to address the main open challenges.

DevOps advocates the usage of Virtualization Technologies (VT), such as Virtual Machines and Containers. However, it is complex to predict how the usage of a given VT will impact on the performance of an application. In this paper, we present a collection of reference benchmarks that developers can use to orient when looking for the best-performing VT w.r.t their application profile. To gather our benchmarks in a resource-wise comprehensive and comparable way, we introduce VTmark: a semi-automatic open-source suite that assembles off-the-shelf tools for benchmarking the different resources used by applications (CPU, RAM, etc.). After performing a survey of VTs in the market, we use VTmark to report the benchmarks of 6 of the most widely adopted and popular ones, namely Docker, KVM, Podman, VMWare Workstation, VirtualBox, and Xen. To validate the accuracy of our reference benchmarks, we show how they correlate with the profile performance of a production-grade application ported and deployed on the considered VTs. Beyond our immediate results, VTmark let us shed light on some contradicting findings in the related literature and, by releasing VTmark , we provide DevOps with an open-source, extendable tool to assess the (resource-wise) costs of VTs.

Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinningsrespectively process calculi and lambda calculusthe two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long. In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.

In microservices, Model-Driven Engineering (MDE) has emerged as a powerful methodology for architectural design. Independently, the community of programming languages has investigated new linguistic abstractions for effective microservice development. Here, we present the first preliminary study of how the two approaches can cross-pollinate, taking the LEMMA framework and the Jolie programming language as respective representatives. We establish a common ground for comparing the two technologies in terms of metamodels, discuss practical enhancements that can be derived from the comparison, and present some directions for future work that arise from our new viewpoint.

We develop a novel approach for run-time global adaptation of microservice applications, based on synthesis of architecture-level reconfiguration orchestrations. More precisely, we devise an algorithm for automatic reconfiguration that reaches a target system Maximum Computational Load by performing optimal deployment orchestrations. To conceive and simulate our approach, we introduce a novel integrated timed architectural modeling/execution language based on an extension of the actor-based object-oriented Abstract Behavioral Specification (ABS) language. In particular, we realize a timed extension of SmartDeployer, whose ABS code annotations make it possible to express architectural properties. Our Timed SmartDeployer tool fully integrates time features of ABS and architectural annotations by generating timed deployment orchestrations. We evaluate the applicability of our approach on a realistic microservice application taken from the literature: an Email Pipeline Processing System. We prove its effectiveness by simulating such an application and by comparing architecture-level reconfiguration with traditional local scaling techniques (which detect scaling needs and enact replications at the level of single microservices). Our comparison results show that our approach avoids cascading slowdowns and consequent increased message loss and latency, which affect traditional local scaling.

Serverless computing is a paradigm for programming cloud applications in terms of stateless functions, executed and scaled in proportion to inbound requests. Here, we revisit SKC, a calculus capturing the essential features of serverless programming. By exploring the design space of the language, we refined the integration between the fundamental features of the two calculi that inspire SKC: the lambda- and the pi-calculus. That investigation led us to a revised syntax and semantics, which support an increase in the expressiveness of the language. In particular, now function names are first-class citizens and can be passed around. To illustrate the new features, we present step-by-step examples and two non-trivial use cases from artificial intelligence, which model, respectively, a perceptron and an image tagging system into compositions of serverless functions. We also illustrate how SKC supports reasoning on serverless implementations, i.e., the underlying network of communicating, concurrent, and mobile processes which execute serverless functions in the cloud. To that aim, we show an encoding from SKC to the asynchronous pi-calculus and prove it correct in terms of an operational correspondence.

Following previous work on the automated deployment of component-based applications, we present a formal model specifically tailored for reasoning on the deployment of microservice architectures. The first result that we present is a formal proof of decidability of the problem of synthesizing optimal deployment plans for microservice architectures, a problem which was proved to be undecidable for generic component-based applications. Then, given that such proof translates the deployment problem into a constraint satisfaction problem, we present the implementation of a tool that, by exploiting state-of-the-art constraint solvers, can be used to actually synthesize optimal deployment plans. We evaluate the applicability of our tool on a realistic microservice architecture taken from the literature.

Serverless computing is a Cloud development paradigm where developers write and compose stateless functions, abstracting from their deployment and scaling. In this paper, we address the problem of function-execution scheduling, i.e., how to schedule the execution of Serverless functions to optimise their performance against some user-defined goals. We introduce a declarative language of Allocation Priority Policies (APP) to specify policies that inform the scheduling of function execution. We present a prototypical implementation of APP as an extension of Apache OpenWhisk and we validate it by i) implementing a use case combining IoT, Edge, and Cloud Computing and ii) by comparing its performance to an alternative implementation that uses vanilla OpenWhisk.

The Internet of Things (IoT) advocates for multi-layered platformsfrom edge devices to Cloud nodeswhere each layer adopts its own communication standards (media and data formats). While this freedom is optimal for in-layer communication, it puzzles cross-layer integration due to incompatibilities among standards. Also enforcing a unique communication stack within the same IoT platform is not a solution, as it leads to the current phenomenon of ``IoT islands’’, where disparate platforms hardly interact with each other. In this paper we tackle the problem of IoT cross-layer and cross-platform integration following a language-based approach. We build on the Jolie programming language, which provides uniform linguistic abstractions to exploit heterogeneous communication stacks, allowing the programmer to specify in a declarative way the desired stack, and to easily change it, even at runtime. Jolie currently supports the main technologies from Service-Oriented Computing, such as TCP/IP, Bluetooth, and RMI at transport level, and HTTP and SOAP at application level. We integrate in Jolie the two most adopted protocols for IoT communication, i.e., CoAP and MQTT. We report our experience on a case study on Cloud-based home automation, and we present high-level concepts valuable both for the general implementation of interoperable systems and for the development of other language-based solutions.

Platoon formation is a freight organization system where a group of vehicles follows a predefined trajectory maintaining a desired spatial pattern. Benefits of platooning include fuel savings, reduction of carbon dioxide emissions, and efficient allocation of road capacity. While traditionally platooning has been an exclusive option limited to specific geographical areas managed by a single operator, recent technological developments and EU initiatives are directed at the creation of an international, federated market for platooning, i.e., a consortium of platoon operators that collaborate and coordinate their users to constitute freights covering international routes. In this paper, we look at federated platooning from an insiders’ perspective. In our development, first we outline the basic elements of platooning and federation of platooning operators. Then, we provide a comprehensive analysis to identify the possible insiders (employees, users, operators, and federated members) and the threats they pose. Finally, we propose two layered, composable technical solutions to mitigate those threats: a) a decentralized overlay network that regulates the interactions among the stakeholders, useful to mitigate issues linked to data safety and trustworthiness and b) a dynamic federation platform, needed to monitor and interrupt deviant behaviours of federated members.

In Choreographic Programming, a choreography specifies in a single artefact the expected behaviour of all the participants in a distributed system. The choreography is used to synthesise correct-by- construction programs for each participant. In previous work, we defined Dynamic Choreographies to support the update of distributed systems at runtime. In this work, we extend Dynamic Choreographies to include new participants at runtime, capturing those use cases where the system might be updated to interact with new, unforeseen stakeholders. We formalise our extension, prove its correctness, and present an implementation in the AIOCJ choreographic framework.

Serverless computing, also known as Functions-as-a-Service, is a recent paradigm aimed at simplifying the programming of cloud applications. The idea is that developers design applications in terms of functions, which are then deployed on a cloud infrastructure. The infrastructure takes care of executing the functions whenever requested by remote clients, dealing automatically with distribution and scaling with respect to inbound traffic. While vendors already support a variety of programming languages for serverless computing (e.g. Go, Java, Javascript, Python), as far as we know there is no reference model yet to formally reason on this paradigm. In this paper, we propose the first core formal programming model for serverless computing, which combines ideas from both the lambda-calculus (for functions) and the pi-calculus (for communication). To illustrate our proposal, we model a real-world serverless system. Thanks to our model, we capture limitations of current vendors and formalise possible amendments.

Ephemeral data handling, whereby processed data do not persist, is an emerging requirement of connected IT systems, due to storage constraints (IoT) or regulatory demands (eHealth, GDPR). We present ongoing work on TQuery, a query language for ephemeral data handling in microservices.

Network Function Virtualization (NFV) and Software Defined Networking (SDN) are technologies that recently acquired a great momentum thanks to their promise of being a flexible and cost-effective solution for replacing hardware-based, vendor-dependent network middleboxes with software appliances running on general purpose hardware in the cloud. Delivering end-to-end networking services across multiple NFV/SDN network domains by implementing the so-called Service Function Chain (SFC) i.e., a sequence of Virtual Network Functions (VNF) that composes the service, is a challenging task. In this paper we address two crucial sub-problems of this task: i) the language to formalize the request of a given SFC to the network and ii) the solution of the SFC design problem, once the request is received. As for i) in our solution the request is built upon the intent-based approach, with a syntax that focuses on asking the user what'' she needs and nothow’’ it should be implemented, in a simple and high level language. Concerning ii) we define a formal model describing network architectures and VNF properties that is then used to solve the SFC design problem by means of Constraint Programming (CP), a programming paradigm which is often used in Artificial Intelligence applications. We argue that CP can be effectively used to address this kind of problems because it provides very expressive and flexible modelling languages which come with powerful solvers, thus providing efficient and scalable performance. We substantiate this claim by validating our tool on some typical and non trivial SFC design problems.

Mobility-as-a-Service (MaaS) applies the everything-as-a-service paradigm of Cloud Computing to transportation: a MaaS provider offers to its users the dynamic composition of solutions of different travel agencies into a single, consistent interface. Traditionally, transits and data on mobility belong to a scattered plethora of operators. Thus, we argue that the economic model of MaaS is that of federations of providers, each trading its resources to coordinate multi-modal solutions for mobility. Such flexibility comes with many security and privacy concerns, of which insider threat is one of the most prominent. In this paper, we revise and extend previous work where we classified the potential threats of individual operators and markets of federated MaaS providers, proposing appropriate countermeasures to mitigate the problems. In addition, we consider the emerging case of Cloud-of-Things (CoT) for mobility, i.e., networks of ubiquitous, pervasive devices that provide real-time data on objects and people. Automation and pervasiveness of CoT make an additional attack surface for insiders. In an effort to limit such phenomenon, we present an overlay networking architecture, based on gossip protocols, that lets users share information on mobility with each other. A peculiarity of the architecture is that it both constrains the quality and quantity of data obtainable by insiders, optimizing the routing of requests to involve only users that are able to answer them.

The Internet of Things (IoT) promotes the communication among heterogeneous entities, from small sensors to Cloud systems. However, this is realized using a wide range of communication media and data protocols, usually incompatible with each other. Thus, IoT systems tend to grow as homogeneous isolated platforms, which hardly interact. To achieve a higher degree of interoperability among disparate IoT platforms, we propose a language-based approach for communication technology integration. We build on the Jolie programming language, which allows programmers to easily make the same logic work over disparate communication stacks in a declarative, dynamic way. Jolie currently supports the main technologies from Service-Oriented Computing, such as TCP/IP, Bluetooth, and RMI at transport level, and HTTP and SOAP at application level. As technical result, we integrate in Jolie the two most adopted protocols for IoT communication, i.e., CoAP and MQTT. In this paper, we report our experience and we present high-level concepts valuable both for the general implementation of interoperable systems and for the development of other language-based solutions.

Over the years, organizations acquired disparate software systems, each answering one specific need. Currently, the desirable outcomes of integrating these systems (higher degrees of automation and better system consistency) are often outbalanced by the complexity of mitigating their discrepancies. These problems are magnified in the decentralized setting (e.g., cross-organizational cases) where the integration is usually dealt with ad-hoc ``glue’’ connectors, each integrating two or more systems. Since the overall logic of the integration is spread among many glue connectors, these solutions are difficult to program correctly (making them prone to misbehaviours and system blocks), maintain, and evolve. In response to these problems, we propose ChIP, an integration process advocating choreographic programs as intermediate artefacts to refine high-level global specifications (e.g., UML Sequence Diagrams), defined by the domain experts of each partner, into concrete, distributed implementations. In ChIP, once the stakeholders agree upon a choreographic integration design, they can automatically generate the respective local connectors, which are guaranteed to faithfully implement the described distributed logic. In the paper, we illustrate ChIP with a pilot from the EU EIT Digital project SMAll, aimed at integrating pre-existing systems from government, university, and transport industry.

Choreographic Programming is a paradigm for distributed programming, where high-level ``Alice and Bob’’ descriptions of communications (choreographies) are used to synthesise correct-by-construction programs. However, implementations of choreographic models use message routing technologies distant from their related theoretical models (e.g., CCS/pi channels). This drives implementers to mediate discrepancies with the theory through undocumented, unproven adaptations, weakening the reliability of their implementations. As a solution, we propose the framework of Applied Choreographies (AC). In AC, programmers write choreographies in a language that follows the standard syntax and semantics of previous works. Then, choreographies are compiled to a real-world execution model for Service-Oriented Computing (SOC). To manage the complexity of this task, our compilation happens in three steps, respectively dealing with: implementing name-based communications using the concrete mechanism found in SOC, projecting a choreography to a set of processes, and translating processes to a distributed implementation in terms of services.

Programming distributed applications free from communication deadlocks and race conditions is complex. Preserving these properties when applications are updated at runtime is even harder. We present a choreographic approach for programming updatable, distributed applications. We define a choreography language, called Dynamic Interaction-Oriented Choreography (DIOC), that allows the programmer to specify, from a global viewpoint, which parts of the application can be updated. At runtime, these parts may be replaced by new DIOC fragments from outside the application. DIOC programs are compiled, generating code for each participant in a process-level language called Dynamic Process-Oriented Choreographies (DPOC). We prove that DPOC distributed applications generated from DIOC specifications are deadlock free and race free and that these properties hold also after any runtime update. We instantiate the theoretical model above into a programming framework called Adaptable Interaction-Oriented Choreographies in Jolie (AIOCJ) that comprises an integrated development environment, a compiler from an extension of DIOCs to distributed Jolie programs, and a runtime environment to support their execution.

Multi-modal travelling is a common phenomenon. However, planning multi-modal journeys is still an unstructured and time-consuming experience for customers: they lose time assembling a comprehensive plan out of disparate data, spread over a multitude of information systems each corresponding to a different company responsible for one of the legs in the journey. Also transport operators are affected by the sparsity of the transportation market, as they might lose potential customers who could not find or know about their services. In this paper, we propose Mobility as a Service (MaaS) as a solution to such problems. Key element of MaaS is that MaaS operators can aggregate solutions of multiple providers to deliver dynamic, transparent multi-modal travels to their users, who experience transportation as managed directly by a single operator. However, given the volume and sparsity of the transportation market, we argue that MaaS operators cannot rely on one-to-one, custom contracts of usage with single mobility operators. Instead, we envision the creation of platforms that automatise the marketing of services for mobility among many mobility providers.

In this work, we detail the required features of a general software platform for such a MaaS market. In particular, we provide a precise definition of MaaS through the MaaS Stack a tiered view of the components needed by entities to join the MaaS market. Then, through the lens of the MaaS Stack, we elicit the features of an enabling software platform. Finally, to validate our approach, we present a compliant prototype, called SMAll, and discuss its main design choices, among which: i) how SMAll supports the creation of a federation-based MaaS market and ii) how microservices an emerging architectural style that fosters cohesiveness and minimality of components enhance flexibility and let the platform and the services of its members efficiently scale according to dynamic demands.

Mobility as a Service (MaaS) applies the everything-as- a-service paradigm of Cloud Computing to transportation: a MaaS provider offers to its users the dynamic composition of solutions of different travel agencies into a single, consistent interface. Traditionally, transits and data on mobility belong to a scattered plethora of operators. Thus, we argue that the economic model of MaaS is that of federations of providers, each trading its resources to coordinate multi-modal solutions for mobility. Such flexibility comes with many security and privacy concerns, of which insider threat is one of the most prominent. In this paper, we follow a tiered structure from individual operators to markets of federated MaaS providers to classify the potential threats of each tier and propose the appropriate countermeasures, in an effort to mitigate the problems.

The microservice architecture is a style inspired by service-oriented computing that has recently started gaining popularity. Before presenting the current state-of-the-art in the field, this chapter reviews the history of software architecture, the reasons that led to the diffusion of objects and services first, and microservices later. Finally, open problems and future challenges are introduced. This survey addresses mostly newcomers to the discipline and offers an academic viewpoint on the topic. In addition, practical aspects are investigated and solutions proposed.

This tutorial describes AIOCJ, which stands for Adaptive Interaction Oriented Choreographies in Jolie, a choreographic language for programming microservice-based applications which can be updated at runtime. The compilation of a single AIOCJ program generates the whole set of distributed microservices that compose the application. Adaptation is performed using adaptation rules. Abstractly, each rule replaces a pre-delimited part of the program with the new code contained in the rule itself. Concretely, at runtime, the application of a rule updates part of the microservices that compose the application so to match the behaviour specified by the updated program. Thanks to the properties of choreographies, the adaptive application is free from communication deadlocks and message races even after adaptation.

Choreographies are a relatively new tool for designing distributed systems from a global viewpoint. Choreographic specifications are also free from deadlocks and race conditions by design. Recent theoretical results defined proper Endpoint Projection (EPP) functions to compile choreographic specifications into their single components. Since EPPs are behavioural preserving, projected systems also enjoy freedom from deadlocks and races by construction.

Aim of this PhD is to formalise non-trivial features of distributed systems with choreographies and to translate our theoretical results into the practice of implemented systems. To this purpose, we provide two main contributions.

The first contribution tackles one of the most challenging features of distributed development: programming correct and consistent runtime updates of distributed systems. Our solution is a theoretical model of dynamic choreographies that provides a clear definition of which components and behaviours can be updated. We prove that compiled choreographic specifications are correct and consistent after any update. We also refine our theoretical model to provide a finer control over updates. On this refinement, we develop a framework for programming adaptable distributed systems.

The second contribution covers one of the main issues of implementing theoretical results on choreographies: formalising the compilation from choreographies to executable programs. There is a sensible departure between the present choreographic frameworks and their theoretical models because their theories abstract communications with synchronisation on names (a la CCS/pi-calculus) yet they compile to Jolie programs, an executable language that uses correlation a renown technology of Service-Oriented Computing for message routing. Our solution is a theory of Applied Choreographies (AC) that models correlation-based message passing. We pinpoint the key theoretical problems and formalise the principles that developers should follow to obtain correct implementations. Finally, we prove our approach by defining a correct compiler from AC to the calculus behind the Jolie language.

Mobility as a Service takes the concept of XaaS to transportation: a MaaS provider shall merge transport options from different mobility providers, seamlessly handling the whole experience of travelling, from providing information, to travel planning, and payments handling. To effectively support the creation of a market of MaaS providers, we envision the creation of ICT infrastructures based on microservices, a modern and renowned development model that fosters the creation of an ecosystem of reusable components. The flexibility of such platforms is their key advantage, yet it poses many security issues. In this paper, we look at these problems through the lens of our experience on one of such platforms, called SMAll. We classify the most relevant vulnerabilities related to data reliability, integrity, and authenticity, and we investigate directions for their mitigation.

Microservices is an emerging paradigm for the development of distributed systems that, originating from Service-Oriented Architecture, focuses on the small dimension, the loose coupling, and the dynamic topology of services. Microservices are particularly appropriate for the development of distributed systems in the Cloud. However, their dynamic nature calls for suitable techniques for their automatic deployment. In this paper we address this problem and we propose JRO (Jolie Redeployment Optimiser), a tool for the automatic and optimised deployment of microservices written in the Jolie language. The tool uses Zephyrus, a state of the art tool that automatically generates a fully detailed Service-Oriented Architecture configuration starting from a partial and abstract description of the target application.

Programming distributed applications free from communication deadlocks and races is complex. Preserving these properties when applications are updated at runtime is even harder. We present DIOC, a language for programming distributed applications that are free from deadlocks and races by construction. A DIOC program describes a whole distributed application as a unique entity (choreography). DIOC allows the programmer to specify which parts of the application can be updated. At runtime, these parts may be replaced by new DIOC fragments from outside the application. DIOC programs are compiled, generating code for each site, in a lower-level language called DPOC. We formalise both DIOC and DPOC semantics as labelled transition systems and prove the correctness of the compilation as a trace equivalence result. As corollaries, DPOC applications are free from communication deadlocks and races, even in presence of runtime updates.

We illustrate our approach to develop and verify distributed, adaptive software systems. The cornerstone of our framework is the use of choreography languages, which allow us to obtain correctness by construction. Workflow Patterns are also used as abstract tools to design real systems, while techniques based on abstract interpretation and on dynamic verification are integrated in our framework to reduce the complexity of verification.

We present AIOCJ, a framework for programming distributed adaptive applications. Applications are programmed using AIOC, a choreographic language suited for expressing patterns of interaction from a global point of view. AIOC allows the programmer to specify which parts of the application can be adapted. Adaptation takes place at runtime by means of rules, which can change during the execution to tackle possibly unforeseen adaptation needs. AIOCJ relies on a solid theory that ensures applications to be deadlock-free by construction also after adaptation. We describe the architecture of AIOCJ, the design of the AIOC language, and an empirical validation of the framework.

In Service-Oriented Architectures (SOA), services are composed by coordinating their communications into a flow of interactions. Coloured Petri nets (CPN) offer a formal yet easy tool for modelling interactions in SOAs, however mapping abstract SOAs into executable ones requires a non-trivial and time-costly analysis. Here, we propose a methodology that maps CPN-modelled SOAs into Jolie SOAs (our tar- get language), exploiting a collection of recurring control-flow patterns, called Workflow Patterns, as composable blocks of the translation. We validate our approach with a realistic use case. In addition, we pragmatically asses the expressiveness of Jolie wrt the considered WPs.

Application Programming Interfaces (APIs) are a standard feature of any application that exposes its functionalities to external invokers. APIs can be composed thus obtaining new programs with new functionalities. However API composition easily becomes a frustrating and time-costly task that hinders API reuse. The issue derives from technology-dependent features of API composition such as the need of extensive documentation, protocol integration, security issues, etc.. In this paper we introduce the perspective of the API-as-a-Service (APIaaS) layer as tool to ease the development and deployment of applications based on API composition, abstracting communication protocols and message formats. We elicit the desirable features of such a layer and provide a proof-of-concept prototype implemented using a service-oriented language.

The main contribution of this master thesis work is the description, verification, and demonstration of the realisability in the Jolie language of Control-Flow and Resources Workflow Patterns defined by the Workflow Patterns Initiative (WPI). The thesis is divided into four chapters.

The first chapter presents a general description of the programming paradigm behind the Jolie language, Service-Oriented Computing, and its main context of application, Business Process Automation (BPA). The presentation is mainly focussed on the principles of Service-Oriented Architectures (SOA) and ultimately describes the main methods concerning service composition orchestration and choreography. The last section of the chapter considers SOC in a strictly industrial perspective, highlighting its strategic features.

The second chapter focuses on the description of Jolie. This chapter is not intended as a comprehensive description of the features in the language but rather gives an overview of the theoretical concepts, data structures, operators, and constructs of Jolie, used to demonstrate the realisability of the considered Workflow Patterns.

The third chapter contains the actual realisation of the considered Workflow Patterns in Jolie. Each pattern is first reported and explained in terms of Coloured Petri Nets, realised as a Jolie program (or architecture of programs), reporting the rationale behind the realisation.

The fourth chapter summarises the results from this thesis work, showing a comparison between Jolie and other BPA languages, as reported by WPI. The chapter also contains a discussion on future work: the completion of this study with an analysis on the remaining patterns from the WPI and their impact on the evolution of the Jolie language.