Modern software systems are often realized by coordinating multiple heterogeneous parts, each responsible for specific tasks. These parts must work together seamlessly to satisfy the overall system requirements. To verify such complex systems, we have developed a non-intrusive coordination frame-work capable of performing formal analysis of heterogeneous parts that exchange data and include real-time capabilities. The framework utilizes a linguistic extension-which is implemented as a central broker and a domain-specific language-for the integration of heterogeneous languages and coordination of parts. Moreover, abstract rule templates are reified as language adapters for non-intrusive communications with the broker. The framework is implemented using rewriting logic (Maude), and its applicability is demonstrated by verifying certain correctness properties of a heterogeneous road-rail crossing system.

P is a domain-specific language designed for specifying asynchronous, event-driven systems. Its computational model is based on actors, i.e., on communicating state machines. This paper presents a formal semantics of P using rewriting logic, extending the language's verification capabilities. Implemented in Maude, a rewriting logic language, this semantics enables automated analysis of P programs, including reachability analysis, LTL model checking, and statistical model checking. Through illustrative examples, this paper demonstrates how this formalization significantly enhances P 's verification capacities in practical scenarios.

NuITP is an inductive equational theorem prover that combines advanced symbolic techniques such as narrowing, equality predicates, variant unification, variant satisfiability, order-sorted congruence closure, ordered rewriting, and strategy-based rewriting (all applied modulo axioms) to verify equational programs with expressive features such as sorts and subsorts, conditional equations and rewriting modulo axioms in Maude and in other equational languages. The present paper introduces the tool, explains its most commonly used inference rules, and illustrates their use in proving the card trick benchmark.

Maude is a high-performance logical framework based on rewriting logic and supporting formal specification, verification and declarative programming of concurrent systems. Since most concurrent open systems are made up of actor-like objects that communicate with each other through message passing, Maude provides special features to support their specification, verification and programming. Since open systems are heterogeneous, involving widely different kinds of objects such as sensors, actuators, devices, databases, graphical user interfaces, and so on, Maude supports declarative message-passing interaction between Maude objects and a wide variety of heterogeneous external objects. In this paper we explain and illustrate a methodology where an open system can first be designed and verified in Maude and then implemented as a distributed system of heterogeneous objects in a way that seamlessly bridges the gap between its formal specification and verification and its distributed implementation.

Multilevel Modelling (MLM) approaches make it possible for designers and modellers to work with an unlimited number of abstraction levels to specify their domain-specific modelling languages (DSMLs). To fully exploit MLM techniques, we need powerful model composition operators. Indeed, the composition of DSMLs is becoming increasingly relevant to the modelling community either because some DSMLs may share commonalities that we want to make reusable, or because we want to facilitate interoperability between DSMLs. In this paper, we propose a composition mechanism for structure and behaviour of multilevel modelling hierarchies. Our approach facilitates the inclusion of additional features while keeping a clear separation of concerns that enhances modularity. We provide a formal semantics of the constructions based on category theory and graph transformations, and show their use in practice on a case study.

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.

Term rewriting is a simple, yet expressive model of computation, which finds direct applications in specification and programming languages (many of which embody rewrite rules, pattern matching, and abstract data types), but also indirect applications, e.g., to express the semantics of data types or concurrent processes, to specify program transformations, to perform computer-aided verification, etc. The Rewrite Engines Competition (REC) was created under the aegis of the Workshop on Rewriting Logic and its Applications (WRLA) to serve three main goals: (i) being a forum in which tool developers and potential users of term rewrite engines can share experience; (ii) bringing together the various language features and implementation techniques used for term rewriting; and (iii) comparing the available term rewriting languages and tools in their common features. The present article provides a retrospective overview of the four editions of the Rewrite Engines Competition (2006, 2008, 2010, and 2018) and traces their evolution over time.

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.

This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax cup E), the E,Ax-variants of a term t are understood as the set of all pairs consisting of a substitution sigma and the E,Ax-canonical form of t sigma. The equational theory (Ax cup E ) has the finite variant property if there is a finite set of most general variants. We have added support in Maude 2.6 for: (i) order-sorted unification modulo associativity, commutativity and identity, (ii) variant generation, (iii) order-sorted unification modulo finite variant theories, and (iv) narrowing-based symbolic reachability modulo finite variant theories. We also explain how these features have a number of interesting applications in areas such as unification theory, cryptographic protocol verification, business processes, and proofs of termination, confluence and coherence.

Domain specific languages (DSLs) play a cornerstone role in Model-Driven Software Development for representing models and metamodels. DSLs' abstract syntax are usually defined by a metamodel. In-place model transformations provide an intuitive way to complement metamod-els with behavioral specifications. In this paper we extend in-place rules with a quantitative model of time and with mechanisms that allow designers to state action properties, facilitating the design of real-time complex systems. This approach avoids making unnatural changes to the DSL metamodels to represent behavioral and time aspects. We present the graphical modeling tool we have built for visually specifying these timed specifications.

Distributed Software Engineering (DSE) concepts in Computer Science (or Engineering) Degrees are commonly introduced using a hands-on approach mainly consisting of teaching a particular distributed and component-based technology platform (such as Java Enterprise Edition or Microsoft .NET) and proposing the students to develop a small distributed software application with it. Though this approach provides the students with some relevant practical knowledge, we believe that it is not the most appropriate way of teaching all the concepts and particularities of DSE. Thus, in this paper we report on our experience of redesigning an initial DSE course following a model-based approach. By raising the level of abstraction we gained modularity, separation of concerns and technology independence, while making the course evolve according to the latest trends in software development methods.

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.

Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CafeOBJ, Maude, and equational subsets of ELAN and CASL. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as muterm, CiME, AProVE, TTT, Termptation, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned tools.