Protocols, Observabilities and Session Types

Communication is not only an essential organisation principle for emerging large-scale distributed applications, such as those for e-Commerce, e-Science, e-Healthcare and financial technology (FinTech). It is also an effective way to use computational resources, such as microservices and manycore chips. In this new paradigm, communication and concurrency are the norm in software development rather than a marginal concern, enabling architects and programmers to harness the power of hundreds or even thousands of concurrent processes interacting through ‘message passing’. However, for this paradigm there is no well-established methodology for software development with safety and security guarantee based on clear and mathematically accurate criteria on its behaviour. This leaves uncertainty on the correctness of the construction of distributed infrastructure.  

The aim of this project is to establish general and practical foundations for safety enforcement of communication-intensive concurrent and distributed applications, building on a general theory of ‘multiparty session types’. 
 
Communications in a distributed application are commonly organised into multiple structured conversations (protocols) where a developer or programmer wishes to enforce ‘observabilities’ of system behaviours to follow a safety and security criteria given by a protocol. Here observability of systems behaviours means a visible sequence of message exchanges with more complex information such as dependency of data, secure information, cost and timing of communications. In the multiparty session types, an end-point system properly carries out its responsibility, so that observable systems behaviours as a whole obey an agreed-upon protocol. 
 
Multiparty session types articulate the basic dynamics in a respective computing paradigm, thus serving as a foundation for modelling, specification, verification, systematic testing and certification, enhanced with other methods such as monitoring and logical assertions. This project aims to fulfil this potential of multiparty session types as types for communication by carrying out experiments. To achieve this goal, the following technical objectives have been identified: 
 
1. The establishment of a uniform type theory for multiparty session types capturing a full range of application-level protocols based on behavioural theory and game semantics, as a foundation of the whole methodology. 
 
2. The establishment of a dependent and refinement type theory of specifications and verifications; and of a scalable algorithm to verify safety and security properties based on automata theory. 
 
3. The development and release of an open-source toolchain, based on (1,2), combined with Application Programming Interface (API) and with industry tools. 
 
4. A theoretically well-founded architecture which can efficiently monitor, trace, log and enforce correct observational behaviour against specifications written in (3). 
 
5. Experiments through collaboration with academic and industry partners, realising formal safety and security assurance against advanced protocols for real-world applications, including multi robotics/UAVs, financial and healthcare systems. 
 
Throughout the research programme, an active and extensive dialogue between theories (1,2) and practice (3,4,5) will be the key enabler for reaching the goals of the fellowship, ultimately establishing cross-disciplinary and co-created ICT research. The project also links assurance methodologies based on session types to the standardisation for Cloud Computing (Cloud Native Computing Foundation) and to the public regulatory requirements for the documentation of financial and e-Healthcare protocols, meeting the goals of People at the Heart of ICT.