| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Type Checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
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.
Cited literature [25 references]
https://hal.inria.fr/hal-01398004
Contributor : Hal Ifip <>
Submitted on : Wednesday, November 16, 2016 - 3:32:44 PM
Last modification on : Friday, March 22, 2019 - 4:46:03 PM
Long-term archiving on: : Thursday, March 16, 2017 - 5:36:36 PM
Contributor : Hal Ifip <>
Submitted on : Wednesday, November 16, 2016 - 3:32:44 PM
Last modification on : Friday, March 22, 2019 - 4:46:03 PM
Long-term archiving on: : Thursday, March 16, 2017 - 5:36:36 PM
File
978-3-662-43613-4_1_Chapter.pd...
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License