Timed and choreographical multiparty session types theory

Multiparty session types (MPSTs) are the formalism for describing protocols among multiple participants from a global point of view. They are used to check type-safety and deadlock freedom for programs. In real-time distributed systems, however, protocol descriptions often include: time-related specifications, such as deadline and timeout, by imposing time restrictions on interactions to guarantee the quality of service; and parallel computation for improving efficiency. The original theory of multiparty session types lacks the ability for expressing time and parallel actions in the global description. Therefore, we propose the theory of timed choreographical session types to solve the problem. To express time-related specifications, we associate time constraints and clock resets to asynchronous message passing in global types and local types. We define the labelled transition systems of timed global and local types, and prove that soundness and completeness are preserved through projection. We add a delay primitive to session calculus to achieve a minimum extension of asynchronous π- calculus and prove theorems of type preservation and subject reduction. We also formalise the theorem of time error-freedom and properties of feasibility and wait- freedom to guarantee that no deadlock is caused by time error. Additionally, we show that timed global session types enjoy progress property if the global types without time constraints and resets are verified to progress. In the theory of choreographical session types, for the purpose of precise thread management, explicit fork/merge operations for parallel composition and choice/join for branching are defined in both global and local session types and session calculus. To ensure well-behaved communications, we formalise the definition of well-formedness for global types and present sufficient conditions for verifying well-formedness. Based on choreographical session calculus, we define the operational semantics and typing system for processes and prove the theorems of subject reduction and type safety. When we model scenarios of concurrent real-time systems, it is natural to combine the formalisms of timed session types and choreographical session types. Then we add time assertions to labelled message passing operations in choreographical global and local types, and delay primitive in session calculus. Due to the orthogonality of time and parallel composition, we easily prove the theorems of subject reduction, and time error-freedom within the timed choreographical context. Due to introduced complexity in global types, we present the progress enablement and time progress property to guarantee that processes will progress.Open Acces