Abstract The problem of managing multi‐service applications on top of Cloud‐Edge networks in a quality of service (QoS)‐aware manner has been thoroughly studied in recent years from a decision‐making perspective. However, only a few studies addressed the problem of actively enforcing such decisions while orchestrating multi‐service applications and considering infrastructure and application variations. In this article, we propose a next‐gen orchestrator prototype based on Docker to achieve the continuous and QoS‐compliant management of multiservice applications on top of geographically distributed Cloud‐Edge resources, in continuity with CI/CD pipelines and infrastructure monitoring tools. Finally, we assess our proposal over a geographically distributed testbed across Italy.

Urban Digital Twins (UDT) represent a powerful tool to effectively make cities smart. Generally, UDTs are linked with other Digital Twins to build ecosystems where the citizen is at the heart of the ecosystem. This is why citizens should be considered first-class entities in the UDTs. At the same time, citizens’ privacy cannot be compromised. In this paper, we propose to integrate citizens’ digital twin in UDTs through their digital avatars (DAs). DAs allow exploiting citizens’ information, behavioral habits and personal preferences, while allowing them to have full control of their own data. We present our architecture that makes use of the Cloud-to-Thing Continuum to optimize available processing resources. We focus on a case study of the public transport service of the city of Malaga (Spain) and describe how we are approaching its implementation. Finally, we validate such UDT implementation through tests that evaluate its accuracy and the factors affecting its performance.

Abstract The problem of service composition is the process of assigning resources to services from a pool of available ones in the shortest possible time so that the overall quality of service is maximized. This article provides solutions for the composition problem that takes into account its scalability, services' locations, and users' restrictions, which are key for the management of applications using state‐of‐the‐art technologies. The provided solutions use different techniques, including genetic algorithms and heuristics. We provide an extensive experimental evaluation, which shows the pros and cons of each of them, and allows us to characterize the preferred option for each specific problem. Since no solution dominates the others, we propose a decision tree, based on our results, to select the best composition algorithm in each situation.

Abstract An adaptive system can modify its settings at runtime as a response to changes in its operational environment. To analyse this kind of systems at design time is a difficult task since it requires considering the system together with the adaptation operations, and taking into account how such adaptations act on the system. In order to use simulation‐based techniques for the analysis of such systems, we not only need precise executable models of the systems to be analyzed, but also to capture the semantics of their adaptation mechanisms. Given the wide range and flexibility of adaptation operations, we need ways to allow the definition of new operations. We present a flexible approach for the definition and simulation‐based analysis in design‐time of adaptive component‐based systems. Our approach combines an extension of the Palladio component model in e‐Motions, a model of the adaptation mechanisms, and elastic requirements specification using the SYBL language. From the model of the system, its adaptation mechanisms, and its requirements, an executable Maude specification is generated for simulation. The application of the approach is illustrated on a use case that comprises some components and adaptations rules. The example is then analyzed using simulations. It is also shown that it is indeed possible to define additional metrics, specify adaptation requirements and rules which conduct simulations of the models in a more flexible way, and that the results of the simulation performed from these definitions can be used to carry on a valuable predictive performance analysis.

The fault handling and recovery from runtime failures of cloud applications should be done by taking into account the inter-dependencies occurring among their components, and by dealing with the diverse and heterogeneous cloud offerings used to host them. The latter is even harder in trans-cloud scenarios, i.e., when application components are possibly deployed on different platforms and at different service levels (IaaS or PaaS). In this paper, we propose a methodology to support the automated management and recovery of (un) foreseen failures in a trans-cloud application, which takes into account all interdependencies occurring among its components. We then present a prototype implementation of our proposal, consisting of an orchestrator that exploits a management framework for trans-cloud application deployments, together with management protocols for the automated planning of the fault-aware administration of applications.

The number of devices connected to the internet is constantly increasing. This large amount of devices can be used to improve people's interaction with their environment. However, this also implies an increase in the complexity when interacting with so many heterogeneous devices. Automating this process is key to keep up with this growth. This is the purpose of the People as a Service model (PeaaS), which works towards developing virtual profiles for every user in their own mobile devices under their full control. These profiles allow to establish preferences and predefined parameters, which are then used by the devices they connect to. By integrating both the information in the users' virtual profiles and the information given by the devices they connect to, we can create a context in which to make smart decisions and apply them to the devices, all of this in a decentralised way. This allows for a programmatically configuration of the devices without the need of the user's intervention. In order to put the proposal in action, we have developed a treasure hunting game as a proof of concept to bring to the spotlight the utility of an environment with programmatically adapted devices.

The diversity in the way different cloud providers offer their services, give their SLAs, present their QoS, support different technologies, etc., complicates the portability and interoperability of cloud applications, and favors vendor lockin. Standards like TOSCA, and tools supporting them, have come to help in the provider-independent description of cloud applications. After the variety of proposed cross-cloud application management tools, we propose going one step further in the unification of cloud services with a deployment tool in which IaaS and PaaS services are integrated into a unified interface. We provide support for applications whose components are to be deployed on different providers, indistinctly using IaaS and PaaS services. The TOSCA standard is used to define a portable model describing the topology of the cloud applications and the required resources in an agnostic, and providers- and resources-independent way. We include in this paper some highlights on our implementation on Apache Brooklyn and present a non-trivial example that illustrates our approach.

Cloud Computing providers offer diverse services and capabilities, which can be used by end-users to compose heterogeneous contexts of multiple cloud platforms to deploy their applications, in accordance with the best offered capabilities. However, this is an ideal scenario, since cloud platforms are being conducted in an isolated way by presenting interoperability and portability restrictions. Each provider defines its own API, non-functional requirements, QoS, add-ons, etc., and developers are often locked-in a concrete cloud environment, hampering the integration of heterogeneous provider services to achieve cross-deployment. This work presents an approach to deploy cross-cloud applications by using standardisation efforts of design, management and deployment of cloud applications. Specifically, using mechanisms specified by the TOSCA and CAMP standards, we propose a methodology to describe the topology and distribution of modules of a cloud application and to deploy the inter-connected modules over heterogeneous clouds. We present our prototype TOMAT, which supports the automatic distribution of cloud applications over multiple providers.

The adaptive management of complex applications deployed across multiple heterogeneous PaaS platforms is one of the problems that have emerged with the cloud revolution. The ongoing EU research project SeaClouds aims at providing seamless adaptive multi-cloud management of complex applications by supporting the distribution, monitoring and migration of application modules over multiple heterogeneous PaaS platforms. In this paper we present context, motivations and objectives of SeaClouds, its relation with other cloud initiatives, and its initial architecture.

We describe a formal methodology for the automatic synthesis of a secure orchestrator for a set of BPMN processes. The synthesized orchestrator is able to guarantee that all the processes that are started reach their end, and the resulting orchestrator process is secure, that is, it does not allow discloure of certain secret messages. In this work we present an implementation of a forth and back translation from BPMN to crypto-CCS, in such a way to exploit the PaMoChSA tool for synthesizing orchestrators. Furthermore, we study the problem of ranking orchestrators based on quantitative valuations of a process, and on the temporal evolution of such valuations and their security, as a function of the knowledge of the attacker.

Cloud computing promises easy access, low entry cost and elasticity. However, elastic service provisioning \nis usually delivered via service replication, which must be supervised manually, hand-picking the services \nto replicate and ensuring their proper load balance. Automated service provisioning, i.e., the function of \nautomatically scaling the services to cope up with their runtime demand, is a research challenge in cloud \ncomputing. In this work, we include such scalability analysis early in its development cycle, right at the design \nstage. We propose a model-driven approach where various QoS parameters can be simulated and analyzed \nusing the e-Motions tool. Additionally, the model is automatically transformed to fit the given throughput \nrequirements by replicating the services which cause the bottleneck. In order to evaluate the proposal, we \npresent some initial experimental results run over the e-Motions tool.

Adaptation is of utmost importance in systems developed by assembling reusable software services accessed through their public interfaces. This process aims at solving, as automatically as possible, mismatch cases which may be given at the different interoperability levels among interfaces by synthesizing a mediating adaptor. In this paper, we present a toolbox that fully supports the adaptation process, including: (i) different methods to construct adaptation contracts involving several services; (ii) simulation and verification techniques which help to identify and correct erroneous behaviours or deadlocking executions; and (iii) techniques for the generation of centralized or distributed adaptor protocols based on the aforementioned contracts. Our toolbox relates our models with implementation platforms, starting with the automatic extraction of behavioural models from existing interface descriptions, until the final adaptor implementation is generated for the target platform.

This paper introduces a service-oriented model for the description of embedded Peer-to-Peer (EP2P) systems and formalizes the proposed model in Maude. The model is organized around the notions of groups of peers and services offered by these groups. We first summarize the main concepts of the model and then present αSMoL, an abstract language with a formal semantics that provides a solid ground to develop tools for the automated analysis and verification of EP2P specifications. We then describe a formalization of αSMoL in Maude, and introduce an example to illustrate both the expressive power of the model and the possibilities of Maude to support automated verification of properties of αSMoL programs.

Software systems grow each day in size and complexity. In an effort to manage increasing complexity and to maximize the reuse of code, the software engineering community has, in recent years, put considerable effort into the design and development of component-based software methodologies and tools. Inspired by the notion of connector (Allen and Garlan (1994) Formal connectors. Technical report CMU-CS-94-115, Carnegie Mellon University, PA, USA) in software architecture and the ‘Design by Contract’ metaphor proposed by Meyer ((2000) Object-Oriented Software Construction. Prentice Hall, USA), this paper presents a methodology for component composition, coordination and dynamic adaptation. Our proposal is based on connectors enriched with contracts, making software architecture more explicit at the implementation level. Those connectors will be components in our system. Therefore, we can use subtyping techniques for connectors development and we could offer a set of generic connectors implementing standard behavior patterns. In addition, the connectors will use semantic web techniques and a Prolog machine to solve functional adaptation problems, such us name or parameters mismatching of a service, at run-time.

Abstract. Semantics of description languages for complex systems are a central issue for implementing verification methods such as abstract model checking . This technique is employed to verify systems by inspecting only a small state space that represents its potential behaviors. This paper presents a generalized operational semantics of the modelling language promela that provides the theoretical basis to introduce this promising method in the model checker SPIN. The generalization consists of identifying language aspects affected by the abstraction. Using these aspects as parameters, it is possible to obtain and relate different interpretations of the language. The new semantics provides a framework to reason about how to construct the tool αspin as an extension of spin.

The usage of object-oriented methodologies in conjunction with formal description techniques has arisen as a promising way of dealing with the increasing complexity of embedded real-time systems. These methodologies are currently well supported by a set of tools that allow the specification, simulation and validation of the functional aspects of these systems. However, most of these methodologies do not take into account non-functional aspects such as hardware interaction and real-time constraints, which are especially important in the context of this kind of system. Based on our experiences in developing embedded real-time systems, we present a new methodology to design them. This methodology is based on a combination of ideas from different existing methodologies (UML, OCTOPUS, etc.) together with the integration of rate-monotonic analysis in the context of the SDL formal description technique development cycle. Additionally, in order to get this integration, a real-time execution model for SDL is presented to allow us to express hard real-time constraints. The methodology pays special attention to the transition from the object model to the task model, taking into account real-time and hardware integration issues. We also illustrate our proposal by applying it to the development of a multi-handset cordless telephone.

Constructor-Based Conditional Rewriting Logic is a general framework for integrating first-order functional and logic programming which gives an algebraic semantics for nondeterministic functional-logic programs. In the context of this formalism, we introduce a simple notion of program module as an open program which can be extended together with several mechanisms to combine them. These mechanisms are based on a reduced set of operations. However, the high expressiveness of these operations enable us to model typical constructs for program modularization like hiding, export/import, genericity/instantiation, and inheritance in a simple way. We also deal with the semantic aspects of the proposal by introducing an immediate consequence operator, and studying several alternative semantics for a program module, based on this operator, in the line of logic programming: the operator itself, its least fixpoint (the least model of the module), the set of its pre-fixpoints (term models of the module), and some other variations in order to find a compositional and fully abstract semantics w.r.t. the set of operations and a natural notion of observability.

Traditional IDLs were defined for describing the services that objects offer, but not those services they require from other objects, nor the relative order in which they expect their methods to be called. Some of the existing proposals try to add protocol information to object interfaces, but most of them fail to do so in a modular way. In this paper we propose an extension of the CORBA IDL that uses a sugared subset of the polyadic /spl pi/-calculus for describing object service protocols, based on the concept of roles. Roles allow the modular specification of the observable behavior of CORBA objects, reducing the complexity of the compatibility tests. Our main aim is the automated checking of protocol interoperability between CORBA objects in open component-based environments, using similar techniques to those used in software architecture description and analysis. In addition, our proposal permits the study of substitutability between CORBA objects, as well as the realization of dynamic compatibility tests during their runtime execution.

Traditional IDLs were defined for describing the services that objects offer, but not those services they require from other objects, nor the relative order in which they expect their methods to be called. In this paper we propose an extension of the Common Object Request Broker Architecture (CORBA) interface description language (IDL) that uses a sugared subset of the polyadic $\pi$-calculus for describing object service protocols, aimed at the automated checking of protocol interoperability between CORBA objects in open component-based environments. In addition, some advantages and disadvantages of our proposal are discussed, as well as some of the practical limitations encountered when trying to implement and use this sort of IDL extension in open systems.

The high complexity of distributed computer systems requires new methodologies and languages especially designed for the characteristics of these systems. Declarative languages have been proposed as a promising alternative because they provide a way of leaving aside system details. However, the behaviour of reactive systems cannot be described in pure relational or functional terms. We propose a declarative environment for distributed programming based on the concurrent logic language Parlog, which has the capability of expressing concurrence, communication and non-determinism in a very natural way. That is, the intrinsic parallel semantics of the concurrent logic languages make them appropriate for distributed programming. The proposed environment is particularly suitable for loosely coupled systems and it contains mechanisms for distributed process control, and both real-time and object-oriented design. Each of these characteristics is achieved by the integration, in the framework of the underlying concurrent logic language, of real-time and distributed processing control primitives and object-oriented constructions. From this viewpoint, an operational semantics is defined and some implementation issues are discussed.