Declarative Choreographies and Liveness
Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review
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.
Original language | English |
---|---|
Title of host publication | International Conference on Formal Techniques for Distributed Objects, Components, and Systems : FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems |
Number of pages | 19 |
Publisher | Springer |
Publication date | Jun 2019 |
Pages | 129-147 |
ISBN (Electronic) | 978-3-030-21759-4 |
DOIs | |
Publication status | Published - Jun 2019 |
Series | Lecture Notes in Computer Science |
---|---|
Volume | 11535 |
ISSN | 0302-9743 |
Downloads
No data available
ID: 84259679