Skip to search boxSkip to navigationSkip to main content

Declarative Choreographies and Liveness

Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
 Peer-review

Open access

Publication Information

Output type

Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
 Peer-review

Host publication Subtitle

FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems

Original language

English

Pages from-to (Number of pages)

Pages 129-147 (19 pages)

Publication milestones

  • Published - 06/2019

Publication status

Published - 06/2019

Publisher

Springer, United States, Germany

Book series

  • Book series name: Lecture Notes in Computer Science
    Volume: 11535
    ISSN: 0302-9743

ISBN (Electronic)

978-3-030-21759-4

Publication IDs

  • Scopus: 85067365596

Host publication title

International Conference on Formal Techniques for Distributed Objects, Components, and Systems

Abstract

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.

Publication metrics

PlumX, opens in new tab

Citations
10
Captures
3

Access to documents