Declarative Choreographies and Liveness - Archive ouverte HAL Access content directly
Conference Papers Year : 2019

Declarative Choreographies and Liveness

(1) , (1) , (1, 2) , (1) , (1)
1
2

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 .
Fichier principal
Vignette du fichier
478668_1_En_8_Chapter.pdf (469.63 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02313738 , version 1 (11-10-2019)

Licence

Attribution - CC BY 4.0

Identifiers

Cite

Thomas T. Hildebrandt, Tijs Slaats, Hugo A. 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⟩
69 View
6 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More