We present an algebra of discrete timed input/output automata that may execute in the context of different clock granularities – which we call timed machines; this algebra includes a refinement operator through which a machine can be extended with new states and transitions in order to accommodate a finer clock granularity as required to interoperate with other machines, and an extension of the traditional product of timed input–output automata to the situation in which the granularities of the two machines are not the same. Over this algebra, we then define an algebra of networks of timed machines that includes operations through which networks can be modified at run time, thus offering a model for systems of interconnected components that can dynamically bind to other systems and, therefore, cannot be adjusted at design time to ensure that they operate in a timed homogeneous setting. We investigate important properties of timed machines such as consistency – in the sense that a machine can be ensured to generate a non-empty language, and feasibility – in the sense that a machine can be ensured to generate a non-empty language no matter what inputs it receives, and propose techniques for checking if timed machines are consistent or are feasible. We generalise those properties to networks of timed machines, and investigate how consistency and feasibility of networks can be proved through properties that can be checked at design time without having to compute, at run time, the product of the machines that operate on those networks, which would not be practical.

Cloud computing has enabled many applications to dynamically accommodate their resources in response to variations in their workloads. Elastic scaling is implemented mostly via reactive techniques that are slow to respond and may induce service degradation during the adaptation period. To avoid those pitfalls, proactive techniques have emerged as an alternative. However, these are typically limited to settings with homogeneous resources. We introduce Augure, a prediction-based controller for live reconfiguration of cloud applications in heterogeneous settings. Augure relies on behavioral patterns of the workload obtained from historical data to feed a proactive adaptation engine. With the help of constraint solvers, Augure's engine finds the combination of (potentially mixed) resource types that best matches the expected evolution of the workload, and derives a plan that minimizes the price billed by the cloud provider and the impact of the reconfiguration on the quality of service provided to clients. We use simulations and a real system implementation to evaluate Augure and compare it to other controllers such as Reactive, Vadara, and Vadara+.

The problem of self-optimization and adaptation in the context of customizable systems is becoming increasingly important with the emergence of complex software systems and unpredictable execution environments. Here, a general framework for automatically deciding on when and how to adapt a system whenever it deviates from the desired behavior is presented. In this framework, the system's target behavior is described as a high-level policy that establishes goals for a set of performance indicators. The decision process is based on information provided independently for each component that describes the available adaptations, their impact on performance indicators, and any limitations or requirements. The technique consists of both offline and online phases. Offline, rules are generated specifying component adaptations that may help to achieve the established goals when a given change in the execution context occurs. Online, the corresponding rules are evaluated when a change occurs to choose which adaptations to perform. Experimental results using a prototype framework in the context of a web-based application demonstrate the effectiveness of this approach.

This paper addresses the self-management of in-memory distributed data grid platforms. A growing number of applications rely in these platforms to speed up access to large sets of data. However, they are complex to manage due to the diversity of configuration and load profiles. The proposed approach employs an adaptation policy expressed in terms of high-level goals to facilitate the task of the system manager, and address the complexity issues posed by the management of multiple configurations. The approach is validated experimentally using the open-source RedHat's Infinispan platform.

Assurances for Self-Adaptive Systems (ASAS) is a workshop that will bring together researchers to discuss software engineering aspects of self-adaptive systems, including methods, architectures, languages, algorithms, techniques, and tools that can be used to support assurances in self-adaptive system development. ASAS is intended as a complement to the efforts started a while ago at the successful FSE workshop series on Self-Healing Systems (WOSS), or the Software Engineering for Adaptive and Self-Managing Systems (SEAMS) symposium. However, in contrast with those events, ASAS is focused on the collection, storage, and analysis of evidence for the provision of assurances that a self-adaptive software system is able to behave functionally and non-functionally according to its specification.

Abstract We propose a formal operational semantics for service discovery and binding. This semantics is based on a graph-based representation of the configuration of global computers typed by business activities. Business activities execute distributed workflows that can trigger, at run time, the discovery, ranking and selection of services to which they bind, thus reconfiguring the workflows that they execute. Discovery, ranking and selection are based on compliance with required business and interaction protocols and optimisation of quality-of-service constraints. Binding and reconfiguration are captured as algebraic operations on configuration graphs. We also discuss the methodological implications that this model framework has on software engineering using a typical travel-booking scenario. To the best of our knowledge, our approach is the first to provide a clear separation between service computation and discovery/instantiation/binding, and to offer a formal framework that is independent of the SOA middleware components that act as service registries or brokers, and the protocols through which bindings and invocations are performed.

We discuss the suitability of service-oriented computing for the automotive domain. We present a formal high-level language in which complex automotive activities can be modelled in terms of components and services that can either be provided by the on-board system or procured from external providers (e.g. via the web) through a negotiation process that involves quality of service attributes and constraints. The ability to re-configure activities, in real-time, through service discovery and dynamic binding takes us one step further from current component-based development techniques: it enhances flexibility and adaptability to changes that occur in the environment in which the system operates (driver, automobile, and external circumstances) and, ultimately, leads to improved levels of satisfaction, safety and reliability.

The adoption of Domain-Specific Modeling Languages (DSMLs) for generating framework-based applications has proved to be an effective way of enforcing the correct use of frameworks and improve the productivity of application developers. However, the development of the code generator of a DSML is typically a laborious task with difficulties in what concerns complexity, understandability, and maintainability. In this paper, we address this problem with a new approach for developing DSMLs for frameworks that allows to eliminate the need of implementing code generators. The approach relies on the extension of frameworks with an additional layer based on aspect-oriented programming that encodes a DSML. By means of a generic language workbench, framework-based applications can be generated from application models described in that DSML. The proposed language workbench was implemented in a prototype tool and a case study on the Eclipse Rich Client Platform was performed.

We propose a mathematical semantics for event-based architectures that serves two main purposes: to characterise the modularisation properties that result from the algebraic structures induced on systems by this discipline of coordination; and to further validate and extend the categorical approach to architectural modelling that we have been building around the language CommUnity with the ‘implicit invocation’, also known as ‘publish/subscribe’ architectural style. We then use this formalisation to bring together synchronous and asynchronous interactions within the same modelling approach. We see this effort as a first step towards a form of engineering of architectural styles. Our approach adopts transition systems extended with events as a mathematical model of implicit invocation, and a family of logics that support abstract levels of modelling.

Community is a formal approach to software architecture. Its main characteristics are: a precise, yet intuitive mathematical semantics based on categorical diagrams; a clear separation between computation, coordination, and distribution (including mobility); and a simple state-based language, inspired by Unity, to describe behaviour. This paper discusses the applicability of this approach to location-aware systems through the modelling of the GSM handover protocol, namely the way communication with a moving cellular phone passes from one station to another. The case study was developed with the Community Workbench, a tool that animates distributed and mobile architectural models.

Abstract. The traditional notion of superposition has been used for supporting two distinct aspects of parallel program design: composition and refinement. This is because, when trace-based semantics of concurrency are considered, which is typical of most formal methods, these two relationships are modelled as inclusion between sets of behaviours. However, when forms of non-deterministic behaviour have to be considered, which is the case for component and service-based development, these two aspects do not coincide. In this paper, we show how the two roles of superposition can be separated and supported at the language and semantic levels. For this purpose, we use a categorical formalisation of program design in the language CommUnity that we are also using for addressing architectural concerns, another area in which the distinction between composition and refinement is particularly important.

We develop a notion of higher-order connector towards supporting the systematic construction of architectural connectors for software design. A higher-order connector takes connectors as parameters and allows for services such as security protocols and fault-tolerance mechanisms to be superposed over the interactions that are handled by the connectors passed as actual arguments. The notion is first illustrated over CommUnity, a parallel program design language that we have been using for formalizing aspects of architectural design. A formal, algebraic semantics is then presented which is independent of any Architectural Description Language. Finally, we discuss how our results can impact software design methods and tools.

In this paper, we address the integration of a distribution dimension in an architectural approach to system development and evolution based on the separation between coordination and computation. This third dimension allows us to separate key concerns raised by mobility, thus contributing to our ability to handle the complexity that is inherent to systems required to operate in "Internet time and space".

For several different reasons, such as changes in the business or technological environment, the configuration of a system may need to evolve during execution. Support for such evolution can be conceived in terms of a language for specifying the dynamic reconfiguration of systems. In this paper, continuing our work on the development of a formal platform for architectural design, we present a high-level language to describe architectures and for operating changes over a configuration (i.e., an architecture instance), such as adding, removing or substituting components or interconnectons. The language follows an imperative style and builds on a semantic domain established in previous work. Therein, we model architectures through categorical diagrams and dynamic reconfiguration through algebraic graph rewriting.