%0 Conference Proceedings
%T Enforcing Availability in Failure-Aware Communicating Systems
%+ Danmarks Tekniske Universitet = Technical University of Denmark (DTU)
%A López, Hugo, A.
%A Nielson, Flemming
%A Nielson, Hanne, Riis
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Heraklion, Greece
%Y Elvira Albert
%Y Ivan Lanese
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9688
%P 195-211
%8 2016-06-06
%D 2016
%R 10.1007/978-3-319-39570-8_13
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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 ($$GC_q$$), 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01432918/document
%2 https://inria.hal.science/hal-01432918/file/426757_1_En_13_Chapter.pdf
%L hal-01432918
%U https://inria.hal.science/hal-01432918
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9688