Skip to main content

2008 | Buch

Coordination Models and Languages

10th International Conference, COORDINATION 2008, Oslo, Norway, June 4-6, 2008. Proceedings

herausgegeben von: Doug Lea, Gianluigi Zavattaro

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

insite
SUCHEN

Über dieses Buch

Modern information systems rely increasingly on combining concurrent, d- tributed, real-time, recon?gurable and heterogeneous components. New models, architectures, languages, and veri?cation techniques are necessary to cope with thecomplexityinducedbythedemandsoftoday’ssoftwaredevelopment. COOR- DINATIONaimstoexplorethespectrumoflanguages,middleware,services,and algorithms that separate behavior from interaction, therefore increasing mo- larity, simplifying reasoning, and ultimately enhancing software development. This volume contains the proceedings of the 10th International Conference on Coordination Models and Languages, COORDINATION 2008, held in Oslo, Norway in June 2008, as part of the federated DisCoTec conference. COORDI- NATIONitselfispartofaserieswhoseproceedingshavebeenpublishedinLNCS volumes 1061, 1282, 1594, 1906, 2315, 2949, 3454, 4038, and 4467. From the 61 submissions received from around the world, the Program Committee selected 21 papers for presentation and publication in this volume on the basis of or- inality, quality, and relevance to the topics of the conference. Each submission received at least three reviews. As with previous editions, the paper submission and selection processes were managed entirely electronically. This was acc- plished using EasyChair, a free Web-based conference management system. In addition to the technical paper presentations, COORDINATION 2008 hosted an invited presentation by Matt Welsh from Harvard University. We are grateful to all the Program Committee members who devoted much e?ort and time to read and discuss the papers. Moreover, we acknowledge the help of additional external reviewers who evaluated submissions in their area of expertise. Finally,wewouldliketothanktheauthorsofallthesubmittedpapersandthe conferenceattendees, for keeping this researchcommunity lively and interactive, and ultimately ensuring the success of this conference series.

Inhaltsverzeichnis

Frontmatter
A Coordination Model for Service-Oriented Interactions
Abstract
We present a formal model for the coordination of interactions in service-oriented systems. This model provides a declarative semantics for the language SRML that is being developed under the FET-GC2 project SENSORIA for modelling and reasoning about complex services at the abstract business level. In SRML, interactions are conversational in the sense that they involve a number of correlated events that capture phenomena that are typical of SOC like committing to a pledge or revoking the effects of a deal. Events are exchanged across wires that connect the parties involved in the provision of the service.
João Abreu, José Luiz Fiadeiro
Implementing Session Centered Calculi
Abstract
Recently, specific attention has been devoted to the development of service oriented process calculi. Besides the foundational aspects, it is also interesting to have prototype implementations for them in order to assess usability and to minimize the gap between theory and practice. Typically, these implementations are done in Java taking advantage of its mechanisms supporting network applications. However, most of the recurrent features of service oriented applications are re-implemented from scratch. In this paper we show how to implement a service oriented calculus, CaSPiS (Calculus of Services with Pipelines and Sessions) using the Java framework IMC, where recurrent mechanisms for network applications are already provided. By using the session oriented and pattern matching communication mechanisms provided by IMC, it is relatively simple to implement in Java all CaSPiS abstractions and thus to easily write the implementation in Java of a CaSPiS process.
Lorenzo Bettini, Rocco De Nicola, Michele Loreti
Service Combinators for Farming Virtual Machines
Abstract
Management is one of the main expenses of running the server farms that implement enterprise services, and operator errors can be costly. Our goal is to develop type-safe programming mechanisms for combining and managing enterprise services, and we achieve this goal in the particular setting of farms of virtual machines. We assume each server is service-oriented, in the sense that the services it provides, and the external services it depends upon, are explicitly described in metadata. We describe the design, implementation, and formal semantics of a library of combinators whose types record and respect server metadata. We describe a series of programming examples run on our implementation, based on existing server code for a typical web application.
Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya
Timed Soft Concurrent Constraint Programs
Abstract
We propose a timed and soft extension of Concurrent Constraint Programming. The time extension is based on the hypothesis of bounded asynchrony: the computation takes a bounded period of time and is measured by a discrete global clock. Action prefixing is then considered as the syntactic marker which distinguishes a time instant from the next one. Supported by soft constraints instead of crisp ones, tell and ask agents are now equipped with a preference (or consistency) threshold which is used to determine their success or suspension. In the paper we provide a language to describe the agents behavior, together with its operational and denotational semantics, for which we also prove the compositionality and correctness properties. Agents negotiating Quality of Service can benefit from this new language, by coordinating among themselves and mediating their preferences.
Stefano Bistarelli, Maurizio Gabbrielli, Maria Chiara Meo, Francesco Santini
Multiparty Sessions in SOC
Abstract
Service oriented applications feature interactions among several participants over the network. Mechanisms such as correlation sets and two-party sessions have been proposed in the literature to separate messages sent to different instances of the same service. This paper presents a process calculus featuring dynamically evolving multiparty sessions to model interactions that spread over several participants. The calculus also provides primitives for service definition/invocation and for structured communication in order to highlight the interactions among the different concepts. Several examples from the SOC area show the suitability of our approach.
Roberto Bruni, Ivan Lanese, Hernán Melgratti, Emilio Tuosto
Formalizing Higher-Order Mobile Embedded Business Processes with Binding Bigraphs
Abstract
We propose and formalize HomeBPEL, a higher-order WSBPEL-like business process execution language where processes are first-class values that can be stored in variables, passed as messages, and activated as embedded sub-instances. A sub-instance is similar to a WSBPEL scope, except that it can be dynamically frozen and stored as a process in a variable, and then subsequently be thawed when reactivated as a sub-instance. We motivate HomeBPEL by an example of pervasive health care where treatment guidelines are dynamically deployed as sub processes that may be delegated dynamically to other workflow engines and in particular stay available for disconnected operation on mobile devices. We provide a formal semantics based on binding bigraphical reactive systems implemented in the BPL Tool as part of the Bigraphical Programming Languages project at ITU. The semantics is an extension of a semantics given previously for a simplified subset of WS-BPEL and exploits the close correspondence between bigraphs and XML to provide a formalized run-time format very close to standard WS-BPEL syntax, which also constitutes the representation of frozen sub-instances.
Mikkel Bundgaard, Arne John Glenstrup, Thomas Hildebrandt, Espen Højsgaard, Henning Niss
From Flow Logic to Static Type Systems for Coordination Languages
Abstract
Coordination languages are often used to describe open ended systems. This makes it challenging to develop tools for guaranteeing security of the coordinated systems and correctness of their interaction. Successful approaches to this problem have been based on type systems with dynamic checks; therefore, the correctness properties cannot be statically enforced. By contrast, static analysis approaches based on Flow Logic usually guarantee properties statically. In this paper we show how to combine these two approaches to obtain a static type system for describing secure access to tuple spaces and safe process migration for a dialect of the language Klaim.
Rocco De Nicola, Daniele Gorla, René Rydhof Hansen, Flemming Nielson, Hanne Riis Nielson, Christian W. Probst, Rosario Pugliese
Session Types for Orchestration Charts
Abstract
We present a novel approach for the sound orchestration of services. It is based on Orcharts and Typecharts: a service orchestration language and an associated behavioural typing language. Sessions play a pivotal role in this approach. Orcharts (orchestration charts) define session based services and Typecharts provide for session types with complex interaction patterns that generalise the request/response interaction paradigm. We provide an algorithm for deciding behavioural well typedeness. We claim that well typed service configurations have the soudness property, i.e., any session that can be initiated in a well typed configuration has its requestor and provider behave in mutual conformance and potentially reach service completion.
Alessandro Fantechi, Elie Najm
Implementing Joins Using Extensible Pattern Matching
Abstract
Join patterns are an attractive declarative way to synchronize both threads and asynchronous distributed computations. We explore joins in the context of extensible pattern matching that recently appeared in languages such as F# and Scala. Our implementation supports join patterns with multiple synchronous events, and guards. Furthermore, we integrated joins into an existing actor-based concurrency framework. It enables join patterns to be used in the context of more advanced synchronization modes, such as future-type message sending and token-passing continuations.
Philipp Haller, Tom Van Cutsem
Advice for Coordination
Abstract
We show how to extend a coordination language with support for aspect oriented programming. The main challenge is how to properly deal with the trapping of actions before the actual data have been bound to the formal parameters. This necessitates dealing with open joinpoints – which is more demanding than the closed joinpoints in more traditional aspect oriented languages like AspectJ. The usefulness of our approach is demonstrated by mechanisms for discretionary and mandatory access control policies, as usually expressed by reference monitors, as well as mechanisms for logging actions.
Chris Hankin, Flemming Nielson, Hanne Riis Nielson, Fan Yang
Modeling and Analysis of Reo Connectors Using Alloy
Abstract
Reo is an exogenous coordination language based on a calculus of channel composition. Different formal models have been developed for this language. In this paper, we present a new approach to modeling and analysis of Reo connectors using Alloy which is a lightweight modeling language based on first-order relational logic. We provide a reusable library of Reo channels in Alloy that can be used to create a model of a Reo connector in Alloy. The model is simple and reflects the original structure of the connector. Furthermore, the model of a connector can be reused as a component for constructing more complex connectors. Using the Alloy Analyzer tool, properties expressed as predicates can be verified by automatically analyzing the execution traces of the Reo connector. We handle the context-sensitive behavior of channels as well as optional constraints on the interactions with environment. Our compositional model can be used as an alternative to other existing approaches, and is supported by a well known tool with a rich set of features such as counterexample generation.
Ramtin Khosravi, Marjan Sirjani, Nesa Asoudeh, Shaghayegh Sahebi, Hamed Iravanchi
Alternating-Time Stream Logic for Multi-agent Systems
Abstract
Constraint automata have been introduced to provide a compositional, operational semantics for the exogenous coordination language Reo, but they can also serve interface specification for components and an operational model for other coordination languages. Constraint automata have been used as basis for equivalence checking and model checking temporal logical properties. The main contribution of this paper is to reason about the local view and interaction and cooperation facilities of individual components or coalitions of components by means of a multi-player semantics for constraint automata. We introduce a temporal logic framework that combines classical features of alternating-time logic (\({\it ATL}\)) for concurrent games with special operators to specify the observable data flow at the I/O-ports of components. Since constraint automata support any kind of synchronous and asynchronous peer-to-peer communication, the resulting game structure is non-standard and requires a series of nontrivial adaptations of the \({\it ATL}\) model checking algorithm.
Sascha Klüppelholz, Christel Baier
A Formal Account of WS-BPEL
Abstract
We introduce B \(\mathit{lite}\), a lightweight language for web services orchestration designed around some of WS-BPEL peculiar features like partner links, process termination, message correlation, long-running business transactions and compensation handlers. B \(\mathit{lite}\) formal presentation helps clarifying some ambiguous aspects of the WS-BPEL specification, which have led to engines implementing different semantics and, thus, have undermined portability of WS-BPEL programs over different platforms. We illustrate the main features of B \(\mathit{lite}\) by means of many examples, some of which are also exploited to test and compare the behaviour of three of the most known free WS-BPEL engines.
Alessandro Lapadula, Rosario Pugliese, Francesco Tiezzi
How to Infer Finite Session Types in a Calculus of Services and Sessions
Abstract
The notion of session is fundamental in service oriented applications, as it separates interactions between different instances of the same service, and it groups together basic units of work. Together with sessions, session types were introduced to track the type of the values exchanged in each session. In this paper we propose an algorithm to infer a restricted form of session types and we show that the problem is not directly related to the unification since we are in a context with duality in interactions. The discussion is based on a SCC-like [3] calculus adapted to fit session types. The calculus simplifies the discussion imposing strong syntactic constraints, but the ideas and the proposed algorithm can be adopted to study the type inference for other session oriented calculi. Also an OCaml prototype of the algorithm has been developed to show its feasibility.
Leonardo Gaetano Mezzina
An Event-Based Coordination Model for Context-Aware Applications
Abstract
Context-aware applications adapt their behavior depending on changes in their environment context. Programming such applications in a modular way requires to modularize the global context into more specific contexts and attach specific behavior to these contexts. This is reminiscent of aspects and has led to the notion of context-aware aspects. This paper revisits this notion of context-aware aspects in the light of previous work on concurrent event-based aspect-oriented programming (CEAOP). It shows how CEAOP can be extended in a seamless way in order to define a model for the coordination of concurrent adaptation rules with explicit contexts. This makes it possible to reason about the compositions of such rules. The model is concretized into a prototypical modeling language.
Angel Núñez, Jacques Noyé
Formal Analysis of BPMN Via a Translation into COWS
Abstract
A translation of the Business Process Modeling Notation into the process calculus COWS is presented. The stochastic extension of COWS is then exploited to address quantitative reasoning about the behaviour of business processes. An example of such reasoning is shown by running the PRISM probabilistic model checker on a case study.
Davide Prandi, Paola Quaglia, Nicola Zannone
Encrypted Shared Data Spaces
Abstract
The deployment of Share Data Spaces in open, possibly hostile, environments arises the need of protecting the confidentiality of the data space content. Existing approaches focus on access control mechanisms that protect the data space from untrusted agents. The basic assumption is that the hosts (and their administrators) where the data space is deployed have to be trusted. Encryption schemes can be used to protect the data space content from malicious hosts. However, these schemes do not allow searching on encrypted data. In this paper we present a novel encryption scheme that allows tuple matching on completely encrypted tuples. Since the data space does not need to decrypt tuples to perform the search, tuple confidentiality can be guaranteed even when the data space is deployed on malicious hosts (or an adversary gains access to the host). Our scheme does not require authorised agents to share keys for inserting and retrieving tuples. Each authorised agent can encrypt, decrypt, and search encrypted tuples without having to know other agents’ keys. This is beneficial inasmuch as it simplifies the task of key management. An implementation of an encrypted data space based on this scheme is described and some preliminary performance results are given.
Giovanni Russello, Changyu Dong, Naranker Dulay, Michel Chaudron, Maarten van Steen
CiAN: A Workflow Engine for MANETs
Abstract
The practice of using workflows to model complex activities in stable networks is commonplace and is supported by many commercially available workflow management systems (WfMSs). However, the use of workflows to model collaborative activities in mobile environments, while possible at the model level, has not gained traction due to the lack of a suitable WfMS for mobile networks and devices. This paper seeks to address this need. We present CiAN, a choreography-based workflow engine that is designed with MANETs in mind. We describe the design, architecture, and communication protocols used by CiAN as well as its implementation using Java. An evaluation of the communication protocol used to coordinate among various workflow participants across MANETs is also presented.
Rohan Sen, Gruia-Catalin Roman, Christopher Gill
A Process Calculus for Mobile Ad Hoc Networks
Abstract
We present the ω-calculus, a process calculus for formally modeling and reasoning about Mobile Ad Hoc Wireless Networks (MANETs) and their protocols. The ω-calculus naturally captures essential characteristics of MANETs, including the ability of a MANET node to broadcast a message to any other node within its physical transmission range (and no others), and to move in and out of the transmission range of other nodes in the network. A key feature of the ω-calculus is the separation of a node’s communication and computational behavior, described by an ω-process, from the description of its physical transmission range, referred to as an ω-process interface.
Our main technical results are as follows. We give a formal operational semantics of the ω-calculus in terms of labeled transition systems and show that the state reachability problem is decidable for finite-control ω-processes. We also prove that the ω-calculus is a conservative extension of the π-calculus, and that late bisimulation (appropriately lifted from the π-calculus to the ω-calculus) is a congruence. Congruence results are also established for a weak version of late bisimulation, which abstracts away from two types of internal actions: τ-actions, as in the π-calculus, and μ-actions, signaling node movement. Finally, we illustrate the practical utility of the calculus by developing and analyzing a formal model of a leader-election protocol for MANETs.
Anu Singh, C. R. Ramakrishnan, Scott A. Smolka
Actors with Multi-headed Message Receive Patterns
Abstract
The actor model provides high-level concurrency abstractions to coordinate simultaneous computations by message passing. Languages implementing the actor model such as Erlang commonly only support single-headed pattern matching over received messages. We propose and design an extension of Erlang style actors with receive clauses containing multi-headed message patterns. Patterns may be non-linear and constrained by guards. We provide a number of examples to show the usefulness of the extension. We also explore the design space for multi-headed message matching semantics, for example first-match and rule priority-match semantics. The various semantics are inspired by the multi-set constraint matching semantics found in Constraint Handling Rules. This provides us with a formal model to study actors with multi-headed message receive patterns. The system can be implemented efficiently and we have built a prototype as a library-extension to Haskell.
Martin Sulzmann, Edmund S. L. Lam, Peter Van Weert
A Compositional Trace Semantics for Orc
Abstract
Orc [9] is a language for task orchestration. It has a small set of primitives, but sufficient to express many useful programs succinctly. We identify an ambiguity in the trace semantics of Kitchin et al. [9]. We give possible interpretations of the ambiguous definition and show that the semantics is not adequate regardless of the interpretation. We remedy this situation by providing new operational and denotational semantics with a better treatment of variable binding, and proving an adequacy theorem to relate them. Also, we investigate strong bisimulation in Orc and show that bisimulation implies trace equivalence but not vice versa.
Dimitrios Vardoulakis, Mitchell Wand
Backmatter
Metadaten
Titel
Coordination Models and Languages
herausgegeben von
Doug Lea
Gianluigi Zavattaro
Copyright-Jahr
2008
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-68265-3
Print ISBN
978-3-540-68264-6
DOI
https://doi.org/10.1007/978-3-540-68265-3