nach oben

2010 | Buch

Kapitel lesen Erstes Kapitel lesen

Web Services and Formal Methods

6th International Workshop, WS-FM 2009, Bologna, Italy, September 4-5, 2009, Revised Selected Papers

herausgegeben von: Cosimo Laneve, Jianwen Su

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Inhaltsverzeichnis

Frontmatter

Sessions and Session Types: An Overview

Abstract

We illustrate the concepts of sessions and session types as they have been developed in the setting of the π-calculus. Motivated by the goal of obtaining a formalisation closer to existing standards and aiming at their enhancement and strengthening, several extensions of the original core system have been proposed, which we survey together with the embodying of sessions into functional and object-oriented languages, as well as some implementations.

Mariangiola Dezani-Ciancaglini, Ugo de’Liguoro

Choreography Rehearsal

Abstract

We propose a methodology for statically predicting the possible interaction patterns of services within a given choreography. We focus on choreographies exploiting the event notification paradigm to manage service interactions. Control Flow Analysis techniques statically approximate which events can be delivered to match the choreography constraints and how the multicast groups can be optimised to handle event notification within the service choreography.

Chiara Bodei, Gian Luigi Ferrari

A Graph Syntax for Processes and Services

Abstract

We propose a class of hierarchical graphs equipped with a simple algebraic syntax as a convenient way to describe configurations in languages with inherently hierarchical features such as sessions, fault- handling scopes or transactions. The graph syntax can be seen as an intermediate representation language, that facilitates the encoding of structured specifications and, in particular, of process calculi, since it provides primitives for nesting, name restriction and parallel composition. The syntax is based on an algebraic presentation that faithfully characterises families of hierarchical graphs, meaning that each term of the language uniquely identifies an equivalence class of graphs (modulo graph isomorphism). Proving soundness and completeness of an encoding (i.e. proving that structurally equivalent processes are mapped to isomorphic graphs) is then facilitated and can be done by structural induction. Summing up, the graph syntax facilitates the definition of faithful encodings, yet allowing a precise visual representation. We illustrate our work with an application to a workflow language and a service-oriented calculus.

Roberto Bruni, Fabio Gadducci, Alberto Lluch Lafuente

A Formalisation of Adaptable Pervasive Flows

Abstract

Adaptable Pervasive Flows is a novel workflow-based paradigm for the design and execution of pervasive applications, where dynamic workflows situated in the real world are able to modify their execution in order to adapt to changes in their environment. In this paper, we study a formalisation of such flows by means of a formal flow language. More precisely, we define APFoL (Adaptable Pervasive Flow Language) and formalise its textual notation by encoding it in Blite, a formalisation of WS-BPEL. The encoding in Blite equips the language with a formal semantics and enables the use of automated verification techniques. We illustrate the approach with an example of a Warehouse Case Study.

Antonio Bucchiarone, Alberto Lluch Lafuente, Annapaola Marconi, Marco Pistore

Compliance Preorders for Web Services

Abstract

Compliance is a basic property of web-service architectures that ensures the absence of deadlocks and livelocks during execution. Following recent attempts in the literature, we interpret compliance as an experiment, much like the experiments made by a test process in testing theories, and use it as the basis for a notion of compliance preserving substitution of components within a composition of web services.

We review the different notions of compliance in the literature, analyze their relative strengths and weaknesses, and formalize their inter-relationships by providing a uniform formal framework where we reconcile the different perspectives that characterize them.

Michele Bugliesi, Damiano Macedonio, Luca Pino, Sabina Rossi

A Formal Semantics for the WS-BPEL Recovery Framework

The π-Calculus Way

Abstract

While current studies on Web services composition are mostly focused — from the technical viewpoint — on standards and protocols, this work investigates the adoption of formal methods for dependable composition. The Web Services Business Process Execution Language (WS-BPEL) — an OASIS standard widely adopted both in academic and industrial environments — is considered as a touchstone for concrete composition languages and an analysis of its ambiguous Recovery Framework specification is offered. In order to show the use of formal methods, a precise and unambiguous description of its (simplified) mechanisms is provided by means of a conservative extension of the π-calculus. This has to be intended as a well known case study providing methodological arguments for the adoption of formal methods in software specification. The aspect of verification is not the main topic of the paper but some hints are given.

Nicola Dragoni, Manuel Mazzara

Realizability Is Controllability

Abstract

A choreography describes the interaction between services. It may be used for specification purposes, for instance serving as a contract in the design of an inter-organizational business process. Typically, not all describable interactions make sense which motivates the study of the realizability problem for a given choreography.

In this paper, we show that realizability can be traced back to the problem of controllability which asks whether a service has compatible partner processes. This way of thinking makes algorithms for controllability available for reasoning about realizability. In addition, it suggests alternative definitions for realizability. We discuss several proposals for defining realizability which differ in the degree of coverage of the specified interaction.

Niels Lohmann, Karsten Wolf

Specification and Verification of Multi-user Data-Driven Web Applications

Abstract

We propose a model for multi-user data-driven communicating Web applications. An arbitrary number of users may access the application concurrently through Web sites and Web services. A Web service may have an arbitrary number of instances. The interaction between users and Web application is data-driven. Synchronous communication is done by shared access to the database and global application state. Private information may be stored in a local state. Asynchronous communication is done by message passing. A version of first-order linear time temporal logic (LTL-FO) is proposed to express behavioral properties of Web applications. The model is used to formally specify a significant fragment of an e-business application. Some of its desirable properties are expressed as LTL-FO formulas. We study a decision problem, namely whether the model satisfies an LTL-FO formula. We show the undecidability of the unrestricted verification problem and discuss some restrictions that ensure decidability.

Monica Marcus

Automated Composition of Nondeterministic Stateful Services

Abstract

This paper addresses the automated composition of nondeterministic available services modeled as transition systems. Nondeterminism stems naturally when the results of client-service interactions cannot be foreseen, and calls for specific orchestration strategies able to deal with partial controllability. We show how to build a set of orchestrators, by resorting to a variant of the simulation relation’s formal notion, by exploiting recent results on LTL formulas’ synthesis and by reducing our technique to the search for a safety game winning strategy. The resulting technique is sound, complete and optimal w.r.t. computational complexity, and generates all possible solutions at once.

Giuseppe De Giacomo, Fabio Patrizi

Towards Compensation Correctness in Interactive Systems

Abstract

One fundamental idea of service-oriented computing is that applications should be developed by composing already available services. Due to the long running nature of service interactions, a main challenge in service composition is ensuring correctness of failure recovery. In this paper, we use a process calculus suitable for modelling long running transactions with a recovery mechanism based on compensations. Within this setting, we discuss and formally state correctness criteria for compensable processes compositions, assuming that each process is correct with respect to failure recovery. Under our theory, we formally interpret self-healing compositions, that can detect and recover from failures, as correct compositions of compensable processes.

Cátia Vaz, Carla Ferreira

Small Specifications for Tree Update

Abstract

O’Hearn, Reynolds and Yang introduced Separation Logic to provide modular reasoning about simple, mutable data structures in memory. They were able to construct small specifications of programs, by reasoning about the local parts of memory accessed by programs. Gardner, Calcagno and Zarfaty generalised this work, introducing Context Logic to reason about more complex data structures. In particular, they developed a formal, compositional specification of the Document Object Model, a W3C XML update library. Whilst keeping to the spirit of local reasoning, they were not able to retain small specifications. We introduce Segment Logic, which provides a more fine-grained analysis of the tree structure and yields small specifications. As well as being aesthetically pleasing, small specifications are important for reasoning about concurrent tree update.

Philippa Gardner, Mark Wheelhouse

Backmatter

Titel: Web Services and Formal Methods
herausgegeben von: Cosimo Laneve
Jianwen Su
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-14458-5
Print ISBN: 978-3-642-14457-8
DOI: https://doi.org/10.1007/978-3-642-14458-5