Enforcing Availability in Failure-Aware Communicating Systems

Hugo-Andrés López-Acosta; Flemming Nielson; Hanne Riis Nielson

doi:10.1007/978-3-319-39570-8_13

Enforcing Availability in Failure-Aware Communicating Systems

Hugo-Andrés López-Acosta
, Flemming Nielson
, Hanne Riis Nielson

Department of Applied Mathematics and Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

598 Downloads (Orbit)

Abstract

Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where the availability of components may change at runtime. We introduce the Global Quality Calculus (GCq), a process calculus featuring novel operators for multiparty, partial and collective communications; we provide a type discipline that controls how partial communications refer only to available components; and we show that well-typed choreographies enjoy progress.

Original language	English
Title of host publication	Proceedings of the 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016)
Editors	Elvira Albert, Ivan Lanese
Publisher	Springer
Publication date	2016
Pages	195-211
ISBN (Print)	978-3-319-39569-2
ISBN (Electronic)	978-3-319-39570-8
DOIs	https://doi.org/10.1007/978-3-319-39570-8_13
Publication status	Published - 2016
Event	36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016) - Heraklion, Greece Duration: 6 Jun 2016 → 9 Jun 2016 Conference number: 36 http://2016.discotec.org/index.php?MG=20&Mid=9&sub1=1

Conference

Conference	36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016)
Number	36
Country/Territory	Greece
City	Heraklion
Period	06/06/2016 → 09/06/2016
Internet address	http://2016.discotec.org/index.php?MG=20&Mid=9&sub1=1

Series	Lecture Notes in Computer Science
Volume	9688
ISSN	0302-9743

Access to Document

10.1007/978-3-319-39570-8_13

MainAccepted author manuscript, 485 KB

OpenUrl availability

Full text

Cite this

López-Acosta, H.-A., Nielson, F., & Nielson, H. R. (2016). Enforcing Availability in Failure-Aware Communicating Systems. In E. Albert, & I. Lanese (Eds.), Proceedings of the 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016) (pp. 195-211). Springer. https://doi.org/10.1007/978-3-319-39570-8_13

López-Acosta, Hugo-Andrés ; Nielson, Flemming ; Nielson, Hanne Riis. / Enforcing Availability in Failure-Aware Communicating Systems. Proceedings of the 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016). editor / Elvira Albert ; Ivan Lanese. Springer, 2016. pp. 195-211 (Lecture Notes in Computer Science, Vol. 9688).

@inproceedings{c915693ce7ff4a429f81c6c4060fdf0f,

title = "Enforcing Availability in Failure-Aware Communicating Systems",

abstract = "Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where the availability of components may change at runtime. We introduce the Global Quality Calculus (GCq), a process calculus featuring novel operators for multiparty, partial and collective communications; we provide a type discipline that controls how partial communications refer only to available components; and we show that well-typed choreographies enjoy progress.",

author = "Hugo-Andr{\'e}s L{\'o}pez-Acosta and Flemming Nielson and Nielson, \{Hanne Riis\}",

year = "2016",

doi = "10.1007/978-3-319-39570-8\_13",

language = "English",

isbn = "978-3-319-39569-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "195--211",

editor = "Albert, \{Elvira \} and Lanese, \{Ivan \}",

booktitle = "Proceedings of the 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016)",

note = "36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016), FORTE ; Conference date: 06-06-2016 Through 09-06-2016",

url = "http://2016.discotec.org/index.php?MG=20\&Mid=9\&sub1=1",

}

López-Acosta, H-A, Nielson, F & Nielson, HR 2016, Enforcing Availability in Failure-Aware Communicating Systems. in E Albert & I Lanese (eds), Proceedings of the 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016). Springer, Lecture Notes in Computer Science, vol. 9688, pp. 195-211, 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016), Heraklion, Greece, 06/06/2016. https://doi.org/10.1007/978-3-319-39570-8_13

Enforcing Availability in Failure-Aware Communicating Systems. / López-Acosta, Hugo-Andrés; Nielson, Flemming; Nielson, Hanne Riis.
Proceedings of the 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016). ed. / Elvira Albert; Ivan Lanese. Springer, 2016. p. 195-211 (Lecture Notes in Computer Science, Vol. 9688).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Enforcing Availability in Failure-Aware Communicating Systems

AU - López-Acosta, Hugo-Andrés

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

N1 - Conference code: 36

PY - 2016

Y1 - 2016

N2 - Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where the availability of components may change at runtime. We introduce the Global Quality Calculus (GCq), a process calculus featuring novel operators for multiparty, partial and collective communications; we provide a type discipline that controls how partial communications refer only to available components; and we show that well-typed choreographies enjoy progress.

AB - Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where the availability of components may change at runtime. We introduce the Global Quality Calculus (GCq), a process calculus featuring novel operators for multiparty, partial and collective communications; we provide a type discipline that controls how partial communications refer only to available components; and we show that well-typed choreographies enjoy progress.

U2 - 10.1007/978-3-319-39570-8_13

DO - 10.1007/978-3-319-39570-8_13

M3 - Article in proceedings

SN - 978-3-319-39569-2

T3 - Lecture Notes in Computer Science

SP - 195

EP - 211

BT - Proceedings of the 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016)

A2 - Albert, Elvira

A2 - Lanese, Ivan

PB - Springer

T2 - 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016)

Y2 - 6 June 2016 through 9 June 2016

ER -

López-Acosta HA, Nielson F, Nielson HR. Enforcing Availability in Failure-Aware Communicating Systems. In Albert E, Lanese I, editors, Proceedings of the 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016). Springer. 2016. p. 195-211. (Lecture Notes in Computer Science, Vol. 9688). doi: 10.1007/978-3-319-39570-8_13

Enforcing Availability in Failure-Aware Communicating Systems

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this