Declarative Choreographies and Liveness

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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

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.
OriginalsprogEngelsk
TitelInternational Conference on Formal Techniques for Distributed Objects, Components, and Systems : FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems
Antal sider19
ForlagSpringer
Publikationsdatojun. 2019
Sider129-147
ISBN (Elektronisk)978-3-030-21759-4
DOI
StatusUdgivet - jun. 2019
NavnLecture Notes in Computer Science
Vol/bind11535
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Declarative Choreographies and Liveness'. Sammen danner de et unikt fingeraftryk.

Citationsformater