Adding Sessions to BPEL
Jonathan Michaux (T\'el\'ecom ParisTech), Elie Najm (T\'el\'ecom, ParisTech), Alessandro Fantechi (Universit\`a degli Studi di Firenze)
TL;DR
This paper introduces SeB, a session-based subset of BPEL, with formal semantics based on control graphs, enabling precise analysis of safe interactions in service orchestration.
Contribution
It defines SeB with formal semantics, including control links and variable usage, and introduces a novel translation approach for analyzing service interaction safety.
Findings
Formal semantics of SeB established
Interaction safety criteria defined
Framework for analyzing BPEL service interactions
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.