Partial Typing for Asynchronous Multiparty Sessions

TL;DR

This paper introduces a partial typing system for asynchronous multiparty sessions, enabling scalable formal verification of specific subsystems within concurrent distributed systems.

Contribution

It proposes a novel partial type assignment for multiparty sessions with asynchronous communication, ensuring partial safety properties.

Findings

Partial types guarantee lock- and orphan-message-freedom in sessions

Sessions can be typed by asynchronous global types for subsets of participants

The approach improves scalability of formal verification in concurrent systems

Abstract

Formal verification methods for concurrent systems cannot always be scaled-down or tailored in order to be applied on specific subsystems. We address such an issue in a MultiParty Session Types setting by devising a partial type assignment system for multiparty sessions (i.e. sets of concurrent participants) with asynchronous communications. Sessions are possibly typed by "asynchronous global types" describing the overall behaviour of specific subsets of participants only (from which the word "partial"). Typability is proven to ensure that sessions enjoy the partial versions of the well-known properties of lock- and orphan-message-freedom.