Session Communication and Integration
This work addresses the problem of modular protocol specification and integration in distributed systems for researchers and practitioners in formal methods and concurrency theory, representing an incremental advancement by extending existing session type theories.
The paper tackles the integration of specification modules in distributed systems by proposing a novel synchronous multiparty session type theory that separates sessions into communicating and integrating levels, resulting in a type system that enables analysis of channel safety and session conformance properties. It demonstrates this through application to system description and uses process slicing to identify violated sessions during type checking.
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.