ITU

Declarative Choreographies and Liveness

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Standard

Declarative Choreographies and Liveness. / Hildebrandt, Thomas T.; Slaats, Tijs; López, Hugo A.; Debois, Søren; Carbone, Marco.

International Conference on Formal Techniques for Distributed Objects, Components, and Systems: FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems . Springer, 2019. p. 129-147 (Lecture Notes in Computer Science, Vol. 11535).

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Harvard

Hildebrandt, TT, Slaats, T, López, HA, Debois, S & Carbone, M 2019, Declarative Choreographies and Liveness. in International Conference on Formal Techniques for Distributed Objects, Components, and Systems: FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems . Springer, Lecture Notes in Computer Science, vol. 11535, pp. 129-147. https://doi.org/10.1007/978-3-030-21759-4_8

APA

Hildebrandt, T. T., Slaats, T., López, H. A., Debois, S., & Carbone, M. (2019). Declarative Choreographies and Liveness. In International Conference on Formal Techniques for Distributed Objects, Components, and Systems: FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems (pp. 129-147). Springer. Lecture Notes in Computer Science Vol. 11535 https://doi.org/10.1007/978-3-030-21759-4_8

Vancouver

Hildebrandt TT, Slaats T, López HA, Debois S, Carbone M. Declarative Choreographies and Liveness. In International Conference on Formal Techniques for Distributed Objects, Components, and Systems: FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems . Springer. 2019. p. 129-147. (Lecture Notes in Computer Science, Vol. 11535). https://doi.org/10.1007/978-3-030-21759-4_8

Author

Hildebrandt, Thomas T. ; Slaats, Tijs ; López, Hugo A. ; Debois, Søren ; Carbone, Marco. / Declarative Choreographies and Liveness. International Conference on Formal Techniques for Distributed Objects, Components, and Systems: FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems . Springer, 2019. pp. 129-147 (Lecture Notes in Computer Science, Vol. 11535).

Bibtex

@inproceedings{486fbcd385c742d19a66809e6ade54d9,
title = "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.",
keywords = "Liveness, Choreographies, Declarative models",
author = "Hildebrandt, {Thomas T.} and Tijs Slaats and L{\'o}pez, {Hugo A.} and S{\o}ren Debois and Marco Carbone",
year = "2019",
month = jun,
doi = "10.1007/978-3-030-21759-4_8",
language = "English",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "129--147",
booktitle = "International Conference on Formal Techniques for Distributed Objects, Components, and Systems",
address = "Germany",

}

RIS

TY - GEN

T1 - Declarative Choreographies and Liveness

AU - Hildebrandt, Thomas T.

AU - Slaats, Tijs

AU - López, Hugo A.

AU - Debois, Søren

AU - Carbone, Marco

PY - 2019/6

Y1 - 2019/6

N2 - 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.

AB - 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.

KW - Liveness

KW - Choreographies

KW - Declarative models

U2 - 10.1007/978-3-030-21759-4_8

DO - 10.1007/978-3-030-21759-4_8

M3 - Article in proceedings

T3 - Lecture Notes in Computer Science

SP - 129

EP - 147

BT - International Conference on Formal Techniques for Distributed Objects, Components, and Systems

PB - Springer

ER -

ID: 84259679