Abstract : 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.
Type de document :
Communication dans un congrès
Erika Ábrahám; Catuscia Palamidessi. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. Springer, Lecture Notes in Computer Science, LNCS-8461, pp.1-16, 2014, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-662-43613-4_1〉
https://hal.inria.fr/hal-01398004
Contributeur : Hal Ifip
<>
Soumis le : mercredi 16 novembre 2016 - 15:32:44
Dernière modification le : mercredi 16 novembre 2016 - 16:23:24
Document(s) archivé(s) le : jeudi 16 mars 2017 - 17:36:36
Søren Debois, Thomas Hildebrandt, Tijs Slaats, Nobuko Yoshida. Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion. Erika Ábrahám; Catuscia Palamidessi. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. Springer, Lecture Notes in Computer Science, LNCS-8461, pp.1-16, 2014, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-662-43613-4_1〉. 〈hal-01398004〉
