Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2009 | Book

Calculi for Service-Oriented Computing Read chapter Read first chapter

Formal Methods for Web Services

9th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2009, Bertinoro, Italy, June 1-6, 2009, Advanced Lectures

Editors: Marco Bernardo, Luca Padovani, Gianluigi Zavattaro

Publisher: Springer Berlin Heidelberg

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

Table of Contents

Frontmatter
Calculi for Service-Oriented Computing
Abstract
It is widely recognised that process calculi stay to concurrent computing as lambda-calculus stays to sequential computing; in fact, they lay abstract, rigorous foundations for the analysis of interactive, communicating systems. Nowadays, the increasing popularity of Service-Oriented Computing (SOC) challenges the quest for novel abstractions tailored to the well-disciplined handling of specific issues, like long running interactions, orchestration, and unexpected events. In fact, these features emerge neatly in most SOC applications and need to be studied as first-class aspects, whereas they would be obfuscated if dealt with by sophisticated encoding in traditional process calculi. This paper overviews some of the most recent proposals emerged in the literature, pointing out their main characteristics and presents in more detail one such proposal, called CaSPiS, by providing several examples to give evidence of its flexibility. No prior acquaintance with process calculi is assumed, indeed a gentle introduction to their basics is provided before the more advanced material be presented.
Roberto Bruni
Service Interaction: Patterns, Formalization, and Analysis
Abstract
As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.
Wil M. P. van der Aalst, Arjan J. Mooij, Christian Stahl, Karsten Wolf
Synthesis and Composition of Web Services
Abstract
One of the key ideas underlying Web services is that of allowing the combination of existing services published on the Web into a new service that achieves some higher-level functionality and satisfies some business goals. As the manual development of the new composite service is recognized as a difficult and error-prone task, the automated synthesis of the composition is considered one of the key challenges in the field of Web services.
In this paper, we will present a survey of existing approaches for the synthesis of Web service compositions. We will then focus on a specific approach, the ASTRO approach, which has been shown to support complex composition requirements and to be applicable in real domains. In the paper, we will present the formal framework behind the ASTRO approach; we will present the implementation of the framework and its integration within a commercial toolkit for developing Web services; we will finally evaluate the approach on a real-world composition domain.
Annapaola Marconi, Marco Pistore
Fundamentals of Session Types
Abstract
We present a reconstruction of session types in a linear pi calculus where types are qualified as linear or unrestricted. Linearly qualified communication channels are guaranteed to occur in exactly one thread, possibly multiple times. In our language each channel is characterised by two distinct variables, one used for reading, the other for writing; scope restriction binds together two variables, thus establishing the correspondence between the two ends of a same channel. This mechanism allows a precise control of resources via a linear type system. We build the language gradually, starting from simple input/output, then adding choice, recursive types, replication and finally subtyping. We also present an algorithmic type checking system.
Vasco T. Vasconcelos
Asynchronous Session Types: Exceptions and Multiparty Interactions
Abstract
Session types are a formalism for structuring communication based on the notion of session: the structure of a conversation is abstracted as a type which is then used as a basis of validating programs through an associated type discipline. While standard session types have proven to be able to capture many real scenarios, there are cases where they are not powerful enough for describing and validating interactions involving more complex scenarios. In this note, we shall explore two extensions of session types to interactional exceptions and multiparty session in presence of asynchronous communication.
Marco Carbone, Nobuko Yoshida, Kohei Honda
Contract-Based Discovery and Adaptation of Web Services
Abstract
A contract describes the observable behavior of a Web service. When looking for Web services providing specific capabilities, the contract can be used as an important search key. This calls for a notion of contract equivalence that goes beyond nominal or structural equivalence.
In this paper we define a simple, yet expressive formal language for describing Web service contracts. We provide a natural, set-theoretic semantics of contracts and we use it for defining a family of equivalence relations that can be effectively used for discovering and adapting Web services implementing a specific contract.
Luca Padovani
Contract-Based Discovery and Composition of Web Services
Abstract
In the context of Service Oriented Computing behavioural contracts are descriptions of the observable message-passing behaviour of services. In other terms, contracts are behavioural interfaces that can be used, for instance, to check whether a group of services can be safely combined avoiding, e.g., undesired deadlocks. In this paper we consider the problem of discovering available services that can be used to implement a given service system. The idea is to first design a service system by describing the overall behaviour of each of its participant, and then instantiate such participants retrieving services exposing a behavioural contract which is conformant with the corresponding given behaviour.
Mario Bravetti, Gianluigi Zavattaro
Quantitative Analysis of Web Services Using SRMC
Abstract
In this tutorial paper we present quantitative methods for analysing Web Services with the goal of understanding how they will perform under increased demand, or when asked to serve a larger pool of service subscribers. We use a process calculus called SRMC to model the service. We apply efficient analysis techniques to numerically evaluate our model. The process calculus and the numerical analysis are supported by a set of software tools which relieve the modeller of the burden of generating and evaluating a large family of related models. The methods are illustrated on a classical example of Web Service usage in a business-to-business scenario.
Allan Clark, Stephen Gilmore, Mirco Tribastone
Backmatter
Metadata
Title
Formal Methods for Web Services
Editors
Marco Bernardo
Luca Padovani
Gianluigi Zavattaro
Copyright Year
2009
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-01918-0
Print ISBN
978-3-642-01917-3
DOI
https://doi.org/10.1007/978-3-642-01918-0

Premium Partner

    Image Credits