Catálogo de publicaciones - libros

Constraint automata have been used as an operational model for component connectors that coordinate the cooperation and communication of the components by means of a network of channels. In this paper, we introduce a variant of constraint automata (called continuous-time constraint automata) that allows us to specify time-dependent stochastic assumptions about the channel connections or the component interfaces, such as the arrival rates of communication requests, the average delay of enabled I/O-operations at the channel ends or the stochastic duration of internal computations. This yields the basis for a performance analysis of channel-based coordination mechanisms. We focus on compositional reasoning and discuss several bisimulation relations on continuous-time constraint automata. For this, we adapt notions of strong and weak bisimulation that have been introduced for similar stochastic models and introduce a new notion of weak bisimulation which abstracts away from invisible non-stochastic computations as well as the internal stochastic evolution.

In this paper we investigate the relationship between two problems, related to distributed systems, that are of particular interest in the context of Service Oriented Computing: atomic commit and negotiation. We will show that there exists a rather strict interdependency between the two problems by discussing how negotiation could be expressed as an instance of the atomic commit problem, and vice versa. To this end we exploit the Contract Net Protocol, a well known negotiation protocol, that will be described by means of the asynchronous pi calculus (Pi-CNP). Besides modeling CNP we also formally describe some basic properties of the CNP protocol.

Process algebraic specifications can provide useful support for the architectural design of software systems due to the possibility of analyzing their properties. In addition to that, such specifications can be exploited to guide the generation of code. What is needed at this level is a general methodology that accompanies the translation process, which in particular should help understanding whether and when it is more appropriate to implement a software component as a thread or as a monitor. The objective of this paper is to develop a systematic approach to the synthesis of correctly coordinating monitors from arbitrary process algebraic specifications that satisfy some suitable constraints. The whole approach will be illustrated by means of the process algebraic specification of a cruise control system.

How to coordinate the processes in a complex component-based software system is a nontrivial issue. Many different coordination approaches exist, each with its own specific advantages and drawbacks. To support their mutual comparison, this paper proposes a formal methodology to automatically evaluate the performance of coordination approaches. This methodology comprises (1) creation of simulation models of coordination approaches, (2) execution of simulation experiments of these models applied to test examples, and (3) automated evaluation of the models against specified requirements. Moreover, in a specific case study, the methodology is used to evaluate some coordination approaches that originate from various disciplines.

In a previous work we have presented a formal framework devoted to show the relevance of choreography and orchestration in the design of service oriented applications. Even if useful to start a formal investigation of the relationship between choreography and orchestration, the proposed framework was not suitable to specify real case studies. In fact, it simply permitted to specify all possible computations abstracting away from the conditions driving the choice of the actual behaviour. In this paper we tackle this problem by introducing the notion of state variables. The addition of state requires a substantial modification of the entire framework because the same state variable, at the level of choreography, can be actually stored in distributed orchestrators that will need to synchronize in order to maintain consistent views. In order to faithfully investigate this problem we also need to modify the formal model at the orchestration level, moving from synchronous to asynchronous communication as the latter is the communication modality of the ordinary communication infrastructures.

Van der Aalst recently proposed a set of workflow patterns to characterize the kinds of control flow that appear frequently in workflow processes. These patterns are useful for evaluating the capabilities of workflow systems and models. In this paper we provide implementations of the workflow patterns in Orc, a new process calculus for orchestrating wide-area computations. A key feature of the Orc implementations is that they are expressed as definitions that can be reused as needed.

The coordination language Paradigm allows for a flexible and orthogonal modeling of interprocess relationships at the architectural level. It is shown how dynamic system adaptation can be captured in Paradigm by means of a special evolution component and associated evolution coordination scheme. The component, called McPal, drives the migration following a just-in-time strategy in its own view of the system, independent of other coordination relations. During migration, dynamic consistency between components remains assured, even for mixtures of old, intermediate and new behaviour. A restricted scheme of McPal that supports various forms of self-adaptation is presented. A simple but generic example of a scheduler and workers illustrates on-the-fly updating of coordination and run-time adaptation of scheduling policies using McPal.

Bigraphical Reactive Systems have been proposed as a meta model for global ubiquitous computing generalising process calculi for mobility such as the pi-calculus and the Mobile Ambients calculus as well as graphical models for concurrency such as Petri Nets. We investigate in this paper how Bigraphical Reactive Systems represented as Reactive XML can be used to provide a formal semantics as well as an extensible and mobile platform independent execution format for XML based business process and workflow description languages such as WS-BPEL and XPDL. We propose to extend the formalism with primitives for XPath evaluation and higher-order reaction rules to allow for a very direct and succinct semantics.

Enabling coordination among ubiquitous computing applications and resources requires programming abstractions and development tools tailored to this unique environment. This paper introduces a suite of coordination abstractions that enables expressive interaction between ubiquitous computing applications and dynamically available resources. In our model, applications express their coordination needs in terms of application sessions that are loosely defined by a set of interactions with remote resources. Our approach allows developers to delegate responsibility for the construction and maintenance of the communication links necessary to support the application’s sessions to an underlying middleware. In this paper, we formalize a suite of session definitions for coordination in general classes of ubiquitous computing applications. We also present a middleware based on this coordination model that directly supports the software development task. Finally, we demonstrate the simplicity and flexibility of our approach using a real-world application.

We tackle the problem of providing rigorous formal foundations to current software engineering technologies for web services. We focus on two of the most used XML-based languages for web services: WSDL and WS-BPEL . To this aim, first we select an expressive subset of WS-BPEL , with special concern for modeling the interactions among web service instances in a network context, and define its operational semantics. We call ws-calculus the resulting formalism. Then, we put forward a rigorous typing discipline that formalizes the relationship existing between ws-calculus terms and the associated WSDL documents and supports verification of their compliance. We prove that the type system and the operational semantics of ws-calculus are ‘sound’ and apply our approach to an example application involving three interacting web services.