Enforcing Availability in Failure-Aware Communicating Systems

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

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

309 Downloads (Pure)

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 languageEnglish
Title of host publicationProceedings of the 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016)
EditorsElvira Albert, Ivan Lanese
PublisherSpringer
Publication date2016
Pages195-211
ISBN (Print)978-3-319-39569-2
ISBN (Electronic)978-3-319-39570-8
DOIs
Publication statusPublished - 2016
Event36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016) - Heraklion, Crete, Greece
Duration: 6 Jun 20169 Jun 2016
Conference number: 36
http://2016.discotec.org/index.php?MG=20&Mid=9&sub1=1

Conference

Conference36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016)
Number36
CountryGreece
CityHeraklion, Crete
Period06/06/201609/06/2016
Internet address
SeriesLecture Notes in Computer Science
Volume9688
ISSN0302-9743

Cite this