Detail

Responsive Choice in Mobile Processes

In this talk we present the proposal for a general type notation, formal semantics and a sound,
compositional, and decidable type system to characterise some
liveness properties of distributed systems. In the context of mobile processes, we define two concepts, activeness (ability to
send/receive on a channel) and responsiveness (ability to
reliably conduct a conversation on a channel), that make the above
properties precise. The type system respects the semantic definitions of the concepts, in the sense that the logical statements it outputs are, according to the semantics, correct descriptions of the analysed process. Our work is novel in two aspects. First, since mobile processes can make and communicate choices, a fundamental component of data
representation (where a piece of data matches one of a set of
patterns) or conversations (where the protocol may permit more than
one message at each point), our types and type system use branching and selection to capture activeness and responsiveness in process constructs necessary for such usage patterns. Secondly, conditional properties offer compositionality features that permit analysing components of a system individually, and indicate, when applicable, what should be provided to the given process before the properties hold.