We provide the first formal model for declarative choreographies, which is able to express general omega-regular liveness properties. We use the Dynamic Condition Response (DCR) graphs notation for both choreographies and end-points. We define end-point projection as a restriction of DCR graphs and derive the condition for end-point projectability from the causal relationships of the graph. We illustrate the results with a running example of a Buyer-Seller-Shipper protocol. All the examples are available for simulation in the online DCR workbench at http://dcr.tools/forte19.
Title of host publication
International Conference on Formal Techniques for Distributed Objects, Components, and Systems : FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems
This page is printed from https://en.itu.dk/research/portalplaceholder?layoutfraction=top&langRef=https://pure.itu.dk/portal/da/persons/brit-ross-winthereik(8d10ea0b-0abb-4864-baf5-9de9387cfa3e)/clippings.html?pageSize=25&page=1