A Predicate Transformer for Choreographies (Full Version)

Sung-Shik Jongmans, Petra van den Bos

Research output: Book/ReportTechnical reportAcademic

11 Downloads (Pure)

Abstract

Abstract. Construction and analysis of distributed systems is difficult; choreographic programming is a deadlock-freedom-by-construction approach to simplify it. In this paper, we present a new theory of choreographic programming. It supports for the first time: construction of distributed systems that require decentralised decision making (i.e., if/ while-statements with multiparty conditions); analysis of distributed systems to provide not only deadlock freedom but also functional correctness (i.e., pre/postcondition reasoning). Both contributions are enabled by a single new technique, namely a predicate transformer for choreographies.
Original languageEnglish
Place of PublicationHeerlen
PublisherOpen Universiteit Nederland
Number of pages36
Publication statusPublished - 2022

Publication series

SeriesOUNL-CS (Technical Reports)
Number01
Volume2022

Fingerprint

Dive into the research topics of 'A Predicate Transformer for Choreographies (Full Version)'. Together they form a unique fingerprint.

Cite this