Declarative Choreographies and Liveness

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

Thomas T. Hildebrandt, Tijs Slaats, Hugo A. López, Søren Debois, Marco Carbone

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.

OriginalsprogEngelsk
TitelFormal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings
RedaktørerJorge A. Pérez, Nobuko Yoshida
Antal sider19
ForlagSpringer
Publikationsdato2019
Sider129-147
ISBN (Trykt)9783030217587
DOI
StatusUdgivet - 2019
Begivenhed39th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019 - Kongens Lyngby, Danmark
Varighed: 17 jun. 201921 jun. 2019

Konference

Konference39th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019
LandDanmark
ByKongens Lyngby
Periode17/06/201921/06/2019
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind11535 LNCS
ISSN0302-9743

ID: 227336580