TY - BOOK
T1 - A Predicate Transformer for Choreographies (Full Version)
AU - Jongmans, Sung-Shik
AU - van den Bos, Petra
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
UR - https://sungshik.github.io/papers/esop2022.pdf
M3 - Technical report
T3 - OUNL-CS (Technical Reports)
BT - A Predicate Transformer for Choreographies (Full Version)
PB - Open Universiteit Nederland
CY - Heerlen
ER -