Type checking liveness for collaborative processes with bounded and unbounded recursion

TY - GEN

T1 - Type checking liveness for collaborative processes with bounded and unbounded recursion

AU - Debois, Søren

AU - Hildebrandt, Thomas

AU - Slaats, Tijs

AU - Yoshida, Nobuko

N1 - Conference code: 34

PY - 2014

Y1 - 2014

N2 - We present the first session typing system guaranteeing response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (data-based) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.

AB - We present the first session typing system guaranteeing response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a particular label is selected, a set of other labels, its responses, must eventually also be selected. We prove that these extended types are strictly more expressive than standard session types. We provide a type system for a process calculus similar to a subset of collaborative BPMN processes with internal (data-based) and external (event-based) branching, message passing, bounded and unbounded looping. We prove that this type system is sound, i.e., it guarantees request-response liveness for dead-lock free processes. We exemplify the use of the calculus and type system on a concrete example of an infinite state system.

U2 - 10.1007/978-3-662-43613-4_1

DO - 10.1007/978-3-662-43613-4_1

M3 - Article in proceedings

SN - 978-3-662-43612-7

T3 - Lecture notes in computer science

SP - 1

EP - 16

BT - Formal Techniques for Distributed Objects, Components, and Systems

A2 - Ábrahám, Erika

A2 - Palamidessi, Catuscia

PB - Springer

T2 - 34th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems

Y2 - 3 June 2014 through 5 June 2014

ER -