Session Communication and Integration

TL;DR

This paper introduces a two-level synchronous multiparty session type theory that separates communication and integration levels, enhancing modular protocol specification and analysis in distributed systems.

Contribution

It extends existing session type theories by proposing a novel integration mechanism with a two-level system for better modularity and analysis capabilities.

Findings

Developed a two-level session type system for pi-calculus.

Proved channel safety and session conformance properties.

Implemented process slicing to identify session violations.

Abstract

The scenario-based specification of a large distributed system is usually naturally decomposed into various modules. The integration of specification modules contrasts to the parallel composition of program components, and includes various ways such as scenario concatenation, choice, and nesting. The recent development of multiparty session types for process calculi provides useful techniques to accommodate the protocol modularisation, by encoding fragments of communication protocols in the usage of private channels for a class of agents. In this paper, we extend forgoing session type theories by enhancing the session integration mechanism. More specifically, we propose a novel synchronous multiparty session type theory, in which sessions are separated into the communicating and integrating levels. Communicating sessions record the message-based communications between multiple agents, whilst integrating sessions describe the integration of communicating ones. A two-level session type system is developed for pi-calculus with syntactic primitives for session establishment, and several key properties of the type system are studied. Applying the theory to system description, we show that a channel safety property and a session conformance property can be analysed. Also, to improve the utility of the theory, a process slicing method is used to help identify the violated sessions in the type checking.