Adding Sessions to BPEL

Jonathan Michaux
(Télécom ParisTech)
Elie Najm
(Télécom ParisTech)
Alessandro Fantechi
(Università degli Studi di Firenze)

By considering an essential subset of the BPEL orchestration language, we define SeB, a session based style of this subset. We discuss the formal semantics of SeB and we present its main properties. We use a new approach to address the formal semantics, based on a translation into so-called control graphs. Our semantics handles control links and addresses the static semantics that prescribes the valid usage of variables. We also provide the semantics of collections of networked services.

Relying on these semantics, we define precisely what is meant by interaction safety, paving the way to the formal analysis of safe interactions between BPEL services.

In Josep Silva and Francesco Tiezzi: Proceedings 8th International Workshop on Automated Specification and Verification of Web Systems (WWV 2012), Stockholm, Sweden, 16th July 2012, Electronic Proceedings in Theoretical Computer Science 98, pp. 60–76.
Published: 22nd October 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.98.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org