%0 Conference Proceedings
%T Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
%+ IT University of Copenhagen (ITU)
%+ Exformatics [Copenhagen]
%+ Imperial College London
%A Debois, Søren
%A Hildebrandt, Thomas
%A Slaats, Tijs
%A Yoshida, Nobuko
%Z Part 1: Specification Languages and Type Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 34th Formal Techniques for Networked and Distributed Systems (FORTE)
%C Berlin, Germany
%Y Erika Ábrahám
%Y Catuscia Palamidessi
%I Springer
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-8461
%P 1-16
%8 2014-06-03
%D 2014
%R 10.1007/978-3-662-43613-4_1
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01398004/document
%2 https://inria.hal.science/hal-01398004/file/978-3-662-43613-4_1_Chapter.pdf
%L hal-01398004
%U https://inria.hal.science/hal-01398004
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-8461