Skip to Main content Skip to Navigation
Conference papers

Declarative Choreographies and Liveness

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 .
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-02313738
Contributor : Hal Ifip <>
Submitted on : Friday, October 11, 2019 - 2:55:21 PM
Last modification on : Wednesday, January 22, 2020 - 2:52:07 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Thomas Hildebrandt, Tijs Slaats, Hugo López, Søren Debois, Marco Carbone. Declarative Choreographies and Liveness. 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2019, Copenhagen, Denmark. pp.129-147, ⟨10.1007/978-3-030-21759-4_8⟩. ⟨hal-02313738⟩

Share

Metrics

Record views

59