Amending Choreographies
Ivan Lanese (Focus Team, University of Bologna/INRIA, Italy), Fabrizio, Montesi (IT University of Copenhagen, Denmark), Gianluigi Zavattaro (Focus, Team, University of Bologna/INRIA, Italy)
TL;DR
This paper introduces a transformation technique for amending choreographies that violate projection conditions, by reducing concurrency and adding hidden communications to ensure correctness without altering behavior.
Contribution
It proposes an automatic transformation method that amends non-conforming choreographies to satisfy projection conditions, expanding the set of projectable choreographies.
Findings
Successfully reduces concurrency in choreographies.
Automatically infers and adds hidden communications.
Preserves original choreography behavior.
Abstract
Choreographies are global descriptions of system behaviors, from which the local behavior of each endpoint entity can be obtained automatically through projection. To guarantee that its projection is correct, i.e. it has the same behaviors of the original choreography, a choreography usually has to respect some coherency conditions. This restricts the set of choreographies that can be projected. In this paper, we present a transformation for amending choreographies that do not respect common syntactic conditions for projection correctness. Specifically, our transformation automatically reduces the amount of concurrency, and it infers and adds hidden communications that make the resulting choreography respect the desired conditions, while preserving its behavior.
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.